%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS159+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:43 EDT 2024 % Result : Theorem 59.47s 59.55s % Output : CNFRefutation 59.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS159+1 : TPTP v8.2.0. Released v3.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n017.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Wed Jun 19 12:28:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 59.40/59.50 %------------------------------------------- % 59.40/59.50 % File :CSE---1.7 % 59.40/59.50 % Problem :theBenchmark % 59.40/59.50 % Transform :cnf % 59.40/59.50 % Format :tptp:raw % 59.40/59.51 % Command :java -jar mcs_scs.jar %d %s % 59.40/59.51 % 59.40/59.51 % Result :Theorem 58.830000s % 59.40/59.51 % Output :CNFRefutation 58.830000s % 59.40/59.51 %------------------------------------------- % 59.40/59.52 %------------------------------------------------------------------------------ % 59.40/59.52 % File : KRS159+1 : TPTP v8.2.0. Released v3.1.0. % 59.40/59.52 % Domain : Knowledge Representation (Semantic Web) % 59.40/59.52 % Problem : DL Test: k_path ABox test from DL98 systems comparison % 59.40/59.52 % Version : Especial. % 59.40/59.52 % English : % 59.40/59.52 % 59.40/59.52 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 59.40/59.52 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 59.40/59.52 % Source : [Bec03] % 59.40/59.52 % Names : positive_description-logic-Manifest666 [Bec03] % 59.40/59.52 % 59.40/59.52 % Status : Theorem % 59.40/59.52 % Rating : 0.12 v8.2.0, 0.13 v8.1.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.15 v6.2.0, 0.18 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.29 v5.4.0, 0.22 v5.3.0, 0.30 v5.2.0, 0.21 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.21 v4.0.0, 0.20 v3.7.0, 0.67 v3.5.0, 0.38 v3.4.0, 0.42 v3.3.0, 0.22 v3.2.0, 0.44 v3.1.0 % 59.40/59.52 % Syntax : Number of formulae : 343 ( 127 unt; 0 def) % 59.40/59.52 % Number of atoms : 690 ( 0 equ) % 59.40/59.52 % Maximal formula atoms : 54 ( 2 avg) % 59.40/59.52 % Number of connectives : 401 ( 54 ~; 0 |; 132 &) % 59.40/59.52 % ( 187 <=>; 28 =>; 0 <=; 0 <~>) % 59.40/59.52 % Maximal formula depth : 52 ( 3 avg) % 59.40/59.52 % Maximal term depth : 1 ( 1 avg) % 59.40/59.52 % Number of predicates : 197 ( 197 usr; 0 prp; 1-2 aty) % 59.40/59.52 % Number of functors : 11 ( 11 usr; 11 con; 0-0 aty) % 59.40/59.52 % Number of variables : 353 ( 217 !; 136 ?) % 59.40/59.52 % SPC : FOF_THM_RFO_NEQ % 59.40/59.52 % 59.40/59.52 % Comments : Sean Bechhofer says there are some errors in the encoding of % 59.40/59.52 % datatypes, so this problem may not be perfect. At least it's % 59.40/59.52 % still representative of the type of reasoning required for OWL. % 59.40/59.52 %------------------------------------------------------------------------------ % 59.40/59.52 %----Thing and Nothing % 59.40/59.52 fof(axiom_0,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cowlThing(X) % 59.40/59.52 & ~ cowlNothing(X) ) ). % 59.40/59.52 % 59.40/59.52 %----String and Integer disjoint % 59.40/59.52 fof(axiom_1,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( xsd_string(X) % 59.40/59.52 <=> ~ xsd_integer(X) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC10 % 59.40/59.52 fof(axiom_2,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC10(X) % 59.40/59.52 <=> ( cC8(X) % 59.40/59.52 & cC4(X) ) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC100 % 59.40/59.52 fof(axiom_3,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC100(X) % 59.40/59.52 <=> ? [Y0] : ra_Px33(X,Y0) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC100xcomp % 59.40/59.52 fof(axiom_4,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC100xcomp(X) % 59.40/59.52 <=> ~ ? [Y] : ra_Px33(X,Y) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC102 % 59.40/59.52 fof(axiom_5,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC102(X) % 59.40/59.52 <=> ~ ? [Y] : ra_Px34(X,Y) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC102 % 59.40/59.52 fof(axiom_6,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC102(X) % 59.40/59.52 <=> ? [Y] : % 59.40/59.52 ( rR1(X,Y) % 59.40/59.52 & cC6xcomp(Y) ) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC102xcomp % 59.40/59.52 fof(axiom_7,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC102xcomp(X) % 59.40/59.52 <=> ? [Y0] : ra_Px34(X,Y0) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC104 % 59.40/59.52 fof(axiom_8,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC104(X) % 59.40/59.52 <=> ( cC102xcomp(X) % 59.40/59.52 & cC100xcomp(X) ) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC104 % 59.40/59.52 fof(axiom_9,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC104(X) % 59.40/59.52 <=> ~ ? [Y] : ra_Px85(X,Y) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC104xcomp % 59.40/59.52 fof(axiom_10,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC104xcomp(X) % 59.40/59.52 <=> ? [Y0] : ra_Px85(X,Y0) ) ). % 59.40/59.52 % 59.40/59.52 %----Equality cC106 % 59.40/59.52 fof(axiom_11,axiom, % 59.40/59.52 ! [X] : % 59.40/59.52 ( cC106(X) % 59.40/59.52 <=> ? [Y] : % 59.40/59.52 ( rR1(X,Y) % 59.40/59.52 & cC104(Y) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC106 % 59.47/59.52 fof(axiom_12,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC106(X) % 59.47/59.52 <=> ? [Y0] : ra_Px36(X,Y0) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC106xcomp % 59.47/59.52 fof(axiom_13,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC106xcomp(X) % 59.47/59.52 <=> ~ ? [Y] : ra_Px36(X,Y) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC108 % 59.47/59.52 fof(axiom_14,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC108(X) % 59.47/59.52 <=> ( cC98xcomp(X) % 59.47/59.52 & cC106xcomp(X) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC110 % 59.47/59.52 fof(axiom_15,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC110(X) % 59.47/59.52 <=> ( cC108(X) % 59.47/59.52 & cTOP(X) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC112 % 59.47/59.52 fof(axiom_16,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC112(X) % 59.47/59.52 <=> ( cC110(X) % 59.47/59.52 & cC90(X) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC114 % 59.47/59.52 fof(axiom_17,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC114(X) % 59.47/59.52 <=> cTOP(X) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC116 % 59.47/59.52 fof(axiom_18,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC116(X) % 59.47/59.52 <=> ( cC114(X) % 59.47/59.52 & cC112(X) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC118 % 59.47/59.52 fof(axiom_19,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC118(X) % 59.47/59.52 <=> ? [Y] : % 59.47/59.52 ( rR1(X,Y) % 59.47/59.52 & cC92xcomp(Y) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC118 % 59.47/59.52 fof(axiom_20,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC118(X) % 59.47/59.52 <=> ? [Y0] : ra_Px39(X,Y0) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC118xcomp % 59.47/59.52 fof(axiom_21,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC118xcomp(X) % 59.47/59.52 <=> ~ ? [Y] : ra_Px39(X,Y) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC12 % 59.47/59.52 fof(axiom_22,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC12(X) % 59.47/59.52 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC12xcomp % 59.47/59.52 fof(axiom_23,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC12xcomp(X) % 59.47/59.52 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC120 % 59.47/59.52 fof(axiom_24,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC120(X) % 59.47/59.52 <=> ? [Y0] : ra_Px84(X,Y0) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC120 % 59.47/59.52 fof(axiom_25,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC120(X) % 59.47/59.52 <=> ( cC92xcomp(X) % 59.47/59.52 & cC118xcomp(X) ) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC120xcomp % 59.47/59.52 fof(axiom_26,axiom, % 59.47/59.52 ! [X] : % 59.47/59.52 ( cC120xcomp(X) % 59.47/59.52 <=> ~ ? [Y] : ra_Px84(X,Y) ) ). % 59.47/59.52 % 59.47/59.52 %----Equality cC122 % 59.47/59.52 fof(axiom_27,axiom, % 59.47/59.52 ! [X] : % 59.47/59.53 ( cC122(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px43(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC122 % 59.47/59.53 fof(axiom_28,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC122(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC120(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC122xcomp % 59.47/59.53 fof(axiom_29,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC122xcomp(X) % 59.47/59.53 <=> ? [Y0] : ra_Px43(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC124 % 59.47/59.53 fof(axiom_30,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC124(X) % 59.47/59.53 <=> ? [Y0] : ra_Px42(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC124 % 59.47/59.53 fof(axiom_31,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC124(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC92xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC124xcomp % 59.47/59.53 fof(axiom_32,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC124xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px42(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC126 % 59.47/59.53 fof(axiom_33,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC126(X) % 59.47/59.53 <=> ? [Y0] : ra_Px83(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC126 % 59.47/59.53 fof(axiom_34,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC126(X) % 59.47/59.53 <=> ( cC124xcomp(X) % 59.47/59.53 & cC100xcomp(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC126xcomp % 59.47/59.53 fof(axiom_35,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC126xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px83(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC128 % 59.47/59.53 fof(axiom_36,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC128(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC126(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC128 % 59.47/59.53 fof(axiom_37,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC128(X) % 59.47/59.53 <=> ? [Y0] : ra_Px44(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC128xcomp % 59.47/59.53 fof(axiom_38,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC128xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px44(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC130 % 59.47/59.53 fof(axiom_39,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC130(X) % 59.47/59.53 <=> ( cC128xcomp(X) % 59.47/59.53 & cC122xcomp(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC132 % 59.47/59.53 fof(axiom_40,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC132(X) % 59.47/59.53 <=> ( cC130(X) % 59.47/59.53 & cTOP(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC134 % 59.47/59.53 fof(axiom_41,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC134(X) % 59.47/59.53 <=> ( cC116(X) % 59.47/59.53 & cC132(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC136 % 59.47/59.53 fof(axiom_42,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC136(X) % 59.47/59.53 <=> cTOP(X) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC138 % 59.47/59.53 fof(axiom_43,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC138(X) % 59.47/59.53 <=> ( cC136(X) % 59.47/59.53 & cC134(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC14 % 59.47/59.53 fof(axiom_44,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC14(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC12xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC140 % 59.47/59.53 fof(axiom_45,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC140(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC100xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC140 % 59.47/59.53 fof(axiom_46,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC140(X) % 59.47/59.53 <=> ? [Y0] : ra_Px47(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC140xcomp % 59.47/59.53 fof(axiom_47,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC140xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px47(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC142 % 59.47/59.53 fof(axiom_48,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC142(X) % 59.47/59.53 <=> ( cC140xcomp(X) % 59.47/59.53 & cC92xcomp(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC142 % 59.47/59.53 fof(axiom_49,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC142(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px82(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC142xcomp % 59.47/59.53 fof(axiom_50,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC142xcomp(X) % 59.47/59.53 <=> ? [Y0] : ra_Px82(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC144 % 59.47/59.53 fof(axiom_51,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC144(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC142(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC144 % 59.47/59.53 fof(axiom_52,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC144(X) % 59.47/59.53 <=> ? [Y0] : ra_Px51(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC144xcomp % 59.47/59.53 fof(axiom_53,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC144xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px51(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC146 % 59.47/59.53 fof(axiom_54,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC146(X) % 59.47/59.53 <=> ? [Y0] : ra_Px50(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC146 % 59.47/59.53 fof(axiom_55,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC146(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC100xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC146xcomp % 59.47/59.53 fof(axiom_56,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC146xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px50(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC148 % 59.47/59.53 fof(axiom_57,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC148(X) % 59.47/59.53 <=> ? [Y0] : ra_Px81(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC148 % 59.47/59.53 fof(axiom_58,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC148(X) % 59.47/59.53 <=> ( cC100xcomp(X) % 59.47/59.53 & cC146xcomp(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC148xcomp % 59.47/59.53 fof(axiom_59,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC148xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px81(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC150 % 59.47/59.53 fof(axiom_60,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC150(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px52(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC150 % 59.47/59.53 fof(axiom_61,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC150(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC148(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC150xcomp % 59.47/59.53 fof(axiom_62,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC150xcomp(X) % 59.47/59.53 <=> ? [Y0] : ra_Px52(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC152 % 59.47/59.53 fof(axiom_63,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC152(X) % 59.47/59.53 <=> ( cC144xcomp(X) % 59.47/59.53 & cC150xcomp(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC154 % 59.47/59.53 fof(axiom_64,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC154(X) % 59.47/59.53 <=> ( cC152(X) % 59.47/59.53 & cTOP(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC156 % 59.47/59.53 fof(axiom_65,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC156(X) % 59.47/59.53 <=> ( cC154(X) % 59.47/59.53 & cC138(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC158 % 59.47/59.53 fof(axiom_66,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC158(X) % 59.47/59.53 <=> ( cC22(X) % 59.47/59.53 & cC156(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC16 % 59.47/59.53 fof(axiom_67,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC16(X) % 59.47/59.53 <=> ( cC10(X) % 59.47/59.53 & cC14(X) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC160 % 59.47/59.53 fof(axiom_68,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC160(X) % 59.47/59.53 <=> ? [Y0] : ra_Px80(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC160 % 59.47/59.53 fof(axiom_69,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC160(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC6xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC160xcomp % 59.47/59.53 fof(axiom_70,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC160xcomp(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px80(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC162 % 59.47/59.53 fof(axiom_71,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC162(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px55(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC162 % 59.47/59.53 fof(axiom_72,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC162(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC160(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC162xcomp % 59.47/59.53 fof(axiom_73,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC162xcomp(X) % 59.47/59.53 <=> ? [Y0] : ra_Px55(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC164 % 59.47/59.53 fof(axiom_74,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC164(X) % 59.47/59.53 <=> ? [Y] : % 59.47/59.53 ( rR1(X,Y) % 59.47/59.53 & cC92xcomp(Y) ) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC164 % 59.47/59.53 fof(axiom_75,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC164(X) % 59.47/59.53 <=> ~ ? [Y] : ra_Px79(X,Y) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC164xcomp % 59.47/59.53 fof(axiom_76,axiom, % 59.47/59.53 ! [X] : % 59.47/59.53 ( cC164xcomp(X) % 59.47/59.53 <=> ? [Y0] : ra_Px79(X,Y0) ) ). % 59.47/59.53 % 59.47/59.53 %----Equality cC166 % 59.47/59.54 fof(axiom_77,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC166(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC164(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC166 % 59.47/59.54 fof(axiom_78,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC166(X) % 59.47/59.54 <=> ? [Y0] : ra_Px56(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC166xcomp % 59.47/59.54 fof(axiom_79,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC166xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px56(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC168 % 59.47/59.54 fof(axiom_80,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC168(X) % 59.47/59.54 <=> ( cC162xcomp(X) % 59.47/59.54 & cC166xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC170 % 59.47/59.54 fof(axiom_81,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC170(X) % 59.47/59.54 <=> ? [Y0] : ra_Px78(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC170 % 59.47/59.54 fof(axiom_82,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC170(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC18xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC170xcomp % 59.47/59.54 fof(axiom_83,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC170xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px78(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC172 % 59.47/59.54 fof(axiom_84,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC172(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px58(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC172 % 59.47/59.54 fof(axiom_85,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC172(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC170(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC172xcomp % 59.47/59.54 fof(axiom_86,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC172xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px58(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC174 % 59.47/59.54 fof(axiom_87,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC174(X) % 59.47/59.54 <=> ( cC172xcomp(X) % 59.47/59.54 & cC168(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC176 % 59.47/59.54 fof(axiom_88,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC176(X) % 59.47/59.54 <=> ? [Y0] : ra_Px77(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC176 % 59.47/59.54 fof(axiom_89,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC176(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC100xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC176xcomp % 59.47/59.54 fof(axiom_90,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC176xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px77(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC178 % 59.47/59.54 fof(axiom_91,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC178(X) % 59.47/59.54 <=> ? [Y0] : ra_Px60(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC178 % 59.47/59.54 fof(axiom_92,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC178(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC176(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC178xcomp % 59.47/59.54 fof(axiom_93,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC178xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px60(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC18 % 59.47/59.54 fof(axiom_94,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC18(X) % 59.47/59.54 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC18xcomp % 59.47/59.54 fof(axiom_95,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC18xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC180 % 59.47/59.54 fof(axiom_96,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC180(X) % 59.47/59.54 <=> ( cC174(X) % 59.47/59.54 & cC178xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC2 % 59.47/59.54 fof(axiom_97,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC2(X) % 59.47/59.54 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC2xcomp % 59.47/59.54 fof(axiom_98,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC2xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC20 % 59.47/59.54 fof(axiom_99,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC20(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC18xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC22 % 59.47/59.54 fof(axiom_100,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC22(X) % 59.47/59.54 <=> ( cC20(X) % 59.47/59.54 & cC16(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC24 % 59.47/59.54 fof(axiom_101,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC24(X) % 59.47/59.54 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC24 % 59.47/59.54 fof(axiom_102,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC24(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC2xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC24xcomp % 59.47/59.54 fof(axiom_103,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC24xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC26 % 59.47/59.54 fof(axiom_104,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC26(X) % 59.47/59.54 <=> ? [Y0] : ra_Px92(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC26 % 59.47/59.54 fof(axiom_105,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC26(X) % 59.47/59.54 <=> ( cC24xcomp(X) % 59.47/59.54 & cC2xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC26xcomp % 59.47/59.54 fof(axiom_106,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC26xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px92(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC28 % 59.47/59.54 fof(axiom_107,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC28(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC26(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC28 % 59.47/59.54 fof(axiom_108,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC28(X) % 59.47/59.54 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC28xcomp % 59.47/59.54 fof(axiom_109,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC28xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC30 % 59.47/59.54 fof(axiom_110,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC30(X) % 59.47/59.54 <=> ? [Y0] : ra_Px8(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC30 % 59.47/59.54 fof(axiom_111,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC30(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC12xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC30xcomp % 59.47/59.54 fof(axiom_112,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC30xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px8(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC32 % 59.47/59.54 fof(axiom_113,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC32(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px91(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC32 % 59.47/59.54 fof(axiom_114,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC32(X) % 59.47/59.54 <=> ( cC2xcomp(X) % 59.47/59.54 & cC30xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC32xcomp % 59.47/59.54 fof(axiom_115,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC32xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px91(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC34 % 59.47/59.54 fof(axiom_116,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC34(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px10(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC34 % 59.47/59.54 fof(axiom_117,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC34(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC32(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC34xcomp % 59.47/59.54 fof(axiom_118,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC34xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px10(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC36 % 59.47/59.54 fof(axiom_119,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC36(X) % 59.47/59.54 <=> ( cC34xcomp(X) % 59.47/59.54 & cC28xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC38 % 59.47/59.54 fof(axiom_120,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC38(X) % 59.47/59.54 <=> ( cC36(X) % 59.47/59.54 & cTOP(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC4 % 59.47/59.54 fof(axiom_121,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC4(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC2xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC40 % 59.47/59.54 fof(axiom_122,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC40(X) % 59.47/59.54 <=> cTOP(X) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC42 % 59.47/59.54 fof(axiom_123,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC42(X) % 59.47/59.54 <=> ( cC40(X) % 59.47/59.54 & cC38(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC44 % 59.47/59.54 fof(axiom_124,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC44(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px13(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC44 % 59.47/59.54 fof(axiom_125,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC44(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC2xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC44xcomp % 59.47/59.54 fof(axiom_126,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC44xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px13(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC46 % 59.47/59.54 fof(axiom_127,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC46(X) % 59.47/59.54 <=> ? [Y0] : ra_Px90(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC46 % 59.47/59.54 fof(axiom_128,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC46(X) % 59.47/59.54 <=> ( cC44xcomp(X) % 59.47/59.54 & cC12xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC46xcomp % 59.47/59.54 fof(axiom_129,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC46xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px90(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC48 % 59.47/59.54 fof(axiom_130,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC48(X) % 59.47/59.54 <=> ? [Y0] : ra_Px17(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC48 % 59.47/59.54 fof(axiom_131,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC48(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC46(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC48xcomp % 59.47/59.54 fof(axiom_132,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC48xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px17(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC50 % 59.47/59.54 fof(axiom_133,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC50(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC12xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC50 % 59.47/59.54 fof(axiom_134,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC50(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px16(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC50xcomp % 59.47/59.54 fof(axiom_135,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC50xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px16(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC52 % 59.47/59.54 fof(axiom_136,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC52(X) % 59.47/59.54 <=> ? [Y0] : ra_Px89(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC52 % 59.47/59.54 fof(axiom_137,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC52(X) % 59.47/59.54 <=> ( cC50xcomp(X) % 59.47/59.54 & cC12xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC52xcomp % 59.47/59.54 fof(axiom_138,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC52xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px89(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC54 % 59.47/59.54 fof(axiom_139,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC54(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC52(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC54 % 59.47/59.54 fof(axiom_140,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC54(X) % 59.47/59.54 <=> ? [Y0] : ra_Px18(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC54xcomp % 59.47/59.54 fof(axiom_141,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC54xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px18(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC56 % 59.47/59.54 fof(axiom_142,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC56(X) % 59.47/59.54 <=> ( cC48xcomp(X) % 59.47/59.54 & cC54xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC58 % 59.47/59.54 fof(axiom_143,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC58(X) % 59.47/59.54 <=> ( cC56(X) % 59.47/59.54 & cTOP(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC6 % 59.47/59.54 fof(axiom_144,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC6(X) % 59.47/59.54 <=> ? [Y0] : ra_Px27(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC6xcomp % 59.47/59.54 fof(axiom_145,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC6xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px27(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC60 % 59.47/59.54 fof(axiom_146,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC60(X) % 59.47/59.54 <=> ( cC58(X) % 59.47/59.54 & cC42(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC62 % 59.47/59.54 fof(axiom_147,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC62(X) % 59.47/59.54 <=> cTOP(X) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC64 % 59.47/59.54 fof(axiom_148,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC64(X) % 59.47/59.54 <=> ( cC60(X) % 59.47/59.54 & cC62(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC66 % 59.47/59.54 fof(axiom_149,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC66(X) % 59.47/59.54 <=> ? [Y0] : ra_Px21(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC66 % 59.47/59.54 fof(axiom_150,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC66(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC2xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC66xcomp % 59.47/59.54 fof(axiom_151,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC66xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px21(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC68 % 59.47/59.54 fof(axiom_152,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC68(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px88(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC68 % 59.47/59.54 fof(axiom_153,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC68(X) % 59.47/59.54 <=> ( cC18xcomp(X) % 59.47/59.54 & cC66xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC68xcomp % 59.47/59.54 fof(axiom_154,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC68xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px88(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC70 % 59.47/59.54 fof(axiom_155,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC70(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC68(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC70 % 59.47/59.54 fof(axiom_156,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC70(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px25(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC70xcomp % 59.47/59.54 fof(axiom_157,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC70xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px25(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC72 % 59.47/59.54 fof(axiom_158,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC72(X) % 59.47/59.54 <=> ? [Y0] : ra_Px24(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC72 % 59.47/59.54 fof(axiom_159,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC72(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC12xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC72xcomp % 59.47/59.54 fof(axiom_160,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC72xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px24(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC74 % 59.47/59.54 fof(axiom_161,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC74(X) % 59.47/59.54 <=> ( cC72xcomp(X) % 59.47/59.54 & cC18xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC74 % 59.47/59.54 fof(axiom_162,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC74(X) % 59.47/59.54 <=> ? [Y0] : ra_Px87(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC74xcomp % 59.47/59.54 fof(axiom_163,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC74xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px87(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC76 % 59.47/59.54 fof(axiom_164,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC76(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC74(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC76 % 59.47/59.54 fof(axiom_165,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC76(X) % 59.47/59.54 <=> ? [Y0] : ra_Px26(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC76xcomp % 59.47/59.54 fof(axiom_166,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC76xcomp(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px26(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC78 % 59.47/59.54 fof(axiom_167,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC78(X) % 59.47/59.54 <=> ( cC70xcomp(X) % 59.47/59.54 & cC76xcomp(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC8 % 59.47/59.54 fof(axiom_168,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC8(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC6xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC80 % 59.47/59.54 fof(axiom_169,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC80(X) % 59.47/59.54 <=> ( cC78(X) % 59.47/59.54 & cTOP(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC82 % 59.47/59.54 fof(axiom_170,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC82(X) % 59.47/59.54 <=> ( cC64(X) % 59.47/59.54 & cC80(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC84 % 59.47/59.54 fof(axiom_171,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC84(X) % 59.47/59.54 <=> cTOP(X) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC86 % 59.47/59.54 fof(axiom_172,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC86(X) % 59.47/59.54 <=> ( cC82(X) % 59.47/59.54 & cC84(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC88 % 59.47/59.54 fof(axiom_173,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC88(X) % 59.47/59.54 <=> cTOP(X) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC90 % 59.47/59.54 fof(axiom_174,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC90(X) % 59.47/59.54 <=> ( cC86(X) % 59.47/59.54 & cC88(X) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC92 % 59.47/59.54 fof(axiom_175,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC92(X) % 59.47/59.54 <=> ~ ? [Y] : ra_Px28(X,Y) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC92xcomp % 59.47/59.54 fof(axiom_176,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC92xcomp(X) % 59.47/59.54 <=> ? [Y0] : ra_Px28(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC94 % 59.47/59.54 fof(axiom_177,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC94(X) % 59.47/59.54 <=> ? [Y0] : ra_Px29(X,Y0) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC94 % 59.47/59.54 fof(axiom_178,axiom, % 59.47/59.54 ! [X] : % 59.47/59.54 ( cC94(X) % 59.47/59.54 <=> ? [Y] : % 59.47/59.54 ( rR1(X,Y) % 59.47/59.54 & cC6xcomp(Y) ) ) ). % 59.47/59.54 % 59.47/59.54 %----Equality cC94xcomp % 59.47/59.54 fof(axiom_179,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC94xcomp(X) % 59.47/59.55 <=> ~ ? [Y] : ra_Px29(X,Y) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC96 % 59.47/59.55 fof(axiom_180,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC96(X) % 59.47/59.55 <=> ( cC94xcomp(X) % 59.47/59.55 & cC92xcomp(X) ) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC96 % 59.47/59.55 fof(axiom_181,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC96(X) % 59.47/59.55 <=> ? [Y0] : ra_Px86(X,Y0) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC96xcomp % 59.47/59.55 fof(axiom_182,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC96xcomp(X) % 59.47/59.55 <=> ~ ? [Y] : ra_Px86(X,Y) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC98 % 59.47/59.55 fof(axiom_183,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC98(X) % 59.47/59.55 <=> ? [Y] : % 59.47/59.55 ( rR1(X,Y) % 59.47/59.55 & cC96(Y) ) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC98 % 59.47/59.55 fof(axiom_184,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC98(X) % 59.47/59.55 <=> ? [Y0] : ra_Px35(X,Y0) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cC98xcomp % 59.47/59.55 fof(axiom_185,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cC98xcomp(X) % 59.47/59.55 <=> ~ ? [Y] : ra_Px35(X,Y) ) ). % 59.47/59.55 % 59.47/59.55 %----Equality cTEST % 59.47/59.55 fof(axiom_186,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( cTEST(X) % 59.47/59.55 <=> ( cC158(X) % 59.47/59.55 & cC180(X) ) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_187,axiom, % 59.47/59.55 cC150xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_188,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC170xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_189,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC46xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_190,axiom, % 59.47/59.55 cTOP(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_191,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC160xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_192,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC176xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_193,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC164xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_194,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC148xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_195,axiom, % 59.47/59.55 cC76xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_196,axiom, % 59.47/59.55 cC98xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_197,axiom, % 59.47/59.55 cC128xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_198,axiom, % 59.47/59.55 cC166xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_199,axiom, % 59.47/59.55 cC106xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_200,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC120xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_201,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC68xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_202,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC26xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_203,axiom, % 59.47/59.55 cC34xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_204,axiom, % 59.47/59.55 cC144xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_205,axiom, % 59.47/59.55 cC28xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_206,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC104xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_207,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC126xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_208,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC96xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_209,axiom, % 59.47/59.55 cC54xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_210,axiom, % 59.47/59.55 cC122xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_211,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC52xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_212,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC142xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_213,axiom, % 59.47/59.55 cC162xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_214,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC32xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_215,axiom, % 59.47/59.55 cC70xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_216,axiom, % 59.47/59.55 cC172xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_217,axiom, % 59.47/59.55 cC48xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_218,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21026,X) % 59.47/59.55 => cC74xcomp(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_219,axiom, % 59.47/59.55 cowlThing(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_220,axiom, % 59.47/59.55 cC178xcomp(iV21026) ). % 59.47/59.55 % 59.47/59.55 %----iV21026 % 59.47/59.55 fof(axiom_221,axiom, % 59.47/59.55 cTEST(iV21026) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_222,axiom, % 59.47/59.55 rR1(iV21026,iV21030) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_223,axiom, % 59.47/59.55 rR1(iV21026,iV21027) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_224,axiom, % 59.47/59.55 rR1(iV21026,iV21028) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_225,axiom, % 59.47/59.55 rR1(iV21026,iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_226,axiom, % 59.47/59.55 cC12(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_227,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21027,X) % 59.47/59.55 => cC18(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_228,axiom, % 59.47/59.55 cC176xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_229,axiom, % 59.47/59.55 cC96xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_230,axiom, % 59.47/59.55 cC170xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_231,axiom, % 59.47/59.55 cC120xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_232,axiom, % 59.47/59.55 cC92(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_233,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21027,X) % 59.47/59.55 => cC6(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_234,axiom, % 59.47/59.55 cC148xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_235,axiom, % 59.47/59.55 cC142xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_236,axiom, % 59.47/59.55 cC68xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_237,axiom, % 59.47/59.55 cC2xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_238,axiom, % 59.47/59.55 cC18(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_239,axiom, % 59.47/59.55 cC52xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_240,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21027,X) % 59.47/59.55 => cC100(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_241,axiom, % 59.47/59.55 cC104xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_242,axiom, % 59.47/59.55 cC26xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_243,axiom, % 59.47/59.55 cC46xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_244,axiom, % 59.47/59.55 cC126xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_245,axiom, % 59.47/59.55 cC164xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_246,axiom, % 59.47/59.55 cC100(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_247,axiom, % 59.47/59.55 cC160xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_248,axiom, % 59.47/59.55 cowlThing(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_249,axiom, % 59.47/59.55 cC74xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_250,axiom, % 59.47/59.55 cC32xcomp(iV21027) ). % 59.47/59.55 % 59.47/59.55 %----iV21027 % 59.47/59.55 fof(axiom_251,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21027,X) % 59.47/59.55 => cC92(X) ) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_252,axiom, % 59.47/59.55 rR1(iV21027,iV21036) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_253,axiom, % 59.47/59.55 rR1(iV21027,iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21028 % 59.47/59.55 fof(axiom_254,axiom, % 59.47/59.55 cowlThing(iV21028) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_255,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21029,X) % 59.47/59.55 => cC6(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_256,axiom, % 59.47/59.55 cC176xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_257,axiom, % 59.47/59.55 cC96xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_258,axiom, % 59.47/59.55 cC120xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_259,axiom, % 59.47/59.55 cC170xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_260,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21029,X) % 59.47/59.55 => cC18(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_261,axiom, % 59.47/59.55 cC92(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_262,axiom, % 59.47/59.55 cC148xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_263,axiom, % 59.47/59.55 cC142xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_264,axiom, % 59.47/59.55 cC68xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_265,axiom, % 59.47/59.55 cC12xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_266,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21029,X) % 59.47/59.55 => cC92(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_267,axiom, % 59.47/59.55 cC18(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_268,axiom, % 59.47/59.55 cC52xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_269,axiom, % 59.47/59.55 cC104xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_270,axiom, % 59.47/59.55 cC2(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_271,axiom, % 59.47/59.55 cC26xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_272,axiom, % 59.47/59.55 cC46xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_273,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21029,X) % 59.47/59.55 => cC100(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_274,axiom, % 59.47/59.55 cC126xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_275,axiom, % 59.47/59.55 cC164xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_276,axiom, % 59.47/59.55 cC100(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_277,axiom, % 59.47/59.55 cC160xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_278,axiom, % 59.47/59.55 cowlThing(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_279,axiom, % 59.47/59.55 cC74xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 %----iV21029 % 59.47/59.55 fof(axiom_280,axiom, % 59.47/59.55 cC32xcomp(iV21029) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_281,axiom, % 59.47/59.55 rR1(iV21029,iV21034) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_282,axiom, % 59.47/59.55 rR1(iV21029,iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_283,axiom, % 59.47/59.55 cC12(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_284,axiom, % 59.47/59.55 cC176xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_285,axiom, % 59.47/59.55 cC96xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_286,axiom, % 59.47/59.55 cC170xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_287,axiom, % 59.47/59.55 cC120xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_288,axiom, % 59.47/59.55 cC92(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_289,axiom, % 59.47/59.55 cC148xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_290,axiom, % 59.47/59.55 cC142xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_291,axiom, % 59.47/59.55 cC68xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_292,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21030,X) % 59.47/59.55 => cC6(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_293,axiom, % 59.47/59.55 cC18xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_294,axiom, % 59.47/59.55 cC52xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_295,axiom, % 59.47/59.55 cC104xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_296,axiom, % 59.47/59.55 cC2(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_297,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21030,X) % 59.47/59.55 => cC100(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_298,axiom, % 59.47/59.55 cC26xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_299,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21030,X) % 59.47/59.55 => cC18(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_300,axiom, % 59.47/59.55 cC46xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_301,axiom, % 59.47/59.55 cC126xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_302,axiom, % 59.47/59.55 cC164xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_303,axiom, % 59.47/59.55 ! [X] : % 59.47/59.55 ( rR1(iV21030,X) % 59.47/59.55 => cC92(X) ) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_304,axiom, % 59.47/59.55 cC100(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_305,axiom, % 59.47/59.55 cC160xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_306,axiom, % 59.47/59.55 cowlThing(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_307,axiom, % 59.47/59.55 cC74xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(axiom_308,axiom, % 59.47/59.55 cC32xcomp(iV21030) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_309,axiom, % 59.47/59.55 rR1(iV21030,iV21032) ). % 59.47/59.55 % 59.47/59.55 fof(axiom_310,axiom, % 59.47/59.55 rR1(iV21030,iV21031) ). % 59.47/59.55 % 59.47/59.55 %----iV21031 % 59.47/59.55 fof(axiom_311,axiom, % 59.47/59.55 cowlThing(iV21031) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_312,axiom, % 59.47/59.55 cC2xcomp(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_313,axiom, % 59.47/59.55 cC92(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_314,axiom, % 59.47/59.55 cC100(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_315,axiom, % 59.47/59.55 cC6(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_316,axiom, % 59.47/59.55 cowlThing(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21032 % 59.47/59.55 fof(axiom_317,axiom, % 59.47/59.55 cC18(iV21032) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_318,axiom, % 59.47/59.55 cC92(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_319,axiom, % 59.47/59.55 cC12xcomp(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_320,axiom, % 59.47/59.55 cC100(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_321,axiom, % 59.47/59.55 cC6(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_322,axiom, % 59.47/59.55 cowlThing(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21033 % 59.47/59.55 fof(axiom_323,axiom, % 59.47/59.55 cC18(iV21033) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_324,axiom, % 59.47/59.55 cC92(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_325,axiom, % 59.47/59.55 cC2xcomp(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_326,axiom, % 59.47/59.55 cC100(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_327,axiom, % 59.47/59.55 cC6(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_328,axiom, % 59.47/59.55 cowlThing(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21034 % 59.47/59.55 fof(axiom_329,axiom, % 59.47/59.55 cC18(iV21034) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_330,axiom, % 59.47/59.55 cC92(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_331,axiom, % 59.47/59.55 cC12xcomp(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_332,axiom, % 59.47/59.55 cC100(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_333,axiom, % 59.47/59.55 cC6(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_334,axiom, % 59.47/59.55 cowlThing(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21035 % 59.47/59.55 fof(axiom_335,axiom, % 59.47/59.55 cC18(iV21035) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_336,axiom, % 59.47/59.55 cC92(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_337,axiom, % 59.47/59.55 cC2xcomp(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_338,axiom, % 59.47/59.55 cC100(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_339,axiom, % 59.47/59.55 cC6(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_340,axiom, % 59.47/59.55 cowlThing(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----iV21036 % 59.47/59.55 fof(axiom_341,axiom, % 59.47/59.55 cC18(iV21036) ). % 59.47/59.55 % 59.47/59.55 %----Thing and Nothing % 59.47/59.55 %----String and Integer disjoint % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21026 % 59.47/59.55 %----iV21027 % 59.47/59.55 %----iV21027 % 59.47/59.55 %----iV21027 % 59.47/59.55 %----iV21029 % 59.47/59.55 %----iV21029 % 59.47/59.55 %----iV21029 % 59.47/59.55 %----iV21030 % 59.47/59.55 %----iV21030 % 59.47/59.55 %----iV21030 % 59.47/59.55 fof(the_axiom,conjecture, % 59.47/59.55 ( ! [X] : % 59.47/59.55 ( cowlThing(X) % 59.47/59.55 & ~ cowlNothing(X) ) % 59.47/59.55 & ! [X] : % 59.47/59.55 ( xsd_string(X) % 59.47/59.55 <=> ~ xsd_integer(X) ) % 59.47/59.55 & cC108(iV21026) % 59.47/59.55 & cC40(iV21026) % 59.47/59.55 & cC136(iV21026) % 59.47/59.55 & cC10(iV21026) % 59.47/59.55 & cC90(iV21026) % 59.47/59.55 & cowlThing(iV21026) % 59.47/59.55 & cC58(iV21026) % 59.47/59.55 & cC56(iV21026) % 59.47/59.55 & cC158(iV21026) % 59.47/59.55 & cC110(iV21026) % 59.47/59.55 & cC22(iV21026) % 59.47/59.55 & cC60(iV21026) % 59.47/59.55 & cC154(iV21026) % 59.47/59.55 & cC180(iV21026) % 59.47/59.55 & cC78(iV21026) % 59.47/59.55 & cC16(iV21026) % 59.47/59.55 & cC132(iV21026) % 59.47/59.55 & cC114(iV21026) % 59.47/59.55 & cC20(iV21026) % 59.47/59.55 & cC84(iV21026) % 59.47/59.55 & cC38(iV21026) % 59.47/59.55 & cC138(iV21026) % 59.47/59.55 & cC174(iV21026) % 59.47/59.55 & cC62(iV21026) % 59.47/59.55 & cC8(iV21026) % 59.47/59.55 & cC36(iV21026) % 59.47/59.55 & cC112(iV21026) % 59.47/59.55 & cC64(iV21026) % 59.47/59.55 & cC116(iV21026) % 59.47/59.55 & cC82(iV21026) % 59.47/59.55 & cC14(iV21026) % 59.47/59.55 & cC152(iV21026) % 59.47/59.55 & cC80(iV21026) % 59.47/59.55 & cC88(iV21026) % 59.47/59.55 & cC130(iV21026) % 59.47/59.55 & cC168(iV21026) % 59.47/59.55 & cC4(iV21026) % 59.47/59.55 & cC134(iV21026) % 59.47/59.55 & cC42(iV21026) % 59.47/59.55 & cC156(iV21026) % 59.47/59.55 & cC86(iV21026) % 59.47/59.55 & cC30(iV21027) % 59.47/59.55 & cowlThing(iV21027) % 59.47/59.55 & cC24(iV21027) % 59.47/59.55 & cC50(iV21029) % 59.47/59.55 & cC44(iV21029) % 59.47/59.55 & cowlThing(iV21029) % 59.47/59.55 & cC72(iV21030) % 59.47/59.55 & cC66(iV21030) % 59.47/59.55 & cowlThing(iV21030) ) ). % 59.47/59.55 % 59.47/59.55 %------------------------------------------------------------------------------ % 59.47/59.55 %------------------------------------------- % 59.47/59.55 % Proof found % 59.47/59.55 % SZS status Theorem for theBenchmark % 59.47/59.55 % SZS output start Proof % 59.47/59.55 %ClaNum:598(EqnAxiom:0) % 59.47/59.55 %VarNum:1310(SingletonVarNum:616) % 59.47/59.55 %MaxLitNum:49 % 59.47/59.55 %MaxfuncDepth:1 % 59.47/59.55 %SharedTerms:180 % 59.47/59.55 %goalClause: 597 598 % 59.47/59.55 [1]P1(a1) % 59.47/59.55 [2]P1(a2) % 59.47/59.55 [3]P1(a142) % 59.47/59.55 [4]P1(a144) % 59.47/59.55 [5]P1(a145) % 59.47/59.55 [6]P1(a146) % 59.47/59.55 [7]P1(a147) % 59.47/59.55 [8]P1(a148) % 59.47/59.55 [9]P3(a1) % 59.47/59.55 [10]P3(a2) % 59.47/59.55 [11]P3(a142) % 59.47/59.55 [12]P8(a3) % 59.47/59.55 [13]P10(a3) % 59.47/59.55 [14]P141(a3) % 59.47/59.55 [15]P11(a1) % 59.47/59.55 [16]P11(a2) % 59.47/59.55 [17]P19(a142) % 59.47/59.55 [18]P19(a145) % 59.47/59.55 [19]P19(a147) % 59.47/59.55 [20]P20(a1) % 59.47/59.55 [21]P20(a2) % 59.47/59.55 [22]P20(a142) % 59.47/59.55 [23]P22(a3) % 59.47/59.55 [24]P24(a1) % 59.47/59.55 [25]P24(a2) % 59.47/59.55 [26]P24(a142) % 59.47/59.55 [27]P28(a3) % 59.47/59.55 [28]P30(a1) % 59.47/59.55 [29]P30(a2) % 59.47/59.55 [30]P30(a142) % 59.47/59.55 [31]P40(a3) % 59.47/59.55 [32]P42(a1) % 59.47/59.55 [33]P42(a2) % 59.47/59.55 [34]P42(a142) % 59.47/59.55 [35]P46(a3) % 59.47/59.55 [36]P48(a1) % 59.47/59.55 [37]P48(a2) % 59.47/59.55 [38]P48(a142) % 59.47/59.55 [39]P55(a3) % 59.47/59.55 [40]P57(a1) % 59.47/59.55 [41]P57(a2) % 59.47/59.55 [42]P57(a142) % 59.47/59.55 [43]P59(a3) % 59.47/59.55 [44]P61(a1) % 59.47/59.55 [45]P62(a1) % 59.47/59.55 [46]P62(a2) % 59.47/59.55 [47]P62(a142) % 59.47/59.55 [48]P65(a3) % 59.47/59.55 [49]P67(a1) % 59.47/59.55 [50]P67(a2) % 59.47/59.55 [51]P67(a142) % 59.47/59.55 [52]P70(a3) % 59.47/59.55 [53]P72(a2) % 59.47/59.55 [54]P72(a142) % 59.47/59.55 [55]P72(a144) % 59.47/59.55 [56]P72(a145) % 59.47/59.55 [57]P72(a146) % 59.47/59.55 [58]P72(a147) % 59.47/59.55 [59]P72(a148) % 59.47/59.55 [60]P74(a1) % 59.47/59.55 [61]P74(a142) % 59.47/59.55 [62]P75(a2) % 59.47/59.55 [63]P75(a144) % 59.47/59.55 [64]P75(a146) % 59.47/59.55 [65]P75(a148) % 59.47/59.55 [66]P76(a1) % 59.47/59.55 [67]P76(a2) % 59.47/59.55 [68]P76(a142) % 59.47/59.55 [69]P82(a3) % 59.47/59.55 [70]P84(a1) % 59.47/59.55 [71]P84(a2) % 59.47/59.55 [72]P84(a142) % 59.47/59.55 [73]P88(a3) % 59.47/59.55 [74]P90(a1) % 59.47/59.55 [75]P90(a2) % 59.47/59.55 [76]P90(a142) % 59.47/59.55 [77]P99(a3) % 59.47/59.55 [78]P101(a1) % 59.47/59.55 [79]P101(a2) % 59.47/59.55 [80]P101(a142) % 59.47/59.55 [81]P105(a3) % 59.47/59.55 [82]P107(a144) % 59.47/59.55 [83]P107(a145) % 59.47/59.55 [84]P107(a146) % 59.47/59.55 [85]P107(a147) % 59.47/59.55 [86]P107(a148) % 59.47/59.55 [87]P110(a1) % 59.47/59.55 [88]P110(a2) % 59.47/59.55 [89]P110(a142) % 59.47/59.55 [90]P117(a3) % 59.47/59.55 [91]P120(a1) % 59.47/59.55 [92]P120(a2) % 59.47/59.55 [93]P120(a142) % 59.47/59.55 [94]P124(a3) % 59.47/59.55 [95]P126(a1) % 59.47/59.55 [96]P126(a2) % 59.47/59.55 [97]P126(a142) % 59.47/59.55 [98]P126(a144) % 59.47/59.55 [99]P126(a145) % 59.47/59.55 [100]P126(a146) % 59.47/59.55 [101]P126(a147) % 59.47/59.55 [102]P126(a148) % 59.47/59.55 [103]P135(a1) % 59.47/59.55 [104]P135(a2) % 59.47/59.55 [105]P135(a142) % 59.47/59.55 [106]P142(a3) % 59.47/59.55 [107]P143(a3,a1) % 59.47/59.55 [108]P143(a3,a2) % 59.47/59.55 [109]P143(a3,a143) % 59.47/59.55 [110]P143(a3,a142) % 59.47/59.55 [111]P143(a1,a148) % 59.47/59.55 [112]P143(a1,a149) % 59.47/59.55 [113]P143(a2,a144) % 59.47/59.55 [114]P143(a2,a145) % 59.47/59.55 [115]P143(a142,a146) % 59.47/59.55 [116]P143(a142,a147) % 59.47/59.55 [117]~P144(x1171) % 59.47/59.55 [118]P146(x1181)+P145(x1181) % 59.47/59.55 [119]~P49(x1191)+P2(x1191) % 59.47/59.55 [120]~P2(x1201)+P127(x1201) % 59.47/59.55 [121]~P2(x1211)+P91(x1211) % 59.47/59.55 [122]~P5(x1221)+P4(x1221) % 59.47/59.55 [123]~P25(x1231)+P4(x1231) % 59.47/59.55 [124]~P43(x1241)+P4(x1241) % 59.47/59.55 [125]~P5(x1251)+P6(x1251) % 59.47/59.55 [126]~P12(x1261)+P8(x1261) % 59.47/59.55 [127]~P13(x1271)+P12(x1271) % 59.47/59.55 [128]~P12(x1281)+P10(x1281) % 59.47/59.55 [129]~P14(x1291)+P13(x1291) % 59.47/59.55 [130]~P13(x1301)+P141(x1301) % 59.47/59.55 [131]~P15(x1311)+P141(x1311) % 59.47/59.55 [132]~P31(x1321)+P141(x1321) % 59.47/59.55 [133]~P33(x1331)+P141(x1331) % 59.47/59.55 [134]~P50(x1341)+P141(x1341) % 59.47/59.55 [135]~P92(x1351)+P141(x1351) % 59.47/59.55 [136]~P94(x1361)+P141(x1361) % 59.47/59.55 [137]~P108(x1371)+P141(x1371) % 59.47/59.55 [138]~P111(x1381)+P141(x1381) % 59.47/59.55 [139]~P129(x1391)+P141(x1391) % 59.47/59.55 [140]~P130(x1401)+P141(x1401) % 59.47/59.55 [141]~P132(x1411)+P141(x1411) % 59.47/59.55 [142]~P16(x1421)+P14(x1421) % 59.47/59.55 [143]~P14(x1431)+P134(x1431) % 59.47/59.55 [144]~P141(x1441)+P15(x1441) % 59.47/59.55 [145]~P16(x1451)+P15(x1451) % 59.47/59.55 [146]~P34(x1461)+P16(x1461) % 59.47/59.55 [147]~P21(x1471)+P136(x1471) % 59.47/59.55 [148]~P35(x1481)+P136(x1481) % 59.47/59.55 [149]~P137(x1491)+P136(x1491) % 59.47/59.55 [150]~P21(x1501)+P17(x1501) % 59.47/59.55 [151]~P95(x1511)+P19(x1511) % 59.47/59.55 [152]~P102(x1521)+P19(x1521) % 59.47/59.55 [153]~P32(x1531)+P22(x1531) % 59.47/59.55 [154]~P25(x1541)+P26(x1541) % 59.47/59.55 [155]~P32(x1551)+P28(x1551) % 59.47/59.55 [156]~P31(x1561)+P32(x1561) % 59.47/59.55 [157]~P34(x1571)+P31(x1571) % 59.47/59.55 [158]~P36(x1581)+P34(x1581) % 59.47/59.55 [159]~P141(x1591)+P33(x1591) % 59.47/59.55 [160]~P36(x1601)+P33(x1601) % 59.47/59.55 [161]~P52(x1611)+P36(x1611) % 59.47/59.55 [162]~P49(x1621)+P37(x1621) % 59.47/59.55 [163]~P35(x1631)+P38(x1631) % 59.47/59.55 [164]~P51(x1641)+P40(x1641) % 59.47/59.55 [165]~P43(x1651)+P44(x1651) % 59.47/59.55 [166]~P51(x1661)+P46(x1661) % 59.47/59.55 [167]~P50(x1671)+P51(x1671) % 59.47/59.55 [168]~P52(x1681)+P50(x1681) % 59.47/59.55 [169]~P53(x1691)+P52(x1691) % 59.47/59.55 [170]~P142(x1701)+P53(x1701) % 59.47/59.55 [171]~P53(x1711)+P77(x1711) % 59.47/59.55 [172]~P77(x1721)+P49(x1721) % 59.47/59.55 [173]~P63(x1731)+P55(x1731) % 59.47/59.55 [174]~P63(x1741)+P59(x1741) % 59.47/59.55 [175]~P68(x1751)+P63(x1751) % 59.47/59.55 [176]~P113(x1761)+P61(x1761) % 59.47/59.55 [177]~P121(x1771)+P61(x1771) % 59.47/59.55 [178]~P68(x1781)+P65(x1781) % 59.47/59.55 [179]~P73(x1791)+P68(x1791) % 59.47/59.55 [180]~P73(x1801)+P70(x1801) % 59.47/59.55 [181]~P142(x1811)+P73(x1811) % 59.47/59.55 [182]~P79(x1821)+P75(x1821) % 59.47/59.55 [183]~P85(x1831)+P75(x1831) % 59.47/59.55 [184]~P77(x1841)+P78(x1841) % 59.47/59.55 [185]~P79(x1851)+P80(x1851) % 59.47/59.55 [186]~P93(x1861)+P82(x1861) % 59.47/59.55 [187]~P85(x1871)+P86(x1871) % 59.47/59.55 [188]~P93(x1881)+P88(x1881) % 59.47/59.55 [189]~P92(x1891)+P93(x1891) % 59.47/59.55 [190]~P96(x1901)+P92(x1901) % 59.47/59.55 [191]~P141(x1911)+P94(x1911) % 59.47/59.55 [192]~P96(x1921)+P94(x1921) % 59.47/59.55 [193]~P112(x1931)+P96(x1931) % 59.47/59.55 [194]~P95(x1941)+P97(x1941) % 59.47/59.55 [195]~P109(x1951)+P99(x1951) % 59.47/59.55 [196]~P102(x1961)+P103(x1961) % 59.47/59.55 [197]~P109(x1971)+P105(x1971) % 59.47/59.55 [198]~P108(x1981)+P109(x1981) % 59.47/59.55 [199]~P112(x1991)+P108(x1991) % 59.47/59.55 [200]~P114(x2001)+P112(x2001) % 59.47/59.55 [201]~P141(x2011)+P111(x2011) % 59.47/59.55 [202]~P114(x2021)+P111(x2021) % 59.47/59.55 [203]~P131(x2031)+P114(x2031) % 59.47/59.55 [204]~P113(x2041)+P115(x2041) % 59.47/59.55 [205]~P128(x2051)+P117(x2051) % 59.47/59.55 [206]~P121(x2061)+P122(x2061) % 59.47/59.55 [207]~P128(x2071)+P124(x2071) % 59.47/59.55 [208]~P129(x2081)+P128(x2081) % 59.47/59.55 [209]~P131(x2091)+P129(x2091) % 59.47/59.55 [210]~P133(x2101)+P131(x2101) % 59.47/59.55 [211]~P141(x2111)+P130(x2111) % 59.47/59.55 [212]~P133(x2121)+P130(x2121) % 59.47/59.55 [213]~P134(x2131)+P133(x2131) % 59.47/59.55 [214]~P141(x2141)+P132(x2141) % 59.47/59.55 [215]~P134(x2151)+P132(x2151) % 59.47/59.55 [216]~P137(x2161)+P138(x2161) % 59.47/59.55 [217]~P146(x2171)+~P145(x2171) % 59.47/59.55 [297]P1(x2971)+~P143(a1,x2971) % 59.47/59.55 [298]P1(x2981)+~P143(a2,x2981) % 59.47/59.55 [299]P1(x2991)+~P143(a142,x2991) % 59.47/59.55 [300]P3(x3001)+~P143(a3,x3001) % 59.47/59.55 [301]P20(x3011)+~P143(a3,x3011) % 59.47/59.55 [302]P24(x3021)+~P143(a3,x3021) % 59.47/59.55 [303]P30(x3031)+~P143(a3,x3031) % 59.47/59.55 [304]P42(x3041)+~P143(a3,x3041) % 59.47/59.55 [305]P48(x3051)+~P143(a3,x3051) % 59.47/59.55 [306]P57(x3061)+~P143(a3,x3061) % 59.47/59.55 [307]P62(x3071)+~P143(a3,x3071) % 59.47/59.55 [308]P67(x3081)+~P143(a3,x3081) % 59.47/59.55 [309]P72(x3091)+~P143(a1,x3091) % 59.47/59.55 [310]P72(x3101)+~P143(a2,x3101) % 59.47/59.55 [311]P72(x3111)+~P143(a142,x3111) % 59.47/59.55 [312]P76(x3121)+~P143(a3,x3121) % 59.47/59.55 [313]P84(x3131)+~P143(a3,x3131) % 59.47/59.55 [314]P90(x3141)+~P143(a3,x3141) % 59.47/59.55 [315]P101(x3151)+~P143(a3,x3151) % 59.47/59.55 [316]P107(x3161)+~P143(a1,x3161) % 59.47/59.55 [317]P107(x3171)+~P143(a2,x3171) % 59.47/59.55 [318]P107(x3181)+~P143(a142,x3181) % 59.47/59.55 [319]P110(x3191)+~P143(a3,x3191) % 59.47/59.55 [320]P120(x3201)+~P143(a3,x3201) % 59.47/59.55 [321]P126(x3211)+~P143(a1,x3211) % 59.47/59.55 [322]P126(x3221)+~P143(a2,x3221) % 59.47/59.55 [323]P126(x3231)+~P143(a142,x3231) % 59.47/59.55 [324]P135(x3241)+~P143(a3,x3241) % 59.47/59.55 [218]~P39(x2181)+P4(f4(x2181)) % 59.47/59.55 [219]~P45(x2191)+P4(f66(x2191)) % 59.47/59.55 [220]~P69(x2201)+P4(f75(x2201)) % 59.47/59.55 [221]~P7(x2211)+P118(f76(x2211)) % 59.47/59.55 [222]~P54(x2221)+P118(f77(x2221)) % 59.47/59.55 [223]~P127(x2231)+P118(f5(x2231)) % 59.47/59.55 [224]~P139(x2241)+P118(f34(x2241)) % 59.47/59.55 [225]~P9(x2251)+P5(f104(x2251)) % 59.47/59.55 [226]~P18(x2261)+P136(f6(x2261)) % 59.47/59.55 [227]~P27(x2271)+P136(f39(x2271)) % 59.47/59.55 [228]~P58(x2281)+P136(f88(x2281)) % 59.47/59.55 [229]~P37(x2291)+P19(f58(x2291)) % 59.47/59.55 [230]~P87(x2301)+P19(f105(x2301)) % 59.47/59.55 [231]~P104(x2311)+P19(f7(x2311)) % 59.47/59.55 [232]~P123(x2321)+P19(f8(x2321)) % 59.47/59.55 [233]~P23(x2331)+P21(f40(x2331)) % 59.47/59.55 [234]~P29(x2341)+P25(f59(x2341)) % 59.47/59.55 [235]~P41(x2351)+P35(f67(x2351)) % 59.47/59.55 [236]~P47(x2361)+P43(f78(x2361)) % 59.47/59.55 [237]~P56(x2371)+P54(f89(x2371)) % 59.47/59.55 [238]~P60(x2381)+P58(f91(x2381)) % 59.47/59.55 [239]~P66(x2391)+P64(f94(x2391)) % 59.47/59.55 [240]~P64(x2401)+P61(f95(x2401)) % 59.47/59.55 [241]~P78(x2411)+P61(f106(x2411)) % 59.47/59.55 [242]~P71(x2421)+P69(f107(x2421)) % 59.47/59.55 [243]~P81(x2431)+P75(f116(x2431)) % 59.47/59.55 [244]~P91(x2441)+P75(f131(x2441)) % 59.47/59.55 [245]~P98(x2451)+P75(f133(x2451)) % 59.47/59.55 [246]~P116(x2461)+P75(f9(x2461)) % 59.47/59.55 [247]~P83(x2471)+P79(f118(x2471)) % 59.47/59.55 [248]~P89(x2481)+P85(f126(x2481)) % 59.47/59.55 [249]~P100(x2491)+P95(f135(x2491)) % 59.47/59.55 [250]~P106(x2501)+P102(f10(x2501)) % 59.47/59.55 [251]~P119(x2511)+P113(f21(x2511)) % 59.47/59.55 [252]~P125(x2521)+P121(f28(x2521)) % 59.47/59.55 [253]~P140(x2531)+P137(f41(x2531)) % 59.47/59.55 [325]P4(x3251)+P147(x3251,f65(x3251)) % 59.47/59.55 [326]P7(x3261)+P163(x3261,f79(x3261)) % 59.47/59.55 [327]P118(x3271)+P148(x3271,f15(x3271)) % 59.47/59.55 [328]P5(x3281)+P164(x3281,f110(x3281)) % 59.47/59.55 [329]P8(x3291)+P165(x3291,f19(x3291)) % 59.47/59.55 [330]P10(x3301)+P166(x3301,f45(x3301)) % 59.47/59.55 [331]P17(x3311)+P167(x3311,f47(x3311)) % 59.47/59.55 [332]P11(x3321)+P149(x3321,f50(x3321)) % 59.47/59.55 [333]P20(x3331)+P168(x3331,f51(x3331)) % 59.47/59.55 [334]P23(x3341)+P169(x3341,f54(x3341)) % 59.47/59.55 [335]P26(x3351)+P170(x3351,f60(x3351)) % 59.47/59.55 [336]P24(x3361)+P171(x3361,f61(x3361)) % 59.47/59.55 [337]P28(x3371)+P172(x3371,f63(x3371)) % 59.47/59.55 [338]P38(x3381)+P173(x3381,f68(x3381)) % 59.47/59.55 [339]P35(x3391)+P174(x3391,f70(x3391)) % 59.47/59.55 [340]P40(x3401)+P175(x3401,f72(x3401)) % 59.47/59.55 [341]P44(x3411)+P176(x3411,f80(x3411)) % 59.47/59.55 [342]P42(x3421)+P178(x3421,f81(x3421)) % 59.47/59.55 [343]P47(x3431)+P179(x3431,f83(x3431)) % 59.47/59.55 [344]P48(x3441)+P180(x3441,f86(x3441)) % 59.47/59.55 [345]P56(x3451)+P181(x3451,f87(x3451)) % 59.47/59.55 [346]P58(x3461)+P182(x3461,f92(x3461)) % 59.47/59.55 [347]P59(x3471)+P183(x3471,f96(x3471)) % 59.47/59.55 [348]P61(x3481)+P150(x3481,f112(x3481)) % 59.47/59.55 [349]P62(x3491)+P184(x3491,f99(x3491)) % 59.47/59.55 [350]P66(x3501)+P185(x3501,f101(x3501)) % 59.47/59.55 [351]P67(x3511)+P186(x3511,f108(x3511)) % 59.47/59.55 [352]P70(x3521)+P187(x3521,f111(x3521)) % 59.47/59.55 [353]P75(x3531)+P160(x3531,f114(x3531)) % 59.47/59.55 [354]P80(x3541)+P177(x3541,f119(x3541)) % 59.47/59.55 [355]P76(x3551)+P189(x3551,f120(x3551)) % 59.47/59.55 [356]P82(x3561)+P190(x3561,f123(x3561)) % 59.47/59.55 [357]P86(x3571)+P188(x3571,f127(x3571)) % 59.47/59.55 [358]P85(x3581)+P195(x3581,f128(x3581)) % 59.47/59.55 [359]P89(x3591)+P151(x3591,f129(x3591)) % 59.47/59.55 [360]P98(x3601)+P152(x3601,f134(x3601)) % 59.47/59.55 [361]P90(x3611)+P196(x3611,f136(x3611)) % 59.47/59.55 [362]P99(x3621)+P153(x3621,f140(x3621)) % 59.47/59.55 [363]P104(x3631)+P154(x3631,f11(x3631)) % 59.47/59.55 [364]P101(x3641)+P191(x3641,f12(x3641)) % 59.47/59.55 [365]P105(x3651)+P155(x3651,f16(x3651)) % 59.47/59.55 [366]P115(x3661)+P156(x3661,f22(x3661)) % 59.47/59.55 [367]P113(x3671)+P192(x3671,f23(x3671)) % 59.47/59.55 [368]P119(x3681)+P157(x3681,f25(x3681)) % 59.47/59.55 [369]P122(x3691)+P158(x3691,f29(x3691)) % 59.47/59.55 [370]P120(x3701)+P193(x3701,f30(x3701)) % 59.47/59.55 [371]P124(x3711)+P159(x3711,f32(x3711)) % 59.47/59.55 [372]P126(x3721)+P161(x3721,f35(x3721)) % 59.47/59.55 [373]P138(x3731)+P162(x3731,f42(x3731)) % 59.47/59.55 [374]P135(x3741)+P194(x3741,f43(x3741)) % 59.47/59.55 [425]~P1(x4251)+P147(x4251,f55(x4251)) % 59.47/59.55 [426]~P6(x4261)+P163(x4261,f100(x4261)) % 59.47/59.55 [427]~P7(x4271)+P143(x4271,f76(x4271)) % 59.47/59.55 [428]~P9(x4281)+P143(x4281,f104(x4281)) % 59.47/59.55 [429]~P18(x4291)+P143(x4291,f6(x4291)) % 59.47/59.55 [430]~P23(x4301)+P143(x4301,f40(x4301)) % 59.47/59.55 [431]~P27(x4311)+P143(x4311,f39(x4311)) % 59.47/59.55 [432]~P29(x4321)+P143(x4321,f59(x4321)) % 59.47/59.55 [433]~P37(x4331)+P143(x4331,f58(x4331)) % 59.47/59.55 [434]~P39(x4341)+P143(x4341,f4(x4341)) % 59.47/59.55 [435]~P41(x4351)+P143(x4351,f67(x4351)) % 59.47/59.55 [436]~P45(x4361)+P143(x4361,f66(x4361)) % 59.47/59.55 [437]~P47(x4371)+P143(x4371,f78(x4371)) % 59.47/59.55 [438]~P54(x4381)+P143(x4381,f77(x4381)) % 59.47/59.55 [439]~P56(x4391)+P143(x4391,f89(x4391)) % 59.47/59.55 [440]~P58(x4401)+P143(x4401,f88(x4401)) % 59.47/59.55 [441]~P60(x4411)+P143(x4411,f91(x4411)) % 59.47/59.55 [442]~P64(x4421)+P143(x4421,f95(x4421)) % 59.47/59.55 [443]~P66(x4431)+P143(x4431,f94(x4431)) % 59.47/59.55 [444]~P69(x4441)+P143(x4441,f75(x4441)) % 59.47/59.55 [445]~P71(x4451)+P143(x4451,f107(x4451)) % 59.47/59.55 [446]~P78(x4461)+P143(x4461,f106(x4461)) % 59.47/59.55 [447]~P81(x4471)+P143(x4471,f116(x4471)) % 59.47/59.55 [448]~P83(x4481)+P143(x4481,f118(x4481)) % 59.47/59.55 [449]~P87(x4491)+P143(x4491,f105(x4491)) % 59.47/59.55 [450]~P89(x4501)+P143(x4501,f126(x4501)) % 59.47/59.55 [451]~P91(x4511)+P143(x4511,f131(x4511)) % 59.47/59.55 [452]~P98(x4521)+P143(x4521,f133(x4521)) % 59.47/59.55 [453]~P100(x4531)+P143(x4531,f135(x4531)) % 59.47/59.55 [454]~P104(x4541)+P143(x4541,f7(x4541)) % 59.47/59.55 [455]~P106(x4551)+P143(x4551,f10(x4551)) % 59.47/59.55 [456]~P116(x4561)+P143(x4561,f9(x4561)) % 59.47/59.55 [457]~P119(x4571)+P143(x4571,f21(x4571)) % 59.47/59.55 [458]~P123(x4581)+P143(x4581,f8(x4581)) % 59.47/59.55 [459]~P125(x4591)+P143(x4591,f28(x4591)) % 59.47/59.55 [460]~P127(x4601)+P143(x4601,f5(x4601)) % 59.47/59.55 [461]~P139(x4611)+P143(x4611,f34(x4611)) % 59.47/59.55 [462]~P140(x4621)+P143(x4621,f41(x4621)) % 59.47/59.55 [463]~P3(x4631)+P164(x4631,f122(x4631)) % 59.47/59.55 [464]~P9(x4641)+P165(x4641,f141(x4641)) % 59.47/59.55 [465]~P18(x4651)+P167(x4651,f36(x4651)) % 59.47/59.55 [466]~P19(x4661)+P149(x4661,f52(x4661)) % 59.47/59.55 [467]~P21(x4671)+P168(x4671,f53(x4671)) % 59.47/59.55 [468]~P22(x4681)+P169(x4681,f56(x4681)) % 59.47/59.55 [469]~P27(x4691)+P170(x4691,f57(x4691)) % 59.47/59.55 [470]~P25(x4701)+P171(x4701,f62(x4701)) % 59.47/59.55 [471]~P29(x4711)+P172(x4711,f64(x4711)) % 59.47/59.55 [472]~P39(x4721)+P173(x4721,f69(x4721)) % 59.47/59.55 [473]~P30(x4731)+P174(x4731,f71(x4731)) % 59.47/59.55 [474]~P41(x4741)+P175(x4741,f73(x4741)) % 59.47/59.55 [475]~P45(x4751)+P176(x4751,f74(x4751)) % 59.47/59.55 [476]~P43(x4761)+P178(x4761,f82(x4761)) % 59.47/59.55 [477]~P46(x4771)+P179(x4771,f84(x4771)) % 59.47/59.55 [478]~P54(x4781)+P180(x4781,f85(x4781)) % 59.47/59.55 [479]~P55(x4791)+P181(x4791,f90(x4791)) % 59.47/59.55 [480]~P57(x4801)+P182(x4801,f93(x4801)) % 59.47/59.55 [481]~P60(x4811)+P183(x4811,f97(x4811)) % 59.47/59.55 [482]~P64(x4821)+P184(x4821,f98(x4821)) % 59.47/59.55 [483]~P65(x4831)+P185(x4831,f102(x4831)) % 59.47/59.55 [484]~P69(x4841)+P186(x4841,f103(x4841)) % 59.47/59.55 [485]~P71(x4851)+P187(x4851,f109(x4851)) % 59.47/59.55 [486]~P72(x4861)+P150(x4861,f113(x4861)) % 59.47/59.55 [487]~P74(x4871)+P160(x4871,f115(x4871)) % 59.47/59.55 [488]~P81(x4881)+P177(x4881,f117(x4881)) % 59.47/59.55 [489]~P79(x4891)+P189(x4891,f121(x4891)) % 59.47/59.55 [490]~P83(x4901)+P190(x4901,f124(x4901)) % 59.47/59.55 [491]~P87(x4911)+P188(x4911,f125(x4911)) % 59.47/59.55 [492]~P84(x4921)+P195(x4921,f130(x4921)) % 59.47/59.55 [493]~P88(x4931)+P151(x4931,f132(x4931)) % 59.47/59.55 [494]~P97(x4941)+P152(x4941,f137(x4941)) % 59.47/59.55 [495]~P95(x4951)+P196(x4951,f138(x4951)) % 59.47/59.55 [496]~P100(x4961)+P153(x4961,f139(x4961)) % 59.47/59.55 [497]~P103(x4971)+P154(x4971,f13(x4971)) % 59.47/59.55 [498]~P102(x4981)+P191(x4981,f14(x4981)) % 59.47/59.55 [499]~P106(x4991)+P155(x4991,f17(x4991)) % 59.47/59.55 [500]~P107(x5001)+P148(x5001,f18(x5001)) % 59.47/59.55 [501]~P116(x5011)+P156(x5011,f20(x5011)) % 59.47/59.55 [502]~P110(x5021)+P192(x5021,f24(x5021)) % 59.47/59.55 [503]~P117(x5031)+P157(x5031,f26(x5031)) % 59.47/59.55 [504]~P123(x5041)+P158(x5041,f27(x5041)) % 59.47/59.55 [505]~P121(x5051)+P193(x5051,f31(x5051)) % 59.47/59.55 [506]~P125(x5061)+P159(x5061,f33(x5061)) % 59.47/59.55 [507]~P136(x5071)+P161(x5071,f37(x5071)) % 59.47/59.55 [508]~P139(x5081)+P162(x5081,f38(x5081)) % 59.47/59.55 [509]~P137(x5091)+P194(x5091,f44(x5091)) % 59.47/59.55 [510]~P140(x5101)+P166(x5101,f46(x5101)) % 59.47/59.55 [375]P1(x3751)+~P147(x3751,x3752) % 59.47/59.55 [376]P6(x3761)+~P163(x3761,x3762) % 59.47/59.55 [377]P3(x3771)+~P164(x3771,x3772) % 59.47/59.55 [378]P9(x3781)+~P165(x3781,x3782) % 59.47/59.55 [379]P18(x3791)+~P167(x3791,x3792) % 59.47/59.55 [380]P136(x3801)+~P161(x3801,x3802) % 59.47/59.55 [381]P19(x3811)+~P149(x3811,x3812) % 59.47/59.55 [382]P21(x3821)+~P168(x3821,x3822) % 59.47/59.55 [383]P22(x3831)+~P169(x3831,x3832) % 59.47/59.55 [384]P27(x3841)+~P170(x3841,x3842) % 59.47/59.55 [385]P25(x3851)+~P171(x3851,x3852) % 59.47/59.55 [386]P29(x3861)+~P172(x3861,x3862) % 59.47/59.55 [387]P39(x3871)+~P173(x3871,x3872) % 59.47/59.55 [388]P30(x3881)+~P174(x3881,x3882) % 59.47/59.55 [389]P41(x3891)+~P175(x3891,x3892) % 59.47/59.55 [390]P45(x3901)+~P176(x3901,x3902) % 59.47/59.55 [391]P43(x3911)+~P178(x3911,x3912) % 59.47/59.55 [392]P46(x3921)+~P179(x3921,x3922) % 59.47/59.55 [393]P54(x3931)+~P180(x3931,x3932) % 59.47/59.55 [394]P55(x3941)+~P181(x3941,x3942) % 59.47/59.55 [395]P57(x3951)+~P182(x3951,x3952) % 59.47/59.55 [396]P60(x3961)+~P183(x3961,x3962) % 59.47/59.55 [397]P64(x3971)+~P184(x3971,x3972) % 59.47/59.55 [398]P65(x3981)+~P185(x3981,x3982) % 59.47/59.55 [399]P69(x3991)+~P186(x3991,x3992) % 59.47/59.55 [400]P71(x4001)+~P187(x4001,x4002) % 59.47/59.55 [401]P72(x4011)+~P150(x4011,x4012) % 59.47/59.55 [402]P74(x4021)+~P160(x4021,x4022) % 59.47/59.55 [403]P81(x4031)+~P177(x4031,x4032) % 59.47/59.55 [404]P79(x4041)+~P189(x4041,x4042) % 59.47/59.55 [405]P83(x4051)+~P190(x4051,x4052) % 59.47/59.55 [406]P87(x4061)+~P188(x4061,x4062) % 59.47/59.55 [407]P84(x4071)+~P195(x4071,x4072) % 59.47/59.55 [408]P88(x4081)+~P151(x4081,x4082) % 59.47/59.55 [409]P97(x4091)+~P152(x4091,x4092) % 59.47/59.55 [410]P95(x4101)+~P196(x4101,x4102) % 59.47/59.55 [411]P100(x4111)+~P153(x4111,x4112) % 59.47/59.55 [412]P103(x4121)+~P154(x4121,x4122) % 59.47/59.55 [413]P102(x4131)+~P191(x4131,x4132) % 59.47/59.55 [414]P106(x4141)+~P155(x4141,x4142) % 59.47/59.55 [415]P107(x4151)+~P148(x4151,x4152) % 59.47/59.55 [416]P116(x4161)+~P156(x4161,x4162) % 59.47/59.55 [417]P110(x4171)+~P192(x4171,x4172) % 59.47/59.55 [418]P117(x4181)+~P157(x4181,x4182) % 59.47/59.55 [419]P123(x4191)+~P158(x4191,x4192) % 59.47/59.55 [420]P121(x4201)+~P193(x4201,x4202) % 59.47/59.55 [421]P125(x4211)+~P159(x4211,x4212) % 59.47/59.55 [422]P139(x4221)+~P162(x4221,x4222) % 59.47/59.55 [423]P137(x4231)+~P194(x4231,x4232) % 59.47/59.55 [424]P140(x4241)+~P166(x4241,x4242) % 59.47/59.55 [511]~P4(x5111)+~P147(x5111,x5112) % 59.47/59.55 [512]~P7(x5121)+~P163(x5121,x5122) % 59.47/59.55 [513]~P118(x5131)+~P148(x5131,x5132) % 59.47/59.55 [514]~P5(x5141)+~P164(x5141,x5142) % 59.47/59.55 [515]~P8(x5151)+~P165(x5151,x5152) % 59.47/59.55 [516]~P10(x5161)+~P166(x5161,x5162) % 59.47/59.55 [517]~P17(x5171)+~P167(x5171,x5172) % 59.47/59.55 [518]~P11(x5181)+~P149(x5181,x5182) % 59.47/59.55 [519]~P20(x5191)+~P168(x5191,x5192) % 59.47/59.55 [520]~P23(x5201)+~P169(x5201,x5202) % 59.47/59.55 [521]~P26(x5211)+~P170(x5211,x5212) % 59.47/59.55 [522]~P24(x5221)+~P171(x5221,x5222) % 59.47/59.55 [523]~P28(x5231)+~P172(x5231,x5232) % 59.47/59.55 [524]~P38(x5241)+~P173(x5241,x5242) % 59.47/59.55 [525]~P35(x5251)+~P174(x5251,x5252) % 59.47/59.55 [526]~P40(x5261)+~P175(x5261,x5262) % 59.47/59.55 [527]~P44(x5271)+~P176(x5271,x5272) % 59.47/59.55 [528]~P42(x5281)+~P178(x5281,x5282) % 59.47/59.55 [529]~P47(x5291)+~P179(x5291,x5292) % 59.47/59.55 [530]~P48(x5301)+~P180(x5301,x5302) % 59.47/59.55 [531]~P56(x5311)+~P181(x5311,x5312) % 59.47/59.55 [532]~P58(x5321)+~P182(x5321,x5322) % 59.47/59.55 [533]~P59(x5331)+~P183(x5331,x5332) % 59.47/59.55 [534]~P61(x5341)+~P150(x5341,x5342) % 59.47/59.55 [535]~P62(x5351)+~P184(x5351,x5352) % 59.47/59.55 [536]~P66(x5361)+~P185(x5361,x5362) % 59.47/59.55 [537]~P67(x5371)+~P186(x5371,x5372) % 59.47/59.55 [538]~P70(x5381)+~P187(x5381,x5382) % 59.47/59.55 [539]~P75(x5391)+~P160(x5391,x5392) % 59.47/59.55 [540]~P80(x5401)+~P177(x5401,x5402) % 59.47/59.55 [541]~P76(x5411)+~P189(x5411,x5412) % 59.47/59.55 [542]~P82(x5421)+~P190(x5421,x5422) % 59.47/59.55 [543]~P86(x5431)+~P188(x5431,x5432) % 59.47/59.55 [544]~P85(x5441)+~P195(x5441,x5442) % 59.47/59.55 [545]~P89(x5451)+~P151(x5451,x5452) % 59.47/59.55 [546]~P98(x5461)+~P152(x5461,x5462) % 59.47/59.55 [547]~P90(x5471)+~P196(x5471,x5472) % 59.47/59.55 [548]~P99(x5481)+~P153(x5481,x5482) % 59.47/59.55 [549]~P104(x5491)+~P154(x5491,x5492) % 59.47/59.55 [550]~P101(x5501)+~P191(x5501,x5502) % 59.47/59.55 [551]~P105(x5511)+~P155(x5511,x5512) % 59.47/59.55 [552]~P115(x5521)+~P156(x5521,x5522) % 59.47/59.55 [553]~P113(x5531)+~P192(x5531,x5532) % 59.47/59.55 [554]~P119(x5541)+~P157(x5541,x5542) % 59.47/59.55 [555]~P122(x5551)+~P158(x5551,x5552) % 59.47/59.55 [556]~P120(x5561)+~P193(x5561,x5562) % 59.47/59.55 [557]~P124(x5571)+~P159(x5571,x5572) % 59.47/59.55 [558]~P126(x5581)+~P161(x5581,x5582) % 59.47/59.55 [559]~P138(x5591)+~P162(x5591,x5592) % 59.47/59.55 [560]~P135(x5601)+~P194(x5601,x5602) % 59.47/59.55 [254]~P127(x2541)+~P91(x2541)+P2(x2541) % 59.47/59.55 [255]~P4(x2551)+~P6(x2551)+P5(x2551) % 59.47/59.55 [256]~P8(x2561)+~P10(x2561)+P12(x2561) % 59.47/59.55 [257]~P12(x2571)+~P141(x2571)+P13(x2571) % 59.47/59.55 [258]~P13(x2581)+~P134(x2581)+P14(x2581) % 59.47/59.55 [259]~P133(x2591)+~P132(x2591)+P134(x2591) % 59.47/59.55 [260]~P14(x2601)+~P15(x2601)+P16(x2601) % 59.47/59.55 [261]~P136(x2611)+~P17(x2611)+P21(x2611) % 59.47/59.55 [262]~P4(x2621)+~P26(x2621)+P25(x2621) % 59.47/59.55 [263]~P22(x2631)+~P28(x2631)+P32(x2631) % 59.47/59.55 [264]~P141(x2641)+~P32(x2641)+P31(x2641) % 59.47/59.55 [265]~P16(x2651)+~P31(x2651)+P34(x2651) % 59.47/59.55 [266]~P34(x2661)+~P33(x2661)+P36(x2661) % 59.47/59.55 [267]~P136(x2671)+~P38(x2671)+P35(x2671) % 59.47/59.55 [268]~P4(x2681)+~P44(x2681)+P43(x2681) % 59.47/59.55 [269]~P40(x2691)+~P46(x2691)+P51(x2691) % 59.47/59.55 [270]~P141(x2701)+~P51(x2701)+P50(x2701) % 59.47/59.55 [271]~P36(x2711)+~P50(x2711)+P52(x2711) % 59.47/59.55 [272]~P52(x2721)+~P77(x2721)+P53(x2721) % 59.47/59.55 [273]~P49(x2731)+~P78(x2731)+P77(x2731) % 59.47/59.55 [274]~P2(x2741)+~P37(x2741)+P49(x2741) % 59.47/59.55 [275]~P55(x2751)+~P59(x2751)+P63(x2751) % 59.47/59.55 [276]~P63(x2761)+~P65(x2761)+P68(x2761) % 59.47/59.55 [277]~P68(x2771)+~P70(x2771)+P73(x2771) % 59.47/59.55 [278]~P75(x2781)+~P80(x2781)+P79(x2781) % 59.47/59.55 [279]~P75(x2791)+~P86(x2791)+P85(x2791) % 59.47/59.55 [280]~P82(x2801)+~P88(x2801)+P93(x2801) % 59.47/59.55 [281]~P141(x2811)+~P93(x2811)+P92(x2811) % 59.47/59.55 [282]~P92(x2821)+~P94(x2821)+P96(x2821) % 59.47/59.55 [283]~P19(x2831)+~P97(x2831)+P95(x2831) % 59.47/59.55 [284]~P19(x2841)+~P103(x2841)+P102(x2841) % 59.47/59.55 [285]~P99(x2851)+~P105(x2851)+P109(x2851) % 59.47/59.55 [286]~P141(x2861)+~P109(x2861)+P108(x2861) % 59.47/59.55 [287]~P96(x2871)+~P108(x2871)+P112(x2871) % 59.47/59.55 [288]~P112(x2881)+~P111(x2881)+P114(x2881) % 59.47/59.55 [289]~P61(x2891)+~P115(x2891)+P113(x2891) % 59.47/59.55 [290]~P61(x2901)+~P122(x2901)+P121(x2901) % 59.47/59.55 [291]~P117(x2911)+~P124(x2911)+P128(x2911) % 59.47/59.55 [292]~P141(x2921)+~P128(x2921)+P129(x2921) % 59.47/59.55 [293]~P114(x2931)+~P129(x2931)+P131(x2931) % 59.47/59.55 [294]~P131(x2941)+~P130(x2941)+P133(x2941) % 59.47/59.55 [295]~P136(x2951)+~P138(x2951)+P137(x2951) % 59.47/59.55 [296]~P53(x2961)+~P73(x2961)+P142(x2961) % 59.47/59.55 [561]~P143(x5611,x5612)+P127(x5611)+~P118(x5612) % 59.47/59.55 [562]~P143(x5621,x5622)+P91(x5621)+~P75(x5622) % 59.47/59.55 [563]~P143(x5631,x5632)+P7(x5631)+~P118(x5632) % 59.47/59.55 [564]~P143(x5641,x5642)+P9(x5641)+~P5(x5642) % 59.47/59.55 [565]~P143(x5651,x5652)+P18(x5651)+~P136(x5652) % 59.47/59.55 [566]~P143(x5661,x5662)+P23(x5661)+~P21(x5662) % 59.47/59.55 [567]~P143(x5671,x5672)+P27(x5671)+~P136(x5672) % 59.47/59.55 [568]~P143(x5681,x5682)+P29(x5681)+~P25(x5682) % 59.47/59.55 [569]~P143(x5691,x5692)+P37(x5691)+~P19(x5692) % 59.47/59.55 [570]~P143(x5701,x5702)+P39(x5701)+~P4(x5702) % 59.47/59.55 [571]~P143(x5711,x5712)+P41(x5711)+~P35(x5712) % 59.47/59.55 [572]~P143(x5721,x5722)+P45(x5721)+~P4(x5722) % 59.47/59.55 [573]~P143(x5731,x5732)+P47(x5731)+~P43(x5732) % 59.47/59.55 [574]~P143(x5741,x5742)+P54(x5741)+~P118(x5742) % 59.47/59.55 [575]~P143(x5751,x5752)+P56(x5751)+~P54(x5752) % 59.47/59.55 [576]~P143(x5761,x5762)+P58(x5761)+~P136(x5762) % 59.47/59.55 [577]~P143(x5771,x5772)+P60(x5771)+~P58(x5772) % 59.47/59.55 [578]~P143(x5781,x5782)+P64(x5781)+~P61(x5782) % 59.47/59.55 [579]~P143(x5791,x5792)+P66(x5791)+~P64(x5792) % 59.47/59.55 [580]~P143(x5801,x5802)+P69(x5801)+~P4(x5802) % 59.47/59.55 [581]~P143(x5811,x5812)+P71(x5811)+~P69(x5812) % 59.47/59.55 [582]~P143(x5821,x5822)+P78(x5821)+~P61(x5822) % 59.47/59.55 [583]~P143(x5831,x5832)+P81(x5831)+~P75(x5832) % 59.47/59.55 [584]~P143(x5841,x5842)+P83(x5841)+~P79(x5842) % 59.47/59.55 [585]~P143(x5851,x5852)+P87(x5851)+~P19(x5852) % 59.47/59.55 [586]~P143(x5861,x5862)+P89(x5861)+~P85(x5862) % 59.47/59.55 [587]~P143(x5871,x5872)+P98(x5871)+~P75(x5872) % 59.47/59.55 [588]~P143(x5881,x5882)+P100(x5881)+~P95(x5882) % 59.47/59.55 [589]~P143(x5891,x5892)+P104(x5891)+~P19(x5892) % 59.47/59.55 [590]~P143(x5901,x5902)+P106(x5901)+~P102(x5902) % 59.47/59.55 [591]~P143(x5911,x5912)+P116(x5911)+~P75(x5912) % 59.47/59.55 [592]~P143(x5921,x5922)+P119(x5921)+~P113(x5922) % 59.47/59.55 [593]~P143(x5931,x5932)+P123(x5931)+~P19(x5932) % 59.47/59.55 [594]~P143(x5941,x5942)+P125(x5941)+~P121(x5942) % 59.47/59.55 [595]~P143(x5951,x5952)+P139(x5951)+~P118(x5952) % 59.47/59.55 [596]~P143(x5961,x5962)+P140(x5961)+~P137(x5962) % 59.47/59.55 [597]P144(a48)+P145(a49)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P12(a3)+~P13(a3)+~P14(a3)+~P134(a3)+~P15(a3)+~P16(a3)+~P32(a3)+~P31(a3)+~P34(a3)+~P33(a3)+~P36(a3)+~P37(a3)+~P51(a3)+~P50(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P63(a3)+~P68(a3)+~P73(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P93(a3)+~P92(a3)+~P94(a3)+~P96(a3)+~P98(a142)+~P104(a142)+~P109(a3)+~P108(a3)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P128(a3)+~P129(a3)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3) % 59.47/59.56 [598]P144(a48)+P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P12(a3)+~P13(a3)+~P14(a3)+~P134(a3)+~P15(a3)+~P16(a3)+~P32(a3)+~P31(a3)+~P34(a3)+~P33(a3)+~P36(a3)+~P37(a3)+~P51(a3)+~P50(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P63(a3)+~P68(a3)+~P73(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P93(a3)+~P92(a3)+~P94(a3)+~P96(a3)+~P98(a142)+~P104(a142)+~P109(a3)+~P108(a3)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P128(a3)+~P129(a3)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3) % 59.47/59.56 %EqnAxiom % 59.47/59.56 % 59.47/59.56 %------------------------------------------- % 59.47/59.56 cnf(603,plain, % 59.47/59.56 (P20(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301])). % 59.47/59.56 cnf(605,plain, % 59.47/59.56 (P24(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302])). % 59.47/59.56 cnf(609,plain, % 59.47/59.56 (P42(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304])). % 59.47/59.56 cnf(611,plain, % 59.47/59.56 (P48(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305])). % 59.47/59.56 cnf(615,plain, % 59.47/59.56 (P62(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307])). % 59.47/59.56 cnf(617,plain, % 59.47/59.56 (P67(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308])). % 59.47/59.56 cnf(621,plain, % 59.47/59.56 (P76(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312])). % 59.47/59.56 cnf(625,plain, % 59.47/59.56 (P90(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314])). % 59.47/59.56 cnf(627,plain, % 59.47/59.56 (P101(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315])). % 59.47/59.56 cnf(633,plain, % 59.47/59.56 (P120(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320])). % 59.47/59.56 cnf(635,plain, % 59.47/59.56 (P126(a149)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321])). % 59.47/59.56 cnf(637,plain, % 59.47/59.56 (P135(a143)), % 59.47/59.56 inference(scs_inference,[],[109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324])). % 59.47/59.56 cnf(663,plain, % 59.47/59.56 (~P9(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464])). % 59.47/59.56 cnf(665,plain, % 59.47/59.56 (~P29(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471])). % 59.47/59.56 cnf(667,plain, % 59.47/59.56 (~P41(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474])). % 59.47/59.56 cnf(669,plain, % 59.47/59.56 (~P60(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481])). % 59.47/59.56 cnf(671,plain, % 59.47/59.56 (~P71(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485])). % 59.47/59.56 cnf(677,plain, % 59.47/59.56 (~P83(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490])). % 59.47/59.56 cnf(679,plain, % 59.47/59.56 (~P100(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496])). % 59.47/59.56 cnf(681,plain, % 59.47/59.56 (~P106(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499])). % 59.47/59.56 cnf(683,plain, % 59.47/59.56 (~P125(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506])). % 59.47/59.56 cnf(685,plain, % 59.47/59.56 (~P140(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510])). % 59.47/59.56 cnf(723,plain, % 59.47/59.56 (~P121(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505])). % 59.47/59.56 cnf(729,plain, % 59.47/59.56 (P12(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,27,31,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256])). % 59.47/59.56 cnf(731,plain, % 59.47/59.56 (P13(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,27,31,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257])). % 59.47/59.56 cnf(733,plain, % 59.47/59.56 (P32(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263])). % 59.47/59.56 cnf(735,plain, % 59.47/59.56 (P31(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264])). % 59.47/59.56 cnf(737,plain, % 59.47/59.56 (P51(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269])). % 59.47/59.56 cnf(739,plain, % 59.47/59.56 (P50(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270])). % 59.47/59.56 cnf(741,plain, % 59.47/59.56 (P63(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275])). % 59.47/59.56 cnf(743,plain, % 59.47/59.56 (P68(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276])). % 59.47/59.56 cnf(745,plain, % 59.47/59.56 (P73(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277])). % 59.47/59.56 cnf(747,plain, % 59.47/59.56 (P93(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280])). % 59.47/59.56 cnf(749,plain, % 59.47/59.56 (P92(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281])). % 59.47/59.56 cnf(751,plain, % 59.47/59.56 (P109(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285])). % 59.47/59.56 cnf(753,plain, % 59.47/59.56 (P108(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286])). % 59.47/59.56 cnf(755,plain, % 59.47/59.56 (P128(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291])). % 59.47/59.56 cnf(757,plain, % 59.47/59.56 (P129(a3)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292])). % 59.47/59.56 cnf(759,plain, % 59.47/59.56 (~P5(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564])). % 59.47/59.56 cnf(761,plain, % 59.47/59.56 (~P35(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571])). % 59.47/59.56 cnf(763,plain, % 59.47/59.56 (~P58(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577])). % 59.47/59.56 cnf(765,plain, % 59.47/59.56 (~P69(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581])). % 59.47/59.56 cnf(773,plain, % 59.47/59.56 (~P64(a1)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581,584,466,478,482])). % 59.47/59.56 cnf(777,plain, % 59.47/59.56 (~P118(a148)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,111,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581,584,466,478,482,265,574])). % 59.47/59.56 cnf(785,plain, % 59.47/59.56 (~P5(a148)), % 59.47/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,111,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581,584,466,478,482,265,574,576,578,580,122])). % 59.47/59.56 cnf(793,plain, % 59.47/59.56 (~P35(a148)), % 59.60/59.56 inference(scs_inference,[],[12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,111,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581,584,466,478,482,265,574,576,578,580,122,123,124,147,148])). % 59.60/59.56 cnf(822,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P96(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P15(a3)+P145(a49)+~P33(a3)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P133(a3)+~P98(a142)+~P104(a142)+~P111(a3)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[117,12,13,14,23,27,31,35,39,43,44,48,52,62,69,73,77,81,90,94,107,109,111,112,15,20,24,32,36,45,49,66,74,78,91,95,103,297,300,301,302,303,304,305,306,307,308,309,312,313,314,315,316,319,320,321,324,515,516,523,526,533,534,538,539,542,548,551,557,464,471,474,481,485,486,487,490,496,499,506,510,518,519,522,528,530,535,537,541,547,550,556,558,560,467,470,476,495,498,505,507,509,256,257,263,264,269,270,275,276,277,280,281,285,286,291,292,564,571,577,581,584,466,478,482,265,574,576,578,580,122,123,124,147,148,149,380,382,385,391,423,333,336,342,374,271,287,293,597])). % 59.60/59.56 cnf(823,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P15(a3)+~P16(a3)+~P34(a3)+~P33(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P96(a3)+~P98(a142)+~P104(a142)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[117,729,731,733,735,737,739,741,743,745,747,749,751,753,755,757,598])). % 59.60/59.56 cnf(876,plain, % 59.60/59.56 (~P79(a2)), % 59.60/59.56 inference(scs_inference,[],[63,108,603,605,609,611,615,617,621,625,627,633,635,637,665,677,679,681,683,685,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584])). % 59.60/59.56 cnf(880,plain, % 59.60/59.56 (~P69(a2)), % 59.60/59.56 inference(scs_inference,[],[63,108,603,605,609,611,615,617,621,625,627,633,635,637,665,667,671,677,679,681,683,685,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581])). % 59.60/59.56 cnf(886,plain, % 59.60/59.56 (~P58(a2)), % 59.60/59.56 inference(scs_inference,[],[63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577])). % 59.60/59.56 cnf(916,plain, % 59.60/59.56 (~P137(a149)), % 59.60/59.56 inference(scs_inference,[],[63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149])). % 59.60/59.56 cnf(922,plain, % 59.60/59.56 (~P168(a149,x9221)), % 59.60/59.56 inference(scs_inference,[],[63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149,509,498,382])). % 59.60/59.56 cnf(924,plain, % 59.60/59.56 (~P118(x9241)+~P143(a143,x9241)), % 59.60/59.56 inference(scs_inference,[],[63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149,509,498,382,574])). % 59.60/59.56 cnf(926,plain, % 59.60/59.56 (~P4(a144)), % 59.60/59.56 inference(scs_inference,[],[113,63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149,509,498,382,574,580])). % 59.60/59.56 cnf(928,plain, % 59.60/59.56 (~P136(a144)), % 59.60/59.56 inference(scs_inference,[],[113,63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149,509,498,382,574,580,576])). % 59.60/59.56 cnf(930,plain, % 59.60/59.56 (~P127(x9301)+~P143(a143,f5(x9301))), % 59.60/59.56 inference(scs_inference,[],[113,63,108,44,603,605,609,611,615,617,621,625,627,633,635,637,663,665,667,669,671,677,679,681,683,685,773,16,556,530,518,539,558,522,519,537,528,467,535,550,478,547,560,505,487,541,507,147,466,568,588,590,594,596,584,571,581,578,564,577,399,404,410,413,420,484,489,385,482,476,495,423,470,148,149,509,498,382,574,580,576,223])). % 59.60/59.56 cnf(974,plain, % 59.60/59.56 (~P137(a144)), % 59.60/59.56 inference(scs_inference,[],[64,926,928,916,26,33,37,93,96,124,423,374,558,530,391,522,539,556,122,342,528,148,149])). % 59.60/59.56 cnf(982,plain, % 59.60/59.56 (~P54(a2)), % 59.60/59.56 inference(scs_inference,[],[64,926,928,916,21,26,33,37,93,96,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478])). % 59.60/59.56 cnf(1011,plain, % 59.60/59.56 (~P95(a142)), % 59.60/59.56 inference(scs_inference,[],[110,64,926,928,665,679,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588])). % 59.60/59.56 cnf(1015,plain, % 59.60/59.56 (~P102(a142)), % 59.60/59.56 inference(scs_inference,[],[110,64,926,928,665,679,681,685,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590])). % 59.60/59.56 cnf(1017,plain, % 59.60/59.56 (~P118(a145)), % 59.60/59.56 inference(scs_inference,[],[110,114,64,926,928,665,679,681,685,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574])). % 59.60/59.56 cnf(1021,plain, % 59.60/59.56 (~P69(a142)), % 59.60/59.56 inference(scs_inference,[],[110,114,64,926,928,665,667,671,679,681,685,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574,571,581])). % 59.60/59.56 cnf(1029,plain, % 59.60/59.56 (~P4(a145)), % 59.60/59.56 inference(scs_inference,[],[110,114,44,64,880,926,928,663,665,667,671,677,679,681,685,773,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574,571,581,584,564,578,580])). % 59.60/59.56 cnf(1031,plain, % 59.60/59.56 (~P136(a145)), % 59.60/59.56 inference(scs_inference,[],[110,114,44,64,880,886,926,928,663,665,667,671,677,679,681,685,773,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574,571,581,584,564,578,580,576])). % 59.60/59.56 cnf(1033,plain, % 59.60/59.56 (~P58(a142)), % 59.60/59.56 inference(scs_inference,[],[110,114,44,64,880,886,926,928,663,665,667,669,671,677,679,681,685,773,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574,571,581,584,564,578,580,576,577])). % 59.60/59.56 cnf(1043,plain, % 59.60/59.56 (~P168(a144,x10431)), % 59.60/59.56 inference(scs_inference,[],[110,114,44,64,880,886,926,928,663,665,667,669,671,677,679,681,685,773,922,916,21,26,33,37,46,51,68,76,80,93,96,105,124,423,374,558,530,391,522,539,556,122,342,528,148,149,519,380,507,478,333,547,123,541,505,537,487,560,535,550,467,147,568,588,596,590,574,571,581,584,564,578,580,576,577,385,482,476,336,382])). % 59.60/59.56 cnf(1100,plain, % 59.60/59.56 (~P64(a142)), % 59.60/59.56 inference(scs_inference,[],[115,113,44,65,1021,1029,1031,1033,773,1043,974,982,22,34,38,47,97,124,423,530,558,148,149,374,333,539,528,478,380,122,519,507,467,487,123,535,147,382,574,578,580,576,385,391,482])). % 59.60/59.56 cnf(1244,plain, % 59.60/59.56 (P127(x12441)+~P49(x12441)), % 59.60/59.56 inference(scs_inference,[],[119,120])). % 59.60/59.56 cnf(1275,plain, % 59.60/59.56 (~P2(x12751)+P75(f131(x12751))), % 59.60/59.56 inference(scs_inference,[],[121,244])). % 59.60/59.56 cnf(1458,plain, % 59.60/59.56 (P15(a3)), % 59.60/59.56 inference(scs_inference,[],[731,130,144])). % 59.60/59.56 cnf(1459,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P96(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P33(a3)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P133(a3)+~P98(a142)+~P104(a142)+~P111(a3)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1458,822])). % 59.60/59.56 cnf(1460,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P33(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P96(a3)+~P98(a142)+~P104(a142)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1458,823])). % 59.60/59.56 cnf(1492,plain, % 59.60/59.56 (P33(a3)), % 59.60/59.56 inference(scs_inference,[],[1458,131,159])). % 59.60/59.56 cnf(1493,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P96(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P133(a3)+~P98(a142)+~P104(a142)+~P111(a3)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1492,1459])). % 59.60/59.56 cnf(1494,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P94(a3)+~P96(a3)+~P98(a142)+~P104(a142)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1492,1460])). % 59.60/59.56 cnf(1526,plain, % 59.60/59.56 (P94(a3)), % 59.60/59.56 inference(scs_inference,[],[735,132,191])). % 59.60/59.56 cnf(1527,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P96(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P133(a3)+~P98(a142)+~P104(a142)+~P111(a3)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1526,1493])). % 59.60/59.56 cnf(1528,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P96(a3)+~P98(a142)+~P104(a142)+~P112(a3)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1526,1494])). % 59.60/59.56 cnf(1529,plain, % 59.60/59.56 (P96(a3)), % 59.60/59.56 inference(scs_inference,[],[749,1526,282])). % 59.60/59.56 cnf(1531,plain, % 59.60/59.56 (P112(a3)), % 59.60/59.56 inference(scs_inference,[],[753,749,1526,282,287])). % 59.60/59.56 cnf(1537,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P133(a3)+~P98(a142)+~P104(a142)+~P111(a3)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1529,1527])). % 59.60/59.56 cnf(1538,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P111(a3)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1529,1531,1528])). % 59.60/59.56 cnf(1557,plain, % 59.60/59.56 (P111(a3)), % 59.60/59.56 inference(scs_inference,[],[1492,133,201])). % 59.60/59.56 cnf(1558,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P114(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P133(a3)+~P98(a142)+~P104(a142)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1557,1537])). % 59.60/59.56 cnf(1559,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P114(a3)+~P116(a1)+~P123(a1)+~P131(a3)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1557,1538])). % 59.60/59.56 cnf(1560,plain, % 59.60/59.56 (P114(a3)), % 59.60/59.56 inference(scs_inference,[],[1531,1557,288])). % 59.60/59.56 cnf(1562,plain, % 59.60/59.56 (P131(a3)), % 59.60/59.56 inference(scs_inference,[],[757,1531,1557,288,293])). % 59.60/59.56 cnf(1568,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P133(a3)+~P98(a142)+~P104(a142)+~P130(a3)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1560,1558])). % 59.60/59.56 cnf(1569,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)+~P130(a3)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1560,1562,1559])). % 59.60/59.56 cnf(1588,plain, % 59.60/59.56 (P130(a3)), % 59.60/59.56 inference(scs_inference,[],[739,134,211])). % 59.60/59.56 cnf(1589,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P133(a3)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1588,1568])). % 59.60/59.56 cnf(1590,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)+~P133(a3)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1588,1569])). % 59.60/59.56 cnf(1591,plain, % 59.60/59.56 (P133(a3)), % 59.60/59.56 inference(scs_inference,[],[1562,1588,294])). % 59.60/59.56 cnf(1597,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P132(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1591,1589])). % 59.60/59.56 cnf(1598,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)+~P132(a3)), % 59.60/59.56 inference(scs_inference,[],[1591,1590])). % 59.60/59.56 cnf(1617,plain, % 59.60/59.56 (P132(a3)), % 59.60/59.56 inference(scs_inference,[],[749,135,214])). % 59.60/59.56 cnf(1618,plain, % 59.60/59.56 (~P16(a3)+~P36(a3)+~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+P145(a49)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1617,1597])). % 59.60/59.56 cnf(1619,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P14(a3)+~P134(a3)+~P16(a3)+~P34(a3)+~P36(a3)+~P37(a3)+~P52(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1617,1598])). % 59.60/59.56 cnf(1620,plain, % 59.60/59.56 (P134(a3)), % 59.60/59.56 inference(scs_inference,[],[1591,1617,259])). % 59.60/59.56 cnf(1624,plain, % 59.60/59.56 (P14(a3)), % 59.60/59.56 inference(scs_inference,[],[1591,1617,731,44,773,259,578,258])). % 59.60/59.56 cnf(1626,plain, % 59.60/59.56 (P16(a3)), % 59.60/59.56 inference(scs_inference,[],[1458,1591,1617,731,44,773,259,578,258,260])). % 59.60/59.56 cnf(1628,plain, % 59.60/59.56 (P34(a3)), % 59.60/59.56 inference(scs_inference,[],[735,1458,1591,1617,731,44,773,259,578,258,260,265])). % 59.60/59.56 cnf(1630,plain, % 59.60/59.56 (P36(a3)), % 59.60/59.56 inference(scs_inference,[],[735,1458,1492,1591,1617,731,44,773,259,578,258,260,265,266])). % 59.60/59.56 cnf(1632,plain, % 59.60/59.56 (P52(a3)), % 59.60/59.56 inference(scs_inference,[],[735,739,1458,1492,1591,1617,731,44,773,259,578,258,260,265,266,271])). % 59.60/59.56 cnf(1636,plain, % 59.60/59.56 (~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+P145(a49)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1626,1630,1624,1620,1618])). % 59.60/59.56 cnf(1637,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P37(a3)+~P53(a3)+~P77(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[1624,1620,1626,1628,1630,1632,1619])). % 59.60/59.56 cnf(2047,plain, % 59.60/59.56 (P169(a3,f56(a3))), % 59.60/59.56 inference(scs_inference,[],[733,153,468])). % 59.60/59.56 cnf(2289,plain, % 59.60/59.56 (~P49(x22891)+P19(f58(x22891))), % 59.60/59.56 inference(scs_inference,[],[162,229])). % 59.60/59.56 cnf(2412,plain, % 59.60/59.56 (P179(a3,f84(a3))), % 59.60/59.56 inference(scs_inference,[],[737,166,477])). % 59.60/59.56 cnf(2534,plain, % 59.60/59.56 (P77(a3)), % 59.60/59.56 inference(scs_inference,[],[106,170,171])). % 59.60/59.56 cnf(2535,plain, % 59.60/59.56 (~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+P145(a49)+~P37(a3)+~P53(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2534,1636])). % 59.60/59.56 cnf(2536,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P37(a3)+~P53(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2534,1637])). % 59.60/59.56 cnf(2537,plain, % 59.60/59.56 (P53(a3)), % 59.60/59.56 inference(scs_inference,[],[1632,2534,272])). % 59.60/59.56 cnf(2543,plain, % 59.60/59.56 (~P146(a49)+~P2(a3)+~P127(a3)+~P91(a3)+P145(a49)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2537,2535])). % 59.60/59.56 cnf(2544,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P2(a3)+~P127(a3)+~P91(a3)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2537,2536])). % 59.60/59.56 cnf(2563,plain, % 59.60/59.56 (P2(a3)), % 59.60/59.56 inference(scs_inference,[],[2534,172,119])). % 59.60/59.56 cnf(2564,plain, % 59.60/59.56 (~P146(a49)+~P127(a3)+~P91(a3)+P145(a49)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2563,2543])). % 59.60/59.56 cnf(2565,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P127(a3)+~P91(a3)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[2563,2544])). % 59.60/59.56 cnf(2592,plain, % 59.60/59.56 (P181(a3,f90(a3))), % 59.60/59.56 inference(scs_inference,[],[741,173,479])). % 59.60/59.56 cnf(2683,plain, % 59.60/59.56 (~P113(a148)), % 59.60/59.56 inference(scs_inference,[],[773,111,176,578])). % 59.60/59.56 cnf(2684,plain, % 59.60/59.56 (~P4(a149)), % 59.60/59.56 inference(scs_inference,[],[112,765,580])). % 59.60/59.56 cnf(2767,plain, % 59.60/59.56 (P185(a3,f102(a3))), % 59.60/59.56 inference(scs_inference,[],[743,178,483])). % 59.60/59.56 cnf(2950,plain, % 59.60/59.56 (P61(f106(a3))), % 59.60/59.56 inference(scs_inference,[],[2534,184,241])). % 59.60/59.56 cnf(2953,plain, % 59.60/59.56 (~P72(f106(a3))), % 59.60/59.56 inference(scs_inference,[],[2950,534,486])). % 59.60/59.56 cnf(2985,plain, % 59.60/59.56 (~P79(x29851)+~P177(x29851,x29852)), % 59.60/59.56 inference(scs_inference,[],[185,540])). % 59.60/59.56 cnf(3046,plain, % 59.60/59.56 (~P85(x30461)+~P188(x30461,x30462)), % 59.60/59.56 inference(scs_inference,[],[187,543])). % 59.60/59.56 cnf(3077,plain, % 59.60/59.56 (P151(a3,f132(a3))), % 59.60/59.56 inference(scs_inference,[],[747,188,493])). % 59.60/59.56 cnf(3500,plain, % 59.60/59.56 (~P113(x35001)+~P156(x35001,x35002)), % 59.60/59.56 inference(scs_inference,[],[204,552])). % 59.60/59.56 cnf(3531,plain, % 59.60/59.56 (P157(a3,f26(a3))), % 59.60/59.56 inference(scs_inference,[],[755,205,503])). % 59.60/59.56 cnf(3803,plain, % 59.60/59.56 (~P137(x38031)+~P162(x38031,x38032)), % 59.60/59.56 inference(scs_inference,[],[216,559])). % 59.60/59.56 cnf(3864,plain, % 59.60/59.56 (P127(a3)), % 59.60/59.56 inference(scs_inference,[],[2534,1244,172])). % 59.60/59.56 cnf(3865,plain, % 59.60/59.56 (~P146(a49)+~P91(a3)+P145(a49)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[3864,2564])). % 59.60/59.56 cnf(3866,plain, % 59.60/59.56 (P146(a49)+~P145(a49)+~P91(a3)+~P37(a3)+~P49(a3)+~P78(a3)+~P81(a2)+~P87(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)), % 59.60/59.56 inference(scs_inference,[],[3864,2565])). % 59.60/59.56 cnf(4294,plain, % 59.60/59.56 (~P158(x42941,x42942)+P19(f8(x42941))), % 59.60/59.56 inference(scs_inference,[],[232,419])). % 59.60/59.56 cnf(4480,plain, % 59.60/59.56 (P61(f95(a3))), % 59.60/59.56 inference(scs_inference,[],[44,107,240,578])). % 59.60/59.56 cnf(4483,plain, % 59.60/59.56 (~P72(f95(a3))), % 59.60/59.56 inference(scs_inference,[],[4480,534,486])). % 59.60/59.56 cnf(4899,plain, % 59.60/59.56 (P150(a145,f113(a145))), % 59.60/59.56 inference(scs_inference,[],[114,310,486])). % 59.60/59.56 cnf(5605,plain, % 59.60/59.56 (~P177(x56051,x56052)+P75(f116(x56051))), % 59.60/59.56 inference(scs_inference,[],[403,243])). % 59.60/59.56 cnf(5821,plain, % 59.60/59.56 (~P156(x58211,x58212)+P75(f9(x58211))), % 59.60/59.56 inference(scs_inference,[],[416,246])). % 59.60/59.56 cnf(5852,plain, % 59.60/59.56 (~P192(x58521,x58522)+P192(x58521,f24(x58521))), % 59.60/59.56 inference(scs_inference,[],[417,502])). % 59.60/59.56 cnf(5976,plain, % 59.60/59.56 (~P148(f5(a3),x59761)), % 59.60/59.56 inference(scs_inference,[],[3864,513,223])). % 59.60/59.56 cnf(5977,plain, % 59.60/59.56 (P118(f5(a3))), % 59.60/59.56 inference(scs_inference,[],[5976,327])). % 59.60/59.56 cnf(5978,plain, % 59.60/59.56 (~P148(f5(a3),x59781)), % 59.60/59.56 inference(rename_variables,[],[5976])). % 59.60/59.56 cnf(5980,plain, % 59.60/59.56 (~P107(f5(a3))), % 59.60/59.56 inference(scs_inference,[],[5976,5978,327,500])). % 59.60/59.56 cnf(6104,plain, % 59.60/59.56 (P169(a3,f54(a3))), % 59.60/59.56 inference(scs_inference,[],[2047,520,334])). % 59.60/59.56 cnf(6226,plain, % 59.60/59.56 (P179(a3,f83(a3))), % 59.60/59.56 inference(scs_inference,[],[2412,529,343])). % 59.60/59.56 cnf(6287,plain, % 59.60/59.56 (P181(a3,f87(a3))), % 59.60/59.56 inference(scs_inference,[],[2592,531,345])). % 59.60/59.56 cnf(6409,plain, % 59.60/59.56 (P185(a3,f101(a3))), % 59.60/59.56 inference(scs_inference,[],[2767,536,350])). % 59.60/59.56 cnf(6531,plain, % 59.60/59.56 (P151(a3,f129(a3))), % 59.60/59.56 inference(scs_inference,[],[3077,545,359])). % 59.60/59.56 cnf(6592,plain, % 59.60/59.56 (~P152(a1,x65921)), % 59.60/59.56 inference(scs_inference,[],[65,111,546,587])). % 59.60/59.56 cnf(6593,plain, % 59.60/59.56 (P98(a1)), % 59.60/59.56 inference(scs_inference,[],[6592,360])). % 59.60/59.56 cnf(6781,plain, % 59.60/59.56 (P157(a3,f25(a3))), % 59.60/59.56 inference(scs_inference,[],[3531,554,368])). % 59.60/59.56 cnf(6964,plain, % 59.60/59.56 (~P160(f131(a3),x69641)), % 59.60/59.56 inference(scs_inference,[],[2563,1275,539])). % 59.60/59.56 cnf(6965,plain, % 59.60/59.56 (P75(f131(a3))), % 59.60/59.56 inference(scs_inference,[],[6964,353])). % 59.60/59.56 cnf(7580,plain, % 59.60/59.56 (~P156(x75801,x75802)+P192(x75801,f23(x75801))), % 59.60/59.56 inference(scs_inference,[],[3500,367])). % 59.60/59.56 cnf(7833,plain, % 59.60/59.56 (P91(a3)), % 59.60/59.56 inference(scs_inference,[],[2563,121])). % 59.60/59.56 cnf(7835,plain, % 59.60/59.56 (P49(a3)), % 59.60/59.56 inference(scs_inference,[],[2563,2534,121,172])). % 59.60/59.56 cnf(7837,plain, % 59.60/59.56 (P78(a3)), % 59.60/59.56 inference(scs_inference,[],[2563,2534,121,172,184])). % 59.60/59.56 cnf(7843,plain, % 59.60/59.56 (~P56(a3)), % 59.60/59.56 inference(scs_inference,[],[6104,6226,6287,2563,2534,121,172,184,520,529,531])). % 59.60/59.56 cnf(7851,plain, % 59.60/59.56 (P75(f133(a1))), % 59.60/59.56 inference(scs_inference,[],[6593,6104,6226,6287,6409,6531,6781,2563,2534,121,172,184,520,529,531,536,545,554,245])). % 59.60/59.56 cnf(7873,plain, % 59.60/59.56 (P143(a1,f133(a1))), % 59.60/59.56 inference(scs_inference,[],[1,759,761,2683,2684,6593,6104,6226,6287,6409,6531,6781,763,2563,2534,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452])). % 59.60/59.56 cnf(7911,plain, % 59.60/59.56 (P150(a2,f113(a2))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6104,6226,6287,6409,6531,6781,763,2563,3864,2534,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486])). % 59.60/59.56 cnf(7923,plain, % 59.60/59.56 (P91(a2)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6104,6226,6287,6409,6531,6781,723,876,1011,1015,763,17,2563,3864,62,63,2534,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562])). % 59.60/59.56 cnf(7931,plain, % 59.60/59.56 (P87(a2)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,763,17,2563,3864,62,63,2534,114,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585])). % 59.60/59.56 cnf(7933,plain, % 59.60/59.56 (P98(a3)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,763,17,2563,3864,62,63,2534,114,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587])). % 59.60/59.56 cnf(7943,plain, % 59.60/59.56 (~P61(a146)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578])). % 59.60/59.56 cnf(7945,plain, % 59.60/59.56 (P54(a3)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574])). % 59.60/59.56 cnf(7947,plain, % 59.60/59.56 (P37(a3)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162])). % 59.60/59.56 cnf(7951,plain, % 59.60/59.56 (~P4(a1)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511])). % 59.60/59.56 cnf(7955,plain, % 59.60/59.56 (~P113(a1)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553])). % 59.60/59.56 cnf(7957,plain, % 59.60/59.56 (P118(f76(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221])). % 59.60/59.56 cnf(7975,plain, % 59.60/59.56 (P177(a2,f119(a2))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354])). % 59.60/59.56 cnf(7979,plain, % 59.60/59.56 (P158(a1,f29(a1))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369])). % 59.60/59.56 cnf(7999,plain, % 59.60/59.56 (P177(a3,f117(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488])). % 59.60/59.56 cnf(8001,plain, % 59.60/59.56 (P188(a2,f125(a2))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491])). % 59.60/59.56 cnf(8003,plain, % 59.60/59.56 (P156(a3,f20(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501])). % 59.60/59.56 cnf(8005,plain, % 59.60/59.56 (P158(a2,f27(a2))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504])). % 59.60/59.56 cnf(8007,plain, % 59.60/59.56 (P162(a3,f38(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508])). % 59.60/59.56 cnf(8013,plain, % 59.60/59.56 (P192(a3,f23(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580])). % 59.60/59.56 cnf(8019,plain, % 59.60/59.56 (~P11(a145)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518])). % 59.60/59.56 cnf(8021,plain, % 59.60/59.56 (P180(a3,f85(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518,478])). % 59.60/59.56 cnf(8025,plain, % 59.60/59.56 (~P115(a1)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518,478,279,289])). % 59.60/59.56 cnf(8035,plain, % 59.60/59.56 (~P85(a142)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,62,63,2534,114,115,113,110,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518,478,279,289,566,573,575,579,586])). % 59.60/59.56 cnf(8045,plain, % 59.60/59.56 (~P121(f106(a3))), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,683,62,63,765,665,681,2534,114,115,113,110,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518,478,279,289,566,573,575,579,586,592,580,568,590,594])). % 59.60/59.56 cnf(8059,plain, % 59.60/59.56 (~P58(a143)), % 59.60/59.56 inference(scs_inference,[],[1,9,18,28,40,53,60,70,83,87,759,761,777,2683,2684,6593,4899,2953,5980,6965,6104,6226,6287,6409,6531,6781,723,876,1011,1015,1100,763,17,2563,3864,683,62,63,765,663,677,665,667,671,679,681,685,669,2534,114,115,113,110,109,44,5977,121,172,184,520,529,531,536,545,554,245,924,2289,325,328,339,346,367,425,446,451,452,460,463,473,480,492,502,5852,310,311,317,318,327,316,309,487,500,534,466,486,539,278,283,284,290,562,563,569,583,585,587,589,591,593,595,578,574,162,417,511,544,553,221,222,224,229,230,231,232,244,246,354,358,369,427,433,438,447,449,454,456,458,461,488,491,501,504,508,4294,5605,7580,348,353,518,478,279,289,566,573,575,579,586,592,580,568,590,594,581,596,571,588,584,564,577])). % 59.60/59.56 cnf(8100,plain, % 59.60/59.56 (P145(a49)+~P81(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)+~P146(a49)), % 59.60/59.56 inference(scs_inference,[],[7947,7835,7837,7931,7833,3865])). % 59.60/59.56 cnf(8101,plain, % 59.60/59.56 (~P81(a2)+~P98(a142)+~P104(a142)+~P116(a1)+~P123(a1)+~P145(a49)+P146(a49)), % 59.60/59.56 inference(scs_inference,[],[7833,7947,7835,7837,7931,3866])). % 59.60/59.56 cnf(8110,plain, % 59.60/59.56 (P123(a1)), % 59.60/59.56 inference(scs_inference,[],[785,7951,7979,8003,3864,930,328,325,3500,419])). % 59.60/59.56 cnf(8182,plain, % 59.60/59.56 (P81(a2)), % 59.60/59.56 inference(scs_inference,[],[2,10,29,41,71,88,785,793,7923,7933,7943,7947,7951,7955,8025,8035,8059,4483,7957,7975,7979,7999,8001,8003,8005,8007,8013,3864,5980,930,328,325,3500,419,504,311,559,5852,552,417,317,463,3803,3046,245,543,346,451,425,452,924,473,318,433,366,2985,458,357,492,480,540,555,339,310,316,358,348,367,502,403])). % 59.60/59.56 cnf(8210,plain, % 59.60/59.56 (P104(a142)), % 59.60/59.56 inference(scs_inference,[],[2,10,19,29,41,54,61,71,84,88,785,793,1017,7923,7933,7943,7947,7951,7955,8019,8025,8035,8059,4483,7957,7911,7975,7979,7999,8001,8003,8005,8007,8013,8021,3864,5980,116,930,328,325,3500,419,504,311,559,5852,552,417,317,463,3803,3046,245,543,346,451,425,452,924,473,318,433,366,2985,458,357,492,480,540,555,339,310,316,358,348,367,502,403,5821,373,332,309,327,487,500,534,466,530,486,539,593,589])). % 59.60/59.56 cnf(8214,plain, % 59.60/59.56 (P116(a1)), % 59.60/59.56 inference(scs_inference,[],[2,10,19,29,41,54,61,71,84,88,785,793,1017,7843,7923,7933,7943,7945,7947,7951,7955,8019,8025,8035,8059,4483,7851,7957,7873,7911,7975,7979,7999,8001,8003,8005,8007,8013,8021,3864,5980,116,930,328,325,3500,419,504,311,559,5852,552,417,317,463,3803,3046,245,543,346,451,425,452,924,473,318,433,366,2985,458,357,492,480,540,555,339,310,316,358,348,367,502,403,5821,373,332,309,327,487,500,534,466,530,486,539,593,589,575,591])). % 59.60/59.56 cnf(8222,plain, % 59.60/59.56 (P98(a142)), % 59.60/59.56 inference(scs_inference,[],[2,10,19,29,41,54,61,71,84,88,785,793,1017,7843,7923,7933,7943,7945,7947,7951,7955,8019,8025,8035,8059,4483,7851,7957,8045,7873,7911,7975,7979,7999,8001,8003,8005,8007,8013,8021,2950,3864,64,5980,116,115,930,328,325,3500,419,504,311,559,5852,552,417,317,463,3803,3046,245,543,346,451,425,452,924,473,318,433,366,2985,458,357,492,480,540,555,339,310,316,358,348,367,502,403,5821,373,332,309,327,487,500,534,466,530,486,539,593,589,575,591,569,562,290,587])). % 59.60/59.56 cnf(8442,plain, % 59.60/59.56 (~P146(a49)+P145(a49)), % 59.60/59.56 inference(scs_inference,[],[8210,8214,8110,8222,8182,8100])). % 59.60/59.56 cnf(8443,plain, % 59.60/59.56 (~P145(a49)+P146(a49)), % 59.60/59.56 inference(scs_inference,[],[8214,8110,8210,8222,8182,8101])). % 59.60/59.56 cnf(8814,plain, % 59.60/59.56 (~P146(a49)), % 59.60/59.56 inference(scs_inference,[],[8442,217])). % 59.60/59.56 cnf(8815,plain, % 59.60/59.56 (~P145(a49)), % 59.60/59.56 inference(scs_inference,[],[8814,8443])). % 59.60/59.56 cnf(8816,plain, % 59.60/59.56 (P145(a49)), % 59.60/59.56 inference(scs_inference,[],[8814,118])). % 59.60/59.56 cnf(8844,plain, % 59.60/59.56 ($false), % 59.60/59.56 inference(scs_inference,[],[8815,8816]), % 59.60/59.56 ['proof']). % 59.60/59.57 % SZS output end Proof % 59.60/59.57 % Total time :58.830000s %------------------------------------------------------------------------------