%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS157+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n005.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 1.32s 1.37s % Output : CNFRefutation 1.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.11 % Problem : KRS157+1 : TPTP v8.2.0. Released v3.1.0. % 0.02/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n005.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Wed Jun 19 14:02:53 EDT 2024 % 0.10/0.32 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 1.22/1.33 %------------------------------------------- % 1.22/1.33 % File :CSE---1.7 % 1.22/1.33 % Problem :theBenchmark % 1.22/1.33 % Transform :cnf % 1.22/1.33 % Format :tptp:raw % 1.22/1.33 % Command :java -jar mcs_scs.jar %d %s % 1.22/1.33 % 1.22/1.33 % Result :Theorem 0.660000s % 1.22/1.33 % Output :CNFRefutation 0.660000s % 1.22/1.33 %------------------------------------------- % 1.22/1.34 %------------------------------------------------------------------------------ % 1.22/1.34 % File : KRS157+1 : TPTP v8.2.0. Released v3.1.0. % 1.22/1.34 % Domain : Knowledge Representation (Semantic Web) % 1.22/1.34 % Problem : ABox test from DL98 systems comparison % 1.22/1.34 % Version : Especial. % 1.22/1.34 % English : % 1.22/1.34 % 1.22/1.34 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.22/1.34 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.22/1.34 % Source : [Bec03] % 1.22/1.34 % Names : positive_description-logic-Manifest664 [Bec03] % 1.22/1.34 % 1.22/1.34 % Status : Theorem % 1.22/1.34 % Rating : 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.11 v4.0.0, 0.10 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.08 v3.3.0, 0.11 v3.1.0 % 1.22/1.34 % Syntax : Number of formulae : 220 ( 12 unt; 0 def) % 1.22/1.34 % Number of atoms : 544 ( 0 equ) % 1.22/1.34 % Maximal formula atoms : 12 ( 2 avg) % 1.22/1.34 % Number of connectives : 375 ( 51 ~; 0 |; 117 &) % 1.22/1.34 % ( 202 <=>; 5 =>; 0 <=; 0 <~>) % 1.22/1.34 % Maximal formula depth : 10 ( 4 avg) % 1.22/1.34 % Maximal term depth : 1 ( 1 avg) % 1.22/1.34 % Number of predicates : 209 ( 209 usr; 0 prp; 1-2 aty) % 1.22/1.34 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 1.22/1.34 % Number of variables : 357 ( 209 !; 148 ?) % 1.22/1.34 % SPC : FOF_THM_RFO_NEQ % 1.22/1.34 % 1.22/1.34 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.22/1.34 % datatypes, so this problem may not be perfect. At least it's % 1.22/1.34 % still representative of the type of reasoning required for OWL. % 1.22/1.34 %------------------------------------------------------------------------------ % 1.22/1.34 %----Thing and Nothing % 1.22/1.34 fof(axiom_0,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cowlThing(X) % 1.22/1.34 & ~ cowlNothing(X) ) ). % 1.22/1.34 % 1.22/1.34 %----String and Integer disjoint % 1.22/1.34 fof(axiom_1,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( xsd_string(X) % 1.22/1.34 <=> ~ xsd_integer(X) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC10 % 1.22/1.34 fof(axiom_2,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC10(X) % 1.22/1.34 <=> ? [Y0] : ra_Px87(X,Y0) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC10 % 1.22/1.34 fof(axiom_3,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC10(X) % 1.22/1.34 <=> ( cC2xcomp(X) % 1.22/1.34 & cC8xcomp(X) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC10xcomp % 1.22/1.34 fof(axiom_4,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC10xcomp(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px87(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC100 % 1.22/1.34 fof(axiom_5,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC100(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC98xcomp(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC100 % 1.22/1.34 fof(axiom_6,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC100(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px76(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC100xcomp % 1.22/1.34 fof(axiom_7,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC100xcomp(X) % 1.22/1.34 <=> ? [Y0] : ra_Px76(X,Y0) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC102 % 1.22/1.34 fof(axiom_8,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC102(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC16xcomp(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC104 % 1.22/1.34 fof(axiom_9,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC104(X) % 1.22/1.34 <=> ( cC16(X) % 1.22/1.34 & cC102(X) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC106 % 1.22/1.34 fof(axiom_10,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC106(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC104(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC106 % 1.22/1.34 fof(axiom_11,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC106(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px37(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC106xcomp % 1.22/1.34 fof(axiom_12,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC106xcomp(X) % 1.22/1.34 <=> ? [Y0] : ra_Px37(X,Y0) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC108 % 1.22/1.34 fof(axiom_13,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC108(X) % 1.22/1.34 <=> ( cC16xcomp(X) % 1.22/1.34 & cC106xcomp(X) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC108 % 1.22/1.34 fof(axiom_14,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC108(X) % 1.22/1.34 <=> ? [Y0] : ra_Px45(X,Y0) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC108xcomp % 1.22/1.34 fof(axiom_15,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC108xcomp(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px45(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC110 % 1.22/1.34 fof(axiom_16,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC110(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC16xcomp(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC112 % 1.22/1.34 fof(axiom_17,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC112(X) % 1.22/1.34 <=> ( cC16(X) % 1.22/1.34 & cC110(X) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC114 % 1.22/1.34 fof(axiom_18,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC114(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC112(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC114 % 1.22/1.34 fof(axiom_19,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC114(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px40(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC114xcomp % 1.22/1.34 fof(axiom_20,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC114xcomp(X) % 1.22/1.34 <=> ? [Y0] : ra_Px40(X,Y0) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC116 % 1.22/1.34 fof(axiom_21,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC116(X) % 1.22/1.34 <=> ( cC16xcomp(X) % 1.22/1.34 & cC114xcomp(X) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC118 % 1.22/1.34 fof(axiom_22,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC118(X) % 1.22/1.34 <=> ? [Y] : % 1.22/1.34 ( rR1(X,Y) % 1.22/1.34 & cC116(Y) ) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC12 % 1.22/1.34 fof(axiom_23,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC12(X) % 1.22/1.34 <=> ~ ? [Y] : ra_Px4(X,Y) ) ). % 1.22/1.34 % 1.22/1.34 %----Equality cC12 % 1.22/1.34 fof(axiom_24,axiom, % 1.22/1.34 ! [X] : % 1.22/1.34 ( cC12(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC10(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC12xcomp % 1.22/1.35 fof(axiom_25,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC12xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px4(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC120 % 1.22/1.35 fof(axiom_26,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC120(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC118(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC122 % 1.22/1.35 fof(axiom_27,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC122(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC16xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC124 % 1.22/1.35 fof(axiom_28,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC124(X) % 1.22/1.35 <=> ( cC16(X) % 1.22/1.35 & cC122(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC126 % 1.22/1.35 fof(axiom_29,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC126(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px43(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC126 % 1.22/1.35 fof(axiom_30,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC126(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC124(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC126xcomp % 1.22/1.35 fof(axiom_31,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC126xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px43(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC128 % 1.22/1.35 fof(axiom_32,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC128(X) % 1.22/1.35 <=> ( cC16xcomp(X) % 1.22/1.35 & cC126xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC130 % 1.22/1.35 fof(axiom_33,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC130(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC128(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC130 % 1.22/1.35 fof(axiom_34,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC130(X) % 1.22/1.35 <=> ? [Y0] : ra_Px44(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC130xcomp % 1.22/1.35 fof(axiom_35,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC130xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px44(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC132 % 1.22/1.35 fof(axiom_36,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC132(X) % 1.22/1.35 <=> ( cC120(X) % 1.22/1.35 & cC130xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC132 % 1.22/1.35 fof(axiom_37,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC132(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px46(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC132xcomp % 1.22/1.35 fof(axiom_38,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC132xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px46(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC134 % 1.22/1.35 fof(axiom_39,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC134(X) % 1.22/1.35 <=> ? [Y0] : ra_Px72(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC134 % 1.22/1.35 fof(axiom_40,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC134(X) % 1.22/1.35 <=> ( cC132xcomp(X) % 1.22/1.35 & cC108xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC134xcomp % 1.22/1.35 fof(axiom_41,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC134xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px72(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC136 % 1.22/1.35 fof(axiom_42,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC136(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC16xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC138 % 1.22/1.35 fof(axiom_43,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC138(X) % 1.22/1.35 <=> ( cC16(X) % 1.22/1.35 & cC136(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC14 % 1.22/1.35 fof(axiom_44,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC14(X) % 1.22/1.35 <=> ( cC2xcomp(X) % 1.22/1.35 & cC12xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC140 % 1.22/1.35 fof(axiom_45,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC140(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC138(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC140 % 1.22/1.35 fof(axiom_46,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC140(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px49(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC140xcomp % 1.22/1.35 fof(axiom_47,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC140xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px49(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC142 % 1.22/1.35 fof(axiom_48,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC142(X) % 1.22/1.35 <=> ( cC16xcomp(X) % 1.22/1.35 & cC140xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC142 % 1.22/1.35 fof(axiom_49,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC142(X) % 1.22/1.35 <=> ? [Y0] : ra_Px57(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC142xcomp % 1.22/1.35 fof(axiom_50,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC142xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px57(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC144 % 1.22/1.35 fof(axiom_51,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC144(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC16xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC146 % 1.22/1.35 fof(axiom_52,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC146(X) % 1.22/1.35 <=> ( cC144(X) % 1.22/1.35 & cC16(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC148 % 1.22/1.35 fof(axiom_53,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC148(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px52(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC148 % 1.22/1.35 fof(axiom_54,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC148(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC146(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC148xcomp % 1.22/1.35 fof(axiom_55,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC148xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px52(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC150 % 1.22/1.35 fof(axiom_56,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC150(X) % 1.22/1.35 <=> ( cC16xcomp(X) % 1.22/1.35 & cC148xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC152 % 1.22/1.35 fof(axiom_57,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC152(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC150(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC154 % 1.22/1.35 fof(axiom_58,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC154(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC152(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC156 % 1.22/1.35 fof(axiom_59,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC156(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC16xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC158 % 1.22/1.35 fof(axiom_60,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC158(X) % 1.22/1.35 <=> ( cC16(X) % 1.22/1.35 & cC156(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC16 % 1.22/1.35 fof(axiom_61,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC16(X) % 1.22/1.35 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC16xcomp % 1.22/1.35 fof(axiom_62,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC16xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC160 % 1.22/1.35 fof(axiom_63,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC160(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px55(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC160 % 1.22/1.35 fof(axiom_64,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC160(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC158(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC160xcomp % 1.22/1.35 fof(axiom_65,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC160xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px55(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC162 % 1.22/1.35 fof(axiom_66,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC162(X) % 1.22/1.35 <=> ( cC16xcomp(X) % 1.22/1.35 & cC160xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC164 % 1.22/1.35 fof(axiom_67,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC164(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC162(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC164 % 1.22/1.35 fof(axiom_68,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC164(X) % 1.22/1.35 <=> ? [Y0] : ra_Px56(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC164xcomp % 1.22/1.35 fof(axiom_69,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC164xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px56(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC166 % 1.22/1.35 fof(axiom_70,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC166(X) % 1.22/1.35 <=> ( cC164xcomp(X) % 1.22/1.35 & cC154(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC166 % 1.22/1.35 fof(axiom_71,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC166(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px58(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC166xcomp % 1.22/1.35 fof(axiom_72,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC166xcomp(X) % 1.22/1.35 <=> ? [Y0] : ra_Px58(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC168 % 1.22/1.35 fof(axiom_73,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC168(X) % 1.22/1.35 <=> ( cC142xcomp(X) % 1.22/1.35 & cC166xcomp(X) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC168 % 1.22/1.35 fof(axiom_74,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC168(X) % 1.22/1.35 <=> ? [Y0] : ra_Px59(X,Y0) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC168xcomp % 1.22/1.35 fof(axiom_75,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC168xcomp(X) % 1.22/1.35 <=> ~ ? [Y] : ra_Px59(X,Y) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC170 % 1.22/1.35 fof(axiom_76,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC170(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC168xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC172 % 1.22/1.35 fof(axiom_77,axiom, % 1.22/1.35 ! [X] : % 1.22/1.35 ( cC172(X) % 1.22/1.35 <=> ? [Y] : % 1.22/1.35 ( rR1(X,Y) % 1.22/1.35 & cC16xcomp(Y) ) ) ). % 1.22/1.35 % 1.22/1.35 %----Equality cC174 % 1.22/1.35 fof(axiom_78,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC174(X) % 1.22/1.36 <=> ( cC16(X) % 1.22/1.36 & cC172(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC176 % 1.22/1.36 fof(axiom_79,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC176(X) % 1.22/1.36 <=> ? [Y0] : ra_Px62(X,Y0) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC176 % 1.22/1.36 fof(axiom_80,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC176(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC174(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC176xcomp % 1.22/1.36 fof(axiom_81,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC176xcomp(X) % 1.22/1.36 <=> ~ ? [Y] : ra_Px62(X,Y) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC178 % 1.22/1.36 fof(axiom_82,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC178(X) % 1.22/1.36 <=> ~ ? [Y] : ra_Px70(X,Y) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC178 % 1.22/1.36 fof(axiom_83,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC178(X) % 1.22/1.36 <=> ( cC16xcomp(X) % 1.22/1.36 & cC176xcomp(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC178xcomp % 1.22/1.36 fof(axiom_84,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC178xcomp(X) % 1.22/1.36 <=> ? [Y0] : ra_Px70(X,Y0) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC18 % 1.22/1.36 fof(axiom_85,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC18(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC16xcomp(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC180 % 1.22/1.36 fof(axiom_86,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC180(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC16xcomp(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC182 % 1.22/1.36 fof(axiom_87,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC182(X) % 1.22/1.36 <=> ( cC16(X) % 1.22/1.36 & cC180(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC184 % 1.22/1.36 fof(axiom_88,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC184(X) % 1.22/1.36 <=> ? [Y0] : ra_Px65(X,Y0) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC184 % 1.22/1.36 fof(axiom_89,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC184(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC182(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC184xcomp % 1.22/1.36 fof(axiom_90,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC184xcomp(X) % 1.22/1.36 <=> ~ ? [Y] : ra_Px65(X,Y) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC186 % 1.22/1.36 fof(axiom_91,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC186(X) % 1.22/1.36 <=> ( cC16xcomp(X) % 1.22/1.36 & cC184xcomp(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC188 % 1.22/1.36 fof(axiom_92,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC188(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC186(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC190 % 1.22/1.36 fof(axiom_93,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC190(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC188(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC192 % 1.22/1.36 fof(axiom_94,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC192(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC16xcomp(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC194 % 1.22/1.36 fof(axiom_95,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC194(X) % 1.22/1.36 <=> ( cC16(X) % 1.22/1.36 & cC192(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC196 % 1.22/1.36 fof(axiom_96,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC196(X) % 1.22/1.36 <=> ? [Y0] : ra_Px68(X,Y0) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC196 % 1.22/1.36 fof(axiom_97,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC196(X) % 1.22/1.36 <=> ? [Y] : % 1.22/1.36 ( rR1(X,Y) % 1.22/1.36 & cC194(Y) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC196xcomp % 1.22/1.36 fof(axiom_98,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC196xcomp(X) % 1.22/1.36 <=> ~ ? [Y] : ra_Px68(X,Y) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC198 % 1.22/1.36 fof(axiom_99,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC198(X) % 1.22/1.36 <=> ( cC16xcomp(X) % 1.22/1.36 & cC196xcomp(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC2 % 1.22/1.36 fof(axiom_100,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC2(X) % 1.22/1.36 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC2xcomp % 1.22/1.36 fof(axiom_101,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC2xcomp(X) % 1.22/1.36 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC20 % 1.22/1.36 fof(axiom_102,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC20(X) % 1.22/1.36 <=> ( cC18(X) % 1.22/1.36 & cC16(X) ) ) ). % 1.22/1.36 % 1.22/1.36 %----Equality cC200 % 1.22/1.36 fof(axiom_103,axiom, % 1.22/1.36 ! [X] : % 1.22/1.36 ( cC200(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC198(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC200 % 1.32/1.36 fof(axiom_104,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC200(X) % 1.32/1.36 <=> ? [Y0] : ra_Px69(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC200xcomp % 1.32/1.36 fof(axiom_105,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC200xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px69(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC202 % 1.32/1.36 fof(axiom_106,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC202(X) % 1.32/1.36 <=> ( cC200xcomp(X) % 1.32/1.36 & cC190(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC202 % 1.32/1.36 fof(axiom_107,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC202(X) % 1.32/1.36 <=> ? [Y0] : ra_Px71(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC202xcomp % 1.32/1.36 fof(axiom_108,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC202xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px71(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC204 % 1.32/1.36 fof(axiom_109,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC204(X) % 1.32/1.36 <=> ( cC202xcomp(X) % 1.32/1.36 & cC178xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC206 % 1.32/1.36 fof(axiom_110,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC206(X) % 1.32/1.36 <=> ( cC204(X) % 1.32/1.36 & cC170(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC208 % 1.32/1.36 fof(axiom_111,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC208(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC206(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC208 % 1.32/1.36 fof(axiom_112,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC208(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px73(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC208xcomp % 1.32/1.36 fof(axiom_113,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC208xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px73(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC210 % 1.32/1.36 fof(axiom_114,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC210(X) % 1.32/1.36 <=> ( cC134xcomp(X) % 1.32/1.36 & cC208xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC212 % 1.32/1.36 fof(axiom_115,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC212(X) % 1.32/1.36 <=> ? [Y0] : ra_Px74(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC212 % 1.32/1.36 fof(axiom_116,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC212(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC210(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC212xcomp % 1.32/1.36 fof(axiom_117,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC212xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px74(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC214 % 1.32/1.36 fof(axiom_118,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC214(X) % 1.32/1.36 <=> ? [Y0] : ra_Px75(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC214 % 1.32/1.36 fof(axiom_119,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC214(X) % 1.32/1.36 <=> ( cC212xcomp(X) % 1.32/1.36 & cC100(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC214xcomp % 1.32/1.36 fof(axiom_120,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC214xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px75(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC216 % 1.32/1.36 fof(axiom_121,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC216(X) % 1.32/1.36 <=> ( cC64(X) % 1.32/1.36 & cC214xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC22 % 1.32/1.36 fof(axiom_122,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC22(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC22 % 1.32/1.36 fof(axiom_123,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC22(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC20(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC22xcomp % 1.32/1.36 fof(axiom_124,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC22xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC24 % 1.32/1.36 fof(axiom_125,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC24(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px88(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC24 % 1.32/1.36 fof(axiom_126,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC24(X) % 1.32/1.36 <=> ( cC16xcomp(X) % 1.32/1.36 & cC22xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC24xcomp % 1.32/1.36 fof(axiom_127,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC24xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px88(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC26 % 1.32/1.36 fof(axiom_128,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC26(X) % 1.32/1.36 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC26 % 1.32/1.36 fof(axiom_129,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC26(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC24(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC26xcomp % 1.32/1.36 fof(axiom_130,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC26xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC28 % 1.32/1.36 fof(axiom_131,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC28(X) % 1.32/1.36 <=> ( cC16xcomp(X) % 1.32/1.36 & cC26xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC30 % 1.32/1.36 fof(axiom_132,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC30(X) % 1.32/1.36 <=> ( cC28(X) % 1.32/1.36 & cC14(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC32 % 1.32/1.36 fof(axiom_133,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC32(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px10(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC32xcomp % 1.32/1.36 fof(axiom_134,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC32xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px10(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC34 % 1.32/1.36 fof(axiom_135,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC34(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC32xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC36 % 1.32/1.36 fof(axiom_136,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC36(X) % 1.32/1.36 <=> ( cC34(X) % 1.32/1.36 & cC32(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC38 % 1.32/1.36 fof(axiom_137,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC38(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC36(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC38 % 1.32/1.36 fof(axiom_138,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC38(X) % 1.32/1.36 <=> ? [Y0] : ra_Px12(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC38xcomp % 1.32/1.36 fof(axiom_139,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC38xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px12(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC4 % 1.32/1.36 fof(axiom_140,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC4(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC2xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC40 % 1.32/1.36 fof(axiom_141,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC40(X) % 1.32/1.36 <=> ? [Y0] : ra_Px86(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC40 % 1.32/1.36 fof(axiom_142,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC40(X) % 1.32/1.36 <=> ( cC32xcomp(X) % 1.32/1.36 & cC38xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC40xcomp % 1.32/1.36 fof(axiom_143,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC40xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px86(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC42 % 1.32/1.36 fof(axiom_144,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC42(X) % 1.32/1.36 <=> ? [Y0] : ra_Px14(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC42 % 1.32/1.36 fof(axiom_145,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC42(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC40(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC42xcomp % 1.32/1.36 fof(axiom_146,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC42xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px14(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC44 % 1.32/1.36 fof(axiom_147,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC44(X) % 1.32/1.36 <=> ( cC42xcomp(X) % 1.32/1.36 & cC32xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC46 % 1.32/1.36 fof(axiom_148,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC46(X) % 1.32/1.36 <=> ( cC30(X) % 1.32/1.36 & cC44(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC48 % 1.32/1.36 fof(axiom_149,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC48(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC16xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC50 % 1.32/1.36 fof(axiom_150,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC50(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC16xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC52 % 1.32/1.36 fof(axiom_151,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC52(X) % 1.32/1.36 <=> ( cC50(X) % 1.32/1.36 & cC16(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC54 % 1.32/1.36 fof(axiom_152,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC54(X) % 1.32/1.36 <=> ? [Y0] : ra_Px18(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC54 % 1.32/1.36 fof(axiom_153,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC54(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC52(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC54xcomp % 1.32/1.36 fof(axiom_154,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC54xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px18(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC56 % 1.32/1.36 fof(axiom_155,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC56(X) % 1.32/1.36 <=> ( cC16xcomp(X) % 1.32/1.36 & cC54xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC58 % 1.32/1.36 fof(axiom_156,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC58(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px19(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC58 % 1.32/1.36 fof(axiom_157,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC58(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC56(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC58xcomp % 1.32/1.36 fof(axiom_158,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC58xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px19(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC6 % 1.32/1.36 fof(axiom_159,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC6(X) % 1.32/1.36 <=> ( cC2(X) % 1.32/1.36 & cC4(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC60 % 1.32/1.36 fof(axiom_160,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC60(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px85(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC60 % 1.32/1.36 fof(axiom_161,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC60(X) % 1.32/1.36 <=> ( cC48(X) % 1.32/1.36 & cC58xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC60xcomp % 1.32/1.36 fof(axiom_162,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC60xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px85(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC62 % 1.32/1.36 fof(axiom_163,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC62(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC60(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC62 % 1.32/1.36 fof(axiom_164,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC62(X) % 1.32/1.36 <=> ? [Y0] : ra_Px20(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC62xcomp % 1.32/1.36 fof(axiom_165,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC62xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px20(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC64 % 1.32/1.36 fof(axiom_166,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC64(X) % 1.32/1.36 <=> ( cC62xcomp(X) % 1.32/1.36 & cTOP(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC66 % 1.32/1.36 fof(axiom_167,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC66(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC16xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC68 % 1.32/1.36 fof(axiom_168,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC68(X) % 1.32/1.36 <=> ( cC16(X) % 1.32/1.36 & cC66(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC70 % 1.32/1.36 fof(axiom_169,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC70(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC68(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC70 % 1.32/1.36 fof(axiom_170,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC70(X) % 1.32/1.36 <=> ? [Y0] : ra_Px23(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC70xcomp % 1.32/1.36 fof(axiom_171,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC70xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px23(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC72 % 1.32/1.36 fof(axiom_172,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC72(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px31(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC72 % 1.32/1.36 fof(axiom_173,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC72(X) % 1.32/1.36 <=> ( cC16xcomp(X) % 1.32/1.36 & cC70xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC72xcomp % 1.32/1.36 fof(axiom_174,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC72xcomp(X) % 1.32/1.36 <=> ? [Y0] : ra_Px31(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC74 % 1.32/1.36 fof(axiom_175,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC74(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC16xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC76 % 1.32/1.36 fof(axiom_176,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC76(X) % 1.32/1.36 <=> ( cC16(X) % 1.32/1.36 & cC74(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC78 % 1.32/1.36 fof(axiom_177,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC78(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC76(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC78 % 1.32/1.36 fof(axiom_178,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC78(X) % 1.32/1.36 <=> ? [Y0] : ra_Px26(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC78xcomp % 1.32/1.36 fof(axiom_179,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC78xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px26(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC8 % 1.32/1.36 fof(axiom_180,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC8(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC6(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC8 % 1.32/1.36 fof(axiom_181,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC8(X) % 1.32/1.36 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC8xcomp % 1.32/1.36 fof(axiom_182,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC8xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC80 % 1.32/1.36 fof(axiom_183,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC80(X) % 1.32/1.36 <=> ( cC16xcomp(X) % 1.32/1.36 & cC78xcomp(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC82 % 1.32/1.36 fof(axiom_184,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC82(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC80(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC84 % 1.32/1.36 fof(axiom_185,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC84(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC82(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC86 % 1.32/1.36 fof(axiom_186,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC86(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC16xcomp(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC88 % 1.32/1.36 fof(axiom_187,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC88(X) % 1.32/1.36 <=> ( cC16(X) % 1.32/1.36 & cC86(X) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC90 % 1.32/1.36 fof(axiom_188,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC90(X) % 1.32/1.36 <=> ? [Y] : % 1.32/1.36 ( rR1(X,Y) % 1.32/1.36 & cC88(Y) ) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC90 % 1.32/1.36 fof(axiom_189,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC90(X) % 1.32/1.36 <=> ? [Y0] : ra_Px29(X,Y0) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC90xcomp % 1.32/1.36 fof(axiom_190,axiom, % 1.32/1.36 ! [X] : % 1.32/1.36 ( cC90xcomp(X) % 1.32/1.36 <=> ~ ? [Y] : ra_Px29(X,Y) ) ). % 1.32/1.36 % 1.32/1.36 %----Equality cC92 % 1.32/1.37 fof(axiom_191,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC92(X) % 1.32/1.37 <=> ( cC16xcomp(X) % 1.32/1.37 & cC90xcomp(X) ) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC94 % 1.32/1.37 fof(axiom_192,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC94(X) % 1.32/1.37 <=> ? [Y0] : ra_Px30(X,Y0) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC94 % 1.32/1.37 fof(axiom_193,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC94(X) % 1.32/1.37 <=> ? [Y] : % 1.32/1.37 ( rR1(X,Y) % 1.32/1.37 & cC92(Y) ) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC94xcomp % 1.32/1.37 fof(axiom_194,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC94xcomp(X) % 1.32/1.37 <=> ~ ? [Y] : ra_Px30(X,Y) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC96 % 1.32/1.37 fof(axiom_195,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC96(X) % 1.32/1.37 <=> ? [Y0] : ra_Px32(X,Y0) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC96 % 1.32/1.37 fof(axiom_196,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC96(X) % 1.32/1.37 <=> ( cC84(X) % 1.32/1.37 & cC94xcomp(X) ) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC96xcomp % 1.32/1.37 fof(axiom_197,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC96xcomp(X) % 1.32/1.37 <=> ~ ? [Y] : ra_Px32(X,Y) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC98 % 1.32/1.37 fof(axiom_198,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC98(X) % 1.32/1.37 <=> ~ ? [Y] : ra_Px34(X,Y) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC98 % 1.32/1.37 fof(axiom_199,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC98(X) % 1.32/1.37 <=> ( cC72xcomp(X) % 1.32/1.37 & cC96xcomp(X) ) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cC98xcomp % 1.32/1.37 fof(axiom_200,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cC98xcomp(X) % 1.32/1.37 <=> ? [Y0] : ra_Px34(X,Y0) ) ). % 1.32/1.37 % 1.32/1.37 %----Equality cTEST % 1.32/1.37 fof(axiom_201,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( cTEST(X) % 1.32/1.37 <=> ( cC216(X) % 1.32/1.37 & cC46(X) ) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_202,axiom, % 1.32/1.37 cTEST(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_203,axiom, % 1.32/1.37 cC2xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_204,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( rR1(iV3102,X) % 1.32/1.37 => cC24xcomp(X) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_205,axiom, % 1.32/1.37 cTOP(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_206,axiom, % 1.32/1.37 cC26xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_207,axiom, % 1.32/1.37 cC32xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_208,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( rR1(iV3102,X) % 1.32/1.37 => cC98(X) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_209,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( rR1(iV3102,X) % 1.32/1.37 => cC60xcomp(X) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_210,axiom, % 1.32/1.37 cC16xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_211,axiom, % 1.32/1.37 cC42xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_212,axiom, % 1.32/1.37 cC62xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_213,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( rR1(iV3102,X) % 1.32/1.37 => cC40xcomp(X) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_214,axiom, % 1.32/1.37 ! [X] : % 1.32/1.37 ( rR1(iV3102,X) % 1.32/1.37 => cC10xcomp(X) ) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_215,axiom, % 1.32/1.37 cC12xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_216,axiom, % 1.32/1.37 cC214xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_217,axiom, % 1.32/1.37 cowlThing(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(axiom_218,axiom, % 1.32/1.37 cC100xcomp(iV3102) ). % 1.32/1.37 % 1.32/1.37 %----Thing and Nothing % 1.32/1.37 %----String and Integer disjoint % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 %----iV3102 % 1.32/1.37 fof(the_axiom,conjecture, % 1.32/1.37 ( ! [X] : % 1.32/1.37 ( cowlThing(X) % 1.32/1.37 & ~ cowlNothing(X) ) % 1.32/1.37 & ! [X] : % 1.32/1.37 ( xsd_string(X) % 1.32/1.37 <=> ~ xsd_integer(X) ) % 1.32/1.37 & cC14(iV3102) % 1.32/1.37 & cC44(iV3102) % 1.32/1.37 & cC216(iV3102) % 1.32/1.37 & cC64(iV3102) % 1.32/1.37 & cC46(iV3102) % 1.32/1.37 & cC28(iV3102) % 1.32/1.37 & cowlThing(iV3102) % 1.32/1.37 & cC30(iV3102) ) ). % 1.32/1.37 % 1.32/1.37 %------------------------------------------------------------------------------ % 1.32/1.37 %------------------------------------------- % 1.32/1.37 % Proof found % 1.32/1.37 % SZS status Theorem for theBenchmark % 1.32/1.37 % SZS output start Proof % 1.32/1.37 %ClaNum:527(EqnAxiom:0) % 1.32/1.37 %VarNum:1429(SingletonVarNum:662) % 1.32/1.37 %MaxLitNum:10 % 1.32/1.37 %MaxfuncDepth:1 % 1.32/1.37 %SharedTerms:26 % 1.32/1.37 %goalClause: 526 527 % 1.32/1.37 [1]P1(a1) % 1.32/1.37 [2]P2(a1) % 1.32/1.37 [3]P5(a1) % 1.32/1.37 [4]P6(a1) % 1.32/1.37 [5]P59(a1) % 1.32/1.37 [6]P94(a1) % 1.32/1.37 [7]P102(a1) % 1.32/1.37 [8]P105(a1) % 1.32/1.37 [9]P114(a1) % 1.32/1.37 [10]P129(a1) % 1.32/1.37 [11]P130(a1) % 1.32/1.37 [12]~P158(x121) % 1.32/1.37 [13]P160(x131)+P159(x131) % 1.32/1.37 [14]~P3(x141)+P1(x141) % 1.32/1.37 [15]~P27(x151)+P1(x151) % 1.32/1.37 [16]~P3(x161)+P131(x161) % 1.32/1.37 [17]~P60(x171)+P4(x171) % 1.32/1.37 [18]~P8(x181)+P7(x181) % 1.32/1.37 [19]~P9(x191)+P5(x191) % 1.32/1.37 [20]~P12(x201)+P5(x201) % 1.32/1.37 [21]~P19(x211)+P5(x211) % 1.32/1.37 [22]~P36(x221)+P5(x221) % 1.32/1.37 [23]~P39(x231)+P5(x231) % 1.32/1.37 [24]~P45(x241)+P5(x241) % 1.32/1.37 [25]~P61(x251)+P5(x251) % 1.32/1.37 [26]~P67(x261)+P5(x261) % 1.32/1.37 [27]~P74(x271)+P5(x271) % 1.32/1.37 [28]~P95(x281)+P5(x281) % 1.32/1.37 [29]~P101(x291)+P5(x291) % 1.32/1.37 [30]~P115(x301)+P5(x301) % 1.32/1.37 [31]~P132(x311)+P5(x311) % 1.32/1.37 [32]~P138(x321)+P5(x321) % 1.32/1.37 [33]~P149(x331)+P5(x331) % 1.32/1.37 [34]~P8(x341)+P46(x341) % 1.32/1.37 [35]~P13(x351)+P46(x351) % 1.32/1.37 [36]~P20(x361)+P46(x361) % 1.32/1.37 [37]~P28(x371)+P46(x371) % 1.32/1.37 [38]~P40(x381)+P46(x381) % 1.32/1.37 [39]~P47(x391)+P46(x391) % 1.32/1.37 [40]~P62(x401)+P46(x401) % 1.32/1.37 [41]~P68(x411)+P46(x411) % 1.32/1.37 [42]~P75(x421)+P46(x421) % 1.32/1.37 [43]~P81(x431)+P46(x431) % 1.32/1.37 [44]~P116(x441)+P46(x441) % 1.32/1.37 [45]~P133(x451)+P46(x451) % 1.32/1.37 [46]~P139(x461)+P46(x461) % 1.32/1.37 [47]~P145(x471)+P46(x471) % 1.32/1.37 [48]~P9(x481)+P10(x481) % 1.32/1.37 [49]~P29(x491)+P14(x491) % 1.32/1.37 [50]~P13(x501)+P15(x501) % 1.32/1.37 [51]~P12(x511)+P17(x511) % 1.32/1.37 [52]~P27(x521)+P6(x521) % 1.32/1.37 [53]~P30(x531)+P21(x531) % 1.32/1.37 [54]~P20(x541)+P24(x541) % 1.32/1.37 [55]~P19(x551)+P25(x551) % 1.32/1.37 [56]~P30(x561)+P31(x561) % 1.32/1.37 [57]~P29(x571)+P33(x571) % 1.32/1.37 [58]~P83(x581)+P34(x581) % 1.32/1.37 [59]~P28(x591)+P35(x591) % 1.32/1.37 [60]~P103(x601)+P27(x601) % 1.32/1.37 [61]~P36(x611)+P37(x611) % 1.32/1.37 [62]~P53(x621)+P41(x621) % 1.32/1.37 [63]~P40(x631)+P42(x631) % 1.32/1.37 [64]~P39(x641)+P43(x641) % 1.32/1.37 [65]~P54(x651)+P48(x651) % 1.32/1.37 [66]~P47(x661)+P50(x661) % 1.32/1.37 [67]~P45(x671)+P51(x671) % 1.32/1.37 [68]~P54(x681)+P55(x681) % 1.32/1.37 [69]~P53(x691)+P57(x691) % 1.32/1.37 [70]~P84(x701)+P63(x701) % 1.32/1.37 [71]~P62(x711)+P64(x711) % 1.32/1.37 [72]~P61(x721)+P65(x721) % 1.32/1.37 [73]~P85(x731)+P69(x731) % 1.32/1.37 [74]~P81(x741)+P70(x741) % 1.32/1.37 [75]~P68(x751)+P71(x751) % 1.32/1.37 [76]~P67(x761)+P72(x761) % 1.32/1.37 [77]~P86(x771)+P76(x771) % 1.32/1.37 [78]~P75(x781)+P78(x781) % 1.32/1.37 [79]~P74(x791)+P79(x791) % 1.32/1.37 [80]~P123(x801)+P82(x801) % 1.32/1.37 [81]~P86(x811)+P87(x811) % 1.32/1.37 [82]~P85(x821)+P89(x821) % 1.32/1.37 [83]~P84(x831)+P85(x831) % 1.32/1.37 [84]~P83(x841)+P90(x841) % 1.32/1.37 [85]~P60(x851)+P92(x851) % 1.32/1.37 [86]~P96(x861)+P59(x861) % 1.32/1.37 [87]~P130(x871)+P96(x871) % 1.32/1.37 [88]~P96(x881)+P134(x881) % 1.32/1.37 [89]~P95(x891)+P97(x891) % 1.32/1.37 [90]~P101(x901)+P94(x901) % 1.32/1.37 [91]~P103(x911)+P101(x911) % 1.32/1.37 [92]~P117(x921)+P103(x921) % 1.32/1.37 [93]~P106(x931)+P104(x931) % 1.32/1.37 [94]~P108(x941)+P102(x941) % 1.32/1.37 [95]~P118(x951)+P102(x951) % 1.32/1.37 [96]~P106(x961)+P107(x961) % 1.32/1.37 [97]~P108(x971)+P109(x971) % 1.32/1.37 [98]~P123(x981)+P111(x981) % 1.32/1.37 [99]~P118(x991)+P105(x991) % 1.32/1.37 [100]~P117(x1001)+P118(x1001) % 1.32/1.37 [101]~P130(x1011)+P117(x1011) % 1.32/1.37 [102]~P126(x1021)+P119(x1021) % 1.32/1.37 [103]~P116(x1031)+P120(x1031) % 1.32/1.37 [104]~P115(x1041)+P121(x1041) % 1.32/1.37 [105]~P126(x1051)+P124(x1051) % 1.32/1.37 [106]~P134(x1061)+P114(x1061) % 1.32/1.37 [107]~P134(x1071)+P129(x1071) % 1.32/1.37 [108]~P133(x1081)+P135(x1081) % 1.32/1.37 [109]~P132(x1091)+P136(x1091) % 1.32/1.37 [110]~P152(x1101)+P140(x1101) % 1.32/1.37 [111]~P139(x1111)+P141(x1111) % 1.32/1.37 [112]~P138(x1121)+P142(x1121) % 1.32/1.37 [113]~P153(x1131)+P146(x1131) % 1.32/1.37 [114]~P145(x1141)+P148(x1141) % 1.32/1.37 [115]~P149(x1151)+P150(x1151) % 1.32/1.37 [116]~P153(x1161)+P154(x1161) % 1.32/1.37 [117]~P152(x1171)+P156(x1171) % 1.32/1.37 [118]~P160(x1181)+~P159(x1181) % 1.32/1.37 [225]P16(x2251)+~P161(a1,x2251) % 1.32/1.37 [226]P100(x2261)+~P161(a1,x2261) % 1.32/1.37 [227]P113(x2271)+~P161(a1,x2271) % 1.32/1.37 [228]P128(x2281)+~P161(a1,x2281) % 1.32/1.37 [229]P152(x2291)+~P161(a1,x2291) % 1.32/1.37 [119]~P22(x1191)+P3(f2(x1191)) % 1.32/1.37 [120]~P111(x1201)+P1(f3(x1201)) % 1.32/1.37 [121]~P4(x1211)+P157(f62(x1211)) % 1.32/1.37 [122]~P7(x1221)+P5(f86(x1221)) % 1.32/1.37 [123]~P15(x1231)+P5(f8(x1231)) % 1.32/1.37 [124]~P24(x1241)+P5(f63(x1241)) % 1.32/1.37 [125]~P35(x1251)+P5(f67(x1251)) % 1.32/1.37 [126]~P42(x1261)+P5(f79(x1261)) % 1.32/1.37 [127]~P50(x1271)+P5(f87(x1271)) % 1.32/1.37 [128]~P64(x1281)+P5(f92(x1281)) % 1.32/1.37 [129]~P70(x1291)+P5(f107(x1291)) % 1.32/1.37 [130]~P71(x1301)+P5(f114(x1301)) % 1.32/1.37 [131]~P78(x1311)+P5(f119(x1311)) % 1.32/1.37 [132]~P119(x1321)+P5(f9(x1321)) % 1.32/1.37 [133]~P120(x1331)+P5(f16(x1331)) % 1.32/1.37 [134]~P135(x1341)+P5(f17(x1341)) % 1.32/1.37 [135]~P141(x1351)+P5(f30(x1351)) % 1.32/1.37 [136]~P148(x1361)+P5(f36(x1361)) % 1.32/1.37 [137]~P11(x1371)+P8(f121(x1371)) % 1.32/1.37 [138]~P18(x1381)+P13(f45(x1381)) % 1.32/1.37 [139]~P23(x1391)+P12(f47(x1391)) % 1.32/1.37 [140]~P21(x1401)+P23(f64(x1401)) % 1.32/1.37 [141]~P26(x1411)+P20(f68(x1411)) % 1.32/1.37 [142]~P32(x1421)+P19(f70(x1421)) % 1.32/1.37 [143]~P38(x1431)+P28(f80(x1431)) % 1.32/1.37 [144]~P44(x1441)+P40(f88(x1441)) % 1.32/1.37 [145]~P49(x1451)+P39(f89(x1451)) % 1.32/1.37 [146]~P48(x1461)+P49(f91(x1461)) % 1.32/1.37 [147]~P52(x1471)+P47(f93(x1471)) % 1.32/1.37 [148]~P56(x1481)+P45(f97(x1481)) % 1.32/1.37 [149]~P63(x1491)+P58(f100(x1491)) % 1.32/1.37 [150]~P66(x1501)+P62(f108(x1501)) % 1.32/1.37 [151]~P73(x1511)+P68(f115(x1511)) % 1.32/1.37 [152]~P77(x1521)+P67(f117(x1521)) % 1.32/1.37 [153]~P76(x1531)+P77(f120(x1531)) % 1.32/1.37 [154]~P80(x1541)+P75(f122(x1541)) % 1.32/1.37 [155]~P88(x1551)+P74(f124(x1551)) % 1.32/1.37 [156]~P98(x1561)+P81(f130(x1561)) % 1.32/1.37 [157]~P91(x1571)+P84(f131(x1571)) % 1.32/1.37 [158]~P93(x1581)+P83(f134(x1581)) % 1.32/1.37 [159]~P99(x1591)+P95(f143(x1591)) % 1.32/1.37 [160]~P107(x1601)+P102(f4(x1601)) % 1.32/1.37 [161]~P110(x1611)+P106(f5(x1611)) % 1.32/1.37 [162]~P112(x1621)+P108(f10(x1621)) % 1.32/1.37 [163]~P122(x1631)+P116(f18(x1631)) % 1.32/1.37 [164]~P125(x1641)+P115(f20(x1641)) % 1.32/1.37 [165]~P144(x1651)+P123(f37(x1651)) % 1.32/1.37 [166]~P127(x1661)+P126(f23(x1661)) % 1.32/1.37 [167]~P137(x1671)+P133(f31(x1671)) % 1.32/1.37 [168]~P143(x1681)+P139(f38(x1681)) % 1.32/1.37 [169]~P147(x1691)+P138(f41(x1691)) % 1.32/1.37 [170]~P146(x1701)+P147(f44(x1701)) % 1.32/1.37 [171]~P151(x1711)+P145(f46(x1711)) % 1.32/1.37 [172]~P155(x1721)+P149(f48(x1721)) % 1.32/1.37 [230]P131(x2301)+P162(x2301,f42(x2301)) % 1.32/1.37 [231]P16(x2311)+P169(x2311,f72(x2311)) % 1.32/1.37 [232]P4(x2321)+P170(x2321,f98(x2321)) % 1.32/1.37 [233]P5(x2331)+P171(x2331,f94(x2331)) % 1.32/1.37 [234]P11(x2341)+P172(x2341,f138(x2341)) % 1.32/1.37 [235]P14(x2351)+P181(x2351,f24(x2351)) % 1.32/1.37 [236]P18(x2361)+P182(x2361,f52(x2361)) % 1.32/1.37 [237]P22(x2371)+P183(x2371,f61(x2371)) % 1.32/1.37 [238]P26(x2381)+P184(x2381,f69(x2381)) % 1.32/1.37 [239]P31(x2391)+P185(x2391,f73(x2391)) % 1.32/1.37 [240]P30(x2401)+P186(x2401,f75(x2401)) % 1.32/1.37 [241]P34(x2411)+P188(x2411,f77(x2411)) % 1.32/1.37 [242]P38(x2421)+P187(x2421,f81(x2421)) % 1.32/1.37 [243]P41(x2431)+P189(x2431,f82(x2431)) % 1.32/1.37 [244]P44(x2441)+P190(x2441,f85(x2441)) % 1.32/1.37 [245]P52(x2451)+P191(x2451,f96(x2451)) % 1.32/1.37 [246]P55(x2461)+P192(x2461,f101(x2461)) % 1.32/1.37 [247]P54(x2471)+P193(x2471,f103(x2471)) % 1.32/1.37 [248]P58(x2481)+P194(x2481,f104(x2481)) % 1.32/1.37 [249]P65(x2491)+P195(x2491,f111(x2491)) % 1.32/1.37 [250]P61(x2501)+P196(x2501,f112(x2501)) % 1.32/1.37 [251]P72(x2511)+P197(x2511,f118(x2511)) % 1.32/1.37 [252]P79(x2521)+P198(x2521,f125(x2521)) % 1.32/1.37 [253]P82(x2531)+P163(x2531,f126(x2531)) % 1.32/1.37 [254]P87(x2541)+P199(x2541,f128(x2541)) % 1.32/1.37 [255]P89(x2551)+P201(x2551,f132(x2551)) % 1.32/1.37 [256]P91(x2561)+P202(x2561,f135(x2561)) % 1.32/1.37 [257]P92(x2571)+P203(x2571,f139(x2571)) % 1.32/1.37 [258]P59(x2581)+P204(x2581,f140(x2581)) % 1.32/1.37 [259]P98(x2591)+P200(x2591,f142(x2591)) % 1.32/1.37 [260]P95(x2601)+P207(x2601,f144(x2601)) % 1.32/1.37 [261]P94(x2611)+P208(x2611,f148(x2611)) % 1.32/1.37 [262]P104(x2621)+P164(x2621,f149(x2621)) % 1.32/1.37 [263]P109(x2631)+P165(x2631,f6(x2631)) % 1.32/1.37 [264]P113(x2641)+P205(x2641,f11(x2641)) % 1.32/1.37 [265]P105(x2651)+P166(x2651,f14(x2651)) % 1.32/1.37 [266]P121(x2661)+P167(x2661,f21(x2661)) % 1.32/1.37 [267]P125(x2671)+P168(x2671,f22(x2671)) % 1.32/1.37 [268]P126(x2681)+P206(x2681,f25(x2681)) % 1.32/1.37 [269]P114(x2691)+P173(x2691,f28(x2691)) % 1.32/1.37 [270]P136(x2701)+P174(x2701,f32(x2701)) % 1.32/1.37 [271]P132(x2711)+P175(x2711,f34(x2711)) % 1.32/1.37 [272]P142(x2721)+P176(x2721,f39(x2721)) % 1.32/1.37 [273]P150(x2731)+P177(x2731,f49(x2731)) % 1.32/1.37 [274]P154(x2741)+P178(x2741,f53(x2741)) % 1.32/1.37 [275]P156(x2751)+P179(x2751,f54(x2751)) % 1.32/1.37 [276]P152(x2761)+P180(x2761,f56(x2761)) % 1.32/1.37 [324]~P3(x3241)+P169(x3241,f65(x3241)) % 1.32/1.37 [325]~P4(x3251)+P161(x3251,f62(x3251)) % 1.32/1.37 [326]~P7(x3261)+P161(x3261,f86(x3261)) % 1.32/1.37 [327]~P11(x3271)+P161(x3271,f121(x3271)) % 1.32/1.37 [328]~P15(x3281)+P161(x3281,f8(x3281)) % 1.32/1.37 [329]~P18(x3291)+P161(x3291,f45(x3291)) % 1.32/1.37 [330]~P23(x3301)+P161(x3301,f47(x3301)) % 1.32/1.37 [331]~P22(x3311)+P161(x3311,f2(x3311)) % 1.32/1.37 [332]~P21(x3321)+P161(x3321,f64(x3321)) % 1.32/1.37 [333]~P24(x3331)+P161(x3331,f63(x3331)) % 1.32/1.37 [334]~P26(x3341)+P161(x3341,f68(x3341)) % 1.32/1.37 [335]~P32(x3351)+P161(x3351,f70(x3351)) % 1.32/1.37 [336]~P35(x3361)+P161(x3361,f67(x3361)) % 1.32/1.37 [337]~P38(x3371)+P161(x3371,f80(x3371)) % 1.32/1.37 [338]~P42(x3381)+P161(x3381,f79(x3381)) % 1.32/1.37 [339]~P44(x3391)+P161(x3391,f88(x3391)) % 1.32/1.37 [340]~P49(x3401)+P161(x3401,f89(x3401)) % 1.32/1.37 [341]~P48(x3411)+P161(x3411,f91(x3411)) % 1.32/1.37 [342]~P50(x3421)+P161(x3421,f87(x3421)) % 1.32/1.37 [343]~P52(x3431)+P161(x3431,f93(x3431)) % 1.32/1.37 [344]~P56(x3441)+P161(x3441,f97(x3441)) % 1.32/1.37 [345]~P63(x3451)+P161(x3451,f100(x3451)) % 1.32/1.37 [346]~P64(x3461)+P161(x3461,f92(x3461)) % 1.32/1.37 [347]~P66(x3471)+P161(x3471,f108(x3471)) % 1.32/1.37 [348]~P70(x3481)+P161(x3481,f107(x3481)) % 1.32/1.37 [349]~P71(x3491)+P161(x3491,f114(x3491)) % 1.32/1.37 [350]~P73(x3501)+P161(x3501,f115(x3501)) % 1.32/1.37 [351]~P77(x3511)+P161(x3511,f117(x3511)) % 1.32/1.37 [352]~P76(x3521)+P161(x3521,f120(x3521)) % 1.32/1.37 [353]~P78(x3531)+P161(x3531,f119(x3531)) % 1.32/1.37 [354]~P80(x3541)+P161(x3541,f122(x3541)) % 1.32/1.37 [355]~P88(x3551)+P161(x3551,f124(x3551)) % 1.32/1.37 [356]~P91(x3561)+P161(x3561,f131(x3561)) % 1.32/1.37 [357]~P93(x3571)+P161(x3571,f134(x3571)) % 1.32/1.37 [358]~P98(x3581)+P161(x3581,f130(x3581)) % 1.32/1.37 [359]~P99(x3591)+P161(x3591,f143(x3591)) % 1.32/1.37 [360]~P107(x3601)+P161(x3601,f4(x3601)) % 1.32/1.37 [361]~P110(x3611)+P161(x3611,f5(x3611)) % 1.32/1.37 [362]~P111(x3621)+P161(x3621,f3(x3621)) % 1.32/1.37 [363]~P112(x3631)+P161(x3631,f10(x3631)) % 1.32/1.37 [364]~P119(x3641)+P161(x3641,f9(x3641)) % 1.32/1.37 [365]~P120(x3651)+P161(x3651,f16(x3651)) % 1.32/1.37 [366]~P122(x3661)+P161(x3661,f18(x3661)) % 1.32/1.37 [367]~P125(x3671)+P161(x3671,f20(x3671)) % 1.32/1.37 [368]~P127(x3681)+P161(x3681,f23(x3681)) % 1.32/1.37 [369]~P135(x3691)+P161(x3691,f17(x3691)) % 1.32/1.37 [370]~P137(x3701)+P161(x3701,f31(x3701)) % 1.32/1.37 [371]~P141(x3711)+P161(x3711,f30(x3711)) % 1.32/1.37 [372]~P143(x3721)+P161(x3721,f38(x3721)) % 1.32/1.37 [373]~P144(x3731)+P161(x3731,f37(x3731)) % 1.32/1.37 [374]~P147(x3741)+P161(x3741,f41(x3741)) % 1.32/1.37 [375]~P146(x3751)+P161(x3751,f44(x3751)) % 1.32/1.37 [376]~P148(x3761)+P161(x3761,f36(x3761)) % 1.32/1.37 [377]~P151(x3771)+P161(x3771,f46(x3771)) % 1.32/1.37 [378]~P155(x3781)+P161(x3781,f48(x3781)) % 1.32/1.37 [379]~P2(x3791)+P170(x3791,f109(x3791)) % 1.32/1.37 [380]~P10(x3801)+P172(x3801,f150(x3801)) % 1.32/1.37 [381]~P9(x3811)+P181(x3811,f15(x3811)) % 1.32/1.37 [382]~P17(x3821)+P182(x3821,f58(x3821)) % 1.32/1.37 [383]~P6(x3831)+P183(x3831,f66(x3831)) % 1.32/1.37 [384]~P25(x3841)+P184(x3841,f71(x3841)) % 1.32/1.37 [385]~P32(x3851)+P185(x3851,f74(x3851)) % 1.32/1.37 [386]~P33(x3861)+P186(x3861,f76(x3861)) % 1.32/1.37 [387]~P29(x3871)+P188(x3871,f78(x3871)) % 1.32/1.37 [388]~P37(x3881)+P187(x3881,f83(x3881)) % 1.32/1.37 [389]~P36(x3891)+P189(x3891,f84(x3891)) % 1.32/1.37 [390]~P43(x3901)+P190(x3901,f90(x3901)) % 1.32/1.37 [391]~P46(x3911)+P171(x3911,f95(x3911)) % 1.32/1.37 [392]~P51(x3921)+P191(x3921,f99(x3921)) % 1.32/1.37 [393]~P56(x3931)+P192(x3931,f102(x3931)) % 1.32/1.37 [394]~P57(x3941)+P193(x3941,f105(x3941)) % 1.32/1.37 [395]~P53(x3951)+P194(x3951,f106(x3951)) % 1.32/1.37 [396]~P66(x3961)+P195(x3961,f110(x3961)) % 1.32/1.37 [397]~P69(x3971)+P196(x3971,f113(x3971)) % 1.32/1.37 [398]~P73(x3981)+P197(x3981,f116(x3981)) % 1.32/1.37 [399]~P80(x3991)+P198(x3991,f123(x3991)) % 1.32/1.37 [400]~P1(x4001)+P163(x4001,f127(x4001)) % 1.32/1.37 [401]~P88(x4011)+P199(x4011,f129(x4011)) % 1.32/1.37 [402]~P86(x4021)+P201(x4021,f133(x4021)) % 1.32/1.37 [403]~P90(x4031)+P202(x4031,f136(x4031)) % 1.32/1.37 [404]~P93(x4041)+P203(x4041,f137(x4041)) % 1.32/1.37 [405]~P60(x4051)+P204(x4051,f141(x4051)) % 1.32/1.37 [406]~P97(x4061)+P200(x4061,f145(x4061)) % 1.32/1.37 [407]~P100(x4071)+P207(x4071,f146(x4071)) % 1.32/1.37 [408]~P99(x4081)+P208(x4081,f147(x4081)) % 1.32/1.37 [409]~P102(x4091)+P164(x4091,f151(x4091)) % 1.32/1.37 [410]~P110(x4101)+P165(x4101,f7(x4101)) % 1.32/1.37 [411]~P108(x4111)+P205(x4111,f12(x4111)) % 1.32/1.37 [412]~P112(x4121)+P166(x4121,f13(x4121)) % 1.32/1.37 [413]~P122(x4131)+P167(x4131,f19(x4131)) % 1.32/1.37 [414]~P124(x4141)+P168(x4141,f26(x4141)) % 1.32/1.37 [415]~P128(x4151)+P206(x4151,f27(x4151)) % 1.32/1.37 [416]~P127(x4161)+P173(x4161,f29(x4161)) % 1.32/1.37 [417]~P137(x4171)+P174(x4171,f33(x4171)) % 1.32/1.37 [418]~P140(x4181)+P175(x4181,f35(x4181)) % 1.32/1.37 [419]~P143(x4191)+P176(x4191,f40(x4191)) % 1.32/1.37 [420]~P144(x4201)+P162(x4201,f43(x4201)) % 1.32/1.37 [421]~P151(x4211)+P177(x4211,f50(x4211)) % 1.32/1.37 [422]~P155(x4221)+P178(x4221,f51(x4221)) % 1.32/1.37 [423]~P153(x4231)+P179(x4231,f55(x4231)) % 1.32/1.37 [424]~P157(x4241)+P180(x4241,f57(x4241)) % 1.32/1.37 [277]P3(x2771)+~P169(x2771,x2772) % 1.32/1.37 [278]P1(x2781)+~P163(x2781,x2782) % 1.32/1.37 [279]P157(x2791)+~P180(x2791,x2792) % 1.32/1.37 [280]P2(x2801)+~P170(x2801,x2802) % 1.32/1.37 [281]P46(x2811)+~P171(x2811,x2812) % 1.32/1.37 [282]P10(x2821)+~P172(x2821,x2822) % 1.32/1.37 [283]P9(x2831)+~P181(x2831,x2832) % 1.32/1.37 [284]P17(x2841)+~P182(x2841,x2842) % 1.32/1.37 [285]P6(x2851)+~P183(x2851,x2852) % 1.32/1.37 [286]P25(x2861)+~P184(x2861,x2862) % 1.32/1.37 [287]P32(x2871)+~P185(x2871,x2872) % 1.32/1.37 [288]P33(x2881)+~P186(x2881,x2882) % 1.32/1.37 [289]P29(x2891)+~P188(x2891,x2892) % 1.32/1.37 [290]P37(x2901)+~P187(x2901,x2902) % 1.32/1.37 [291]P36(x2911)+~P189(x2911,x2912) % 1.32/1.37 [292]P43(x2921)+~P190(x2921,x2922) % 1.32/1.37 [293]P51(x2931)+~P191(x2931,x2932) % 1.32/1.37 [294]P56(x2941)+~P192(x2941,x2942) % 1.32/1.37 [295]P57(x2951)+~P193(x2951,x2952) % 1.32/1.37 [296]P53(x2961)+~P194(x2961,x2962) % 1.32/1.37 [297]P66(x2971)+~P195(x2971,x2972) % 1.32/1.37 [298]P69(x2981)+~P196(x2981,x2982) % 1.32/1.37 [299]P73(x2991)+~P197(x2991,x2992) % 1.32/1.37 [300]P80(x3001)+~P198(x3001,x3002) % 1.32/1.37 [301]P88(x3011)+~P199(x3011,x3012) % 1.32/1.37 [302]P86(x3021)+~P201(x3021,x3022) % 1.32/1.37 [303]P90(x3031)+~P202(x3031,x3032) % 1.32/1.37 [304]P93(x3041)+~P203(x3041,x3042) % 1.32/1.37 [305]P60(x3051)+~P204(x3051,x3052) % 1.32/1.37 [306]P97(x3061)+~P200(x3061,x3062) % 1.32/1.37 [307]P100(x3071)+~P207(x3071,x3072) % 1.32/1.37 [308]P99(x3081)+~P208(x3081,x3082) % 1.32/1.37 [309]P102(x3091)+~P164(x3091,x3092) % 1.32/1.37 [310]P110(x3101)+~P165(x3101,x3102) % 1.32/1.37 [311]P108(x3111)+~P205(x3111,x3112) % 1.32/1.37 [312]P112(x3121)+~P166(x3121,x3122) % 1.32/1.37 [313]P122(x3131)+~P167(x3131,x3132) % 1.32/1.37 [314]P124(x3141)+~P168(x3141,x3142) % 1.32/1.37 [315]P128(x3151)+~P206(x3151,x3152) % 1.32/1.37 [316]P127(x3161)+~P173(x3161,x3162) % 1.32/1.37 [317]P137(x3171)+~P174(x3171,x3172) % 1.32/1.37 [318]P140(x3181)+~P175(x3181,x3182) % 1.32/1.37 [319]P143(x3191)+~P176(x3191,x3192) % 1.32/1.37 [320]P144(x3201)+~P162(x3201,x3202) % 1.32/1.37 [321]P151(x3211)+~P177(x3211,x3212) % 1.32/1.37 [322]P155(x3221)+~P178(x3221,x3222) % 1.32/1.37 [323]P153(x3231)+~P179(x3231,x3232) % 1.32/1.37 [425]~P131(x4251)+~P162(x4251,x4252) % 1.32/1.37 [426]~P16(x4261)+~P169(x4261,x4262) % 1.32/1.37 [427]~P4(x4271)+~P170(x4271,x4272) % 1.32/1.37 [428]~P5(x4281)+~P171(x4281,x4282) % 1.32/1.37 [429]~P11(x4291)+~P172(x4291,x4292) % 1.32/1.37 [430]~P14(x4301)+~P181(x4301,x4302) % 1.32/1.37 [431]~P18(x4311)+~P182(x4311,x4312) % 1.32/1.37 [432]~P22(x4321)+~P183(x4321,x4322) % 1.32/1.37 [433]~P26(x4331)+~P184(x4331,x4332) % 1.32/1.37 [434]~P31(x4341)+~P185(x4341,x4342) % 1.32/1.37 [435]~P30(x4351)+~P186(x4351,x4352) % 1.32/1.37 [436]~P34(x4361)+~P188(x4361,x4362) % 1.32/1.37 [437]~P38(x4371)+~P187(x4371,x4372) % 1.32/1.37 [438]~P41(x4381)+~P189(x4381,x4382) % 1.32/1.37 [439]~P44(x4391)+~P190(x4391,x4392) % 1.32/1.37 [440]~P52(x4401)+~P191(x4401,x4402) % 1.32/1.37 [441]~P55(x4411)+~P192(x4411,x4412) % 1.32/1.37 [442]~P54(x4421)+~P193(x4421,x4422) % 1.32/1.37 [443]~P58(x4431)+~P194(x4431,x4432) % 1.32/1.37 [444]~P65(x4441)+~P195(x4441,x4442) % 1.32/1.37 [445]~P61(x4451)+~P196(x4451,x4452) % 1.32/1.37 [446]~P72(x4461)+~P197(x4461,x4462) % 1.32/1.37 [447]~P79(x4471)+~P198(x4471,x4472) % 1.32/1.37 [448]~P82(x4481)+~P163(x4481,x4482) % 1.32/1.37 [449]~P87(x4491)+~P199(x4491,x4492) % 1.32/1.37 [450]~P89(x4501)+~P201(x4501,x4502) % 1.32/1.37 [451]~P91(x4511)+~P202(x4511,x4512) % 1.32/1.37 [452]~P92(x4521)+~P203(x4521,x4522) % 1.32/1.37 [453]~P59(x4531)+~P204(x4531,x4532) % 1.32/1.37 [454]~P98(x4541)+~P200(x4541,x4542) % 1.32/1.37 [455]~P95(x4551)+~P207(x4551,x4552) % 1.32/1.37 [456]~P94(x4561)+~P208(x4561,x4562) % 1.32/1.37 [457]~P104(x4571)+~P164(x4571,x4572) % 1.32/1.37 [458]~P109(x4581)+~P165(x4581,x4582) % 1.32/1.37 [459]~P113(x4591)+~P205(x4591,x4592) % 1.32/1.37 [460]~P105(x4601)+~P166(x4601,x4602) % 1.32/1.37 [461]~P121(x4611)+~P167(x4611,x4612) % 1.32/1.37 [462]~P125(x4621)+~P168(x4621,x4622) % 1.32/1.37 [463]~P126(x4631)+~P206(x4631,x4632) % 1.32/1.37 [464]~P114(x4641)+~P173(x4641,x4642) % 1.32/1.37 [465]~P136(x4651)+~P174(x4651,x4652) % 1.32/1.37 [466]~P132(x4661)+~P175(x4661,x4662) % 1.32/1.37 [467]~P142(x4671)+~P176(x4671,x4672) % 1.32/1.37 [468]~P150(x4681)+~P177(x4681,x4682) % 1.32/1.37 [469]~P154(x4691)+~P178(x4691,x4692) % 1.32/1.37 [470]~P156(x4701)+~P179(x4701,x4702) % 1.32/1.37 [471]~P152(x4711)+~P180(x4711,x4712) % 1.32/1.37 [173]~P1(x1731)+~P131(x1731)+P3(x1731) % 1.32/1.37 [174]~P7(x1741)+~P46(x1741)+P8(x1741) % 1.32/1.37 [175]~P5(x1751)+~P10(x1751)+P9(x1751) % 1.32/1.37 [176]~P46(x1761)+~P15(x1761)+P13(x1761) % 1.32/1.37 [177]~P5(x1771)+~P17(x1771)+P12(x1771) % 1.32/1.37 [178]~P46(x1781)+~P24(x1781)+P20(x1781) % 1.32/1.37 [179]~P5(x1791)+~P25(x1791)+P19(x1791) % 1.32/1.37 [180]~P21(x1801)+~P31(x1801)+P30(x1801) % 1.32/1.37 [181]~P14(x1811)+~P33(x1811)+P29(x1811) % 1.32/1.37 [182]~P46(x1821)+~P35(x1821)+P28(x1821) % 1.32/1.37 [183]~P1(x1831)+~P6(x1831)+P27(x1831) % 1.32/1.37 [184]~P5(x1841)+~P37(x1841)+P36(x1841) % 1.32/1.37 [185]~P46(x1851)+~P42(x1851)+P40(x1851) % 1.32/1.37 [186]~P5(x1861)+~P43(x1861)+P39(x1861) % 1.32/1.37 [187]~P46(x1871)+~P50(x1871)+P47(x1871) % 1.32/1.37 [188]~P5(x1881)+~P51(x1881)+P45(x1881) % 1.32/1.37 [189]~P48(x1891)+~P55(x1891)+P54(x1891) % 1.32/1.37 [190]~P41(x1901)+~P57(x1901)+P53(x1901) % 1.32/1.37 [191]~P46(x1911)+~P64(x1911)+P62(x1911) % 1.32/1.37 [192]~P5(x1921)+~P65(x1921)+P61(x1921) % 1.32/1.37 [193]~P46(x1931)+~P71(x1931)+P68(x1931) % 1.32/1.37 [194]~P5(x1941)+~P72(x1941)+P67(x1941) % 1.32/1.37 [195]~P46(x1951)+~P78(x1951)+P75(x1951) % 1.32/1.37 [196]~P5(x1961)+~P79(x1961)+P74(x1961) % 1.32/1.37 [197]~P46(x1971)+~P70(x1971)+P81(x1971) % 1.32/1.37 [198]~P76(x1981)+~P87(x1981)+P86(x1981) % 1.32/1.37 [199]~P69(x1991)+~P89(x1991)+P85(x1991) % 1.32/1.37 [200]~P63(x2001)+~P85(x2001)+P84(x2001) % 1.32/1.37 [201]~P34(x2011)+~P90(x2011)+P83(x2011) % 1.32/1.37 [202]~P4(x2021)+~P92(x2021)+P60(x2021) % 1.32/1.37 [203]~P59(x2031)+~P134(x2031)+P96(x2031) % 1.32/1.37 [204]~P114(x2041)+~P129(x2041)+P134(x2041) % 1.32/1.37 [205]~P5(x2051)+~P97(x2051)+P95(x2051) % 1.32/1.37 [206]~P5(x2061)+~P94(x2061)+P101(x2061) % 1.32/1.37 [207]~P27(x2071)+~P101(x2071)+P103(x2071) % 1.32/1.37 [208]~P104(x2081)+~P107(x2081)+P106(x2081) % 1.32/1.37 [209]~P102(x2091)+~P109(x2091)+P108(x2091) % 1.32/1.37 [210]~P102(x2101)+~P105(x2101)+P118(x2101) % 1.32/1.37 [211]~P103(x2111)+~P118(x2111)+P117(x2111) % 1.32/1.37 [212]~P46(x2121)+~P120(x2121)+P116(x2121) % 1.32/1.37 [213]~P5(x2131)+~P121(x2131)+P115(x2131) % 1.32/1.37 [214]~P82(x2141)+~P111(x2141)+P123(x2141) % 1.32/1.37 [215]~P119(x2151)+~P124(x2151)+P126(x2151) % 1.32/1.37 [216]~P46(x2161)+~P135(x2161)+P133(x2161) % 1.32/1.37 [217]~P5(x2171)+~P136(x2171)+P132(x2171) % 1.32/1.37 [218]~P46(x2181)+~P141(x2181)+P139(x2181) % 1.32/1.37 [219]~P5(x2191)+~P142(x2191)+P138(x2191) % 1.32/1.37 [220]~P46(x2201)+~P148(x2201)+P145(x2201) % 1.32/1.37 [221]~P5(x2211)+~P150(x2211)+P149(x2211) % 1.32/1.37 [222]~P146(x2221)+~P154(x2221)+P153(x2221) % 1.32/1.37 [223]~P140(x2231)+~P156(x2231)+P152(x2231) % 1.32/1.37 [224]~P96(x2241)+~P117(x2241)+P130(x2241) % 1.32/1.37 [472]~P161(x4721,x4722)+P4(x4721)+~P157(x4722) % 1.32/1.37 [473]~P161(x4731,x4732)+P7(x4731)+~P5(x4732) % 1.32/1.37 [474]~P161(x4741,x4742)+P11(x4741)+~P8(x4742) % 1.32/1.37 [475]~P161(x4751,x4752)+P15(x4751)+~P5(x4752) % 1.32/1.37 [476]~P161(x4761,x4762)+P18(x4761)+~P13(x4762) % 1.32/1.37 [477]~P161(x4771,x4772)+P23(x4771)+~P12(x4772) % 1.32/1.37 [478]~P161(x4781,x4782)+P22(x4781)+~P3(x4782) % 1.32/1.37 [479]~P161(x4791,x4792)+P21(x4791)+~P23(x4792) % 1.32/1.37 [480]~P161(x4801,x4802)+P24(x4801)+~P5(x4802) % 1.32/1.37 [481]~P161(x4811,x4812)+P26(x4811)+~P20(x4812) % 1.32/1.37 [482]~P161(x4821,x4822)+P32(x4821)+~P19(x4822) % 1.32/1.37 [483]~P161(x4831,x4832)+P35(x4831)+~P5(x4832) % 1.32/1.37 [484]~P161(x4841,x4842)+P38(x4841)+~P28(x4842) % 1.32/1.37 [485]~P161(x4851,x4852)+P42(x4851)+~P5(x4852) % 1.32/1.37 [486]~P161(x4861,x4862)+P44(x4861)+~P40(x4862) % 1.32/1.37 [487]~P161(x4871,x4872)+P49(x4871)+~P39(x4872) % 1.32/1.37 [488]~P161(x4881,x4882)+P48(x4881)+~P49(x4882) % 1.32/1.37 [489]~P161(x4891,x4892)+P50(x4891)+~P5(x4892) % 1.32/1.37 [490]~P161(x4901,x4902)+P52(x4901)+~P47(x4902) % 1.32/1.37 [491]~P161(x4911,x4912)+P56(x4911)+~P45(x4912) % 1.32/1.37 [492]~P161(x4921,x4922)+P63(x4921)+~P58(x4922) % 1.32/1.37 [493]~P161(x4931,x4932)+P64(x4931)+~P5(x4932) % 1.32/1.37 [494]~P161(x4941,x4942)+P66(x4941)+~P62(x4942) % 1.32/1.37 [495]~P161(x4951,x4952)+P70(x4951)+~P5(x4952) % 1.32/1.37 [496]~P161(x4961,x4962)+P71(x4961)+~P5(x4962) % 1.32/1.37 [497]~P161(x4971,x4972)+P73(x4971)+~P68(x4972) % 1.32/1.37 [498]~P161(x4981,x4982)+P77(x4981)+~P67(x4982) % 1.32/1.37 [499]~P161(x4991,x4992)+P76(x4991)+~P77(x4992) % 1.32/1.37 [500]~P161(x5001,x5002)+P78(x5001)+~P5(x5002) % 1.32/1.37 [501]~P161(x5011,x5012)+P80(x5011)+~P75(x5012) % 1.32/1.37 [502]~P161(x5021,x5022)+P88(x5021)+~P74(x5022) % 1.32/1.37 [503]~P161(x5031,x5032)+P91(x5031)+~P84(x5032) % 1.32/1.37 [504]~P161(x5041,x5042)+P93(x5041)+~P83(x5042) % 1.32/1.37 [505]~P161(x5051,x5052)+P98(x5051)+~P81(x5052) % 1.32/1.37 [506]~P161(x5061,x5062)+P99(x5061)+~P95(x5062) % 1.32/1.37 [507]~P161(x5071,x5072)+P107(x5071)+~P102(x5072) % 1.32/1.37 [508]~P161(x5081,x5082)+P110(x5081)+~P106(x5082) % 1.32/1.37 [509]~P161(x5091,x5092)+P111(x5091)+~P1(x5092) % 1.32/1.37 [510]~P161(x5101,x5102)+P112(x5101)+~P108(x5102) % 1.32/1.37 [511]~P161(x5111,x5112)+P119(x5111)+~P5(x5112) % 1.32/1.37 [512]~P161(x5121,x5122)+P120(x5121)+~P5(x5122) % 1.32/1.37 [513]~P161(x5131,x5132)+P122(x5131)+~P116(x5132) % 1.32/1.37 [514]~P161(x5141,x5142)+P125(x5141)+~P115(x5142) % 1.32/1.37 [515]~P161(x5151,x5152)+P127(x5151)+~P126(x5152) % 1.32/1.37 [516]~P161(x5161,x5162)+P135(x5161)+~P5(x5162) % 1.32/1.37 [517]~P161(x5171,x5172)+P137(x5171)+~P133(x5172) % 1.32/1.37 [518]~P161(x5181,x5182)+P141(x5181)+~P5(x5182) % 1.32/1.37 [519]~P161(x5191,x5192)+P143(x5191)+~P139(x5192) % 1.32/1.37 [520]~P161(x5201,x5202)+P144(x5201)+~P123(x5202) % 1.32/1.37 [521]~P161(x5211,x5212)+P147(x5211)+~P138(x5212) % 1.32/1.37 [522]~P161(x5221,x5222)+P146(x5221)+~P147(x5222) % 1.32/1.37 [523]~P161(x5231,x5232)+P148(x5231)+~P5(x5232) % 1.32/1.37 [524]~P161(x5241,x5242)+P151(x5241)+~P145(x5242) % 1.32/1.37 [525]~P161(x5251,x5252)+P155(x5251)+~P149(x5252) % 1.32/1.37 [526]P158(a59)+P159(a60)+~P160(a60)+~P27(a1)+~P96(a1)+~P134(a1)+~P101(a1)+~P103(a1)+~P118(a1)+~P117(a1) % 1.32/1.37 [527]P158(a59)+P160(a60)+~P159(a60)+~P27(a1)+~P96(a1)+~P134(a1)+~P101(a1)+~P103(a1)+~P118(a1)+~P117(a1) % 1.32/1.37 %EqnAxiom % 1.32/1.37 % 1.32/1.37 %------------------------------------------- % 1.32/1.37 cnf(576,plain, % 1.32/1.37 (P27(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,8,9,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183])). % 1.32/1.37 cnf(578,plain, % 1.32/1.37 (P134(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204])). % 1.32/1.37 cnf(580,plain, % 1.32/1.37 (P101(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204,206])). % 1.32/1.37 cnf(582,plain, % 1.32/1.37 (P103(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204,206,207])). % 1.32/1.37 cnf(584,plain, % 1.32/1.37 (P118(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,7,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204,206,207,210])). % 1.32/1.37 cnf(586,plain, % 1.32/1.37 (P117(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,7,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204,206,207,210,211])). % 1.32/1.37 cnf(588,plain, % 1.32/1.37 (P96(a1)), % 1.32/1.37 inference(scs_inference,[],[1,3,4,5,6,7,8,9,10,428,453,456,460,464,391,405,408,412,416,34,35,36,37,38,39,40,41,42,43,44,45,46,47,183,204,206,207,210,211,203])). % 1.32/1.37 cnf(598,plain, % 1.32/1.37 (P159(a60)+~P160(a60)), % 1.32/1.37 inference(scs_inference,[],[12,576,588,578,580,582,584,586,526])). % 1.32/1.37 cnf(599,plain, % 1.32/1.37 (P160(a60)+~P159(a60)), % 1.32/1.37 inference(scs_inference,[],[12,576,588,578,580,582,584,586,527])). % 1.32/1.37 cnf(686,plain, % 1.32/1.37 (~P160(a60)), % 1.32/1.37 inference(scs_inference,[],[598,118])). % 1.32/1.37 cnf(687,plain, % 1.32/1.37 (~P159(a60)), % 1.32/1.37 inference(scs_inference,[],[686,599])). % 1.32/1.37 cnf(688,plain, % 1.32/1.37 ($false), % 1.32/1.37 inference(scs_inference,[],[686,687,13]), % 1.32/1.37 ['proof']). % 1.32/1.37 % SZS output end Proof % 1.32/1.37 % Total time :0.660000s %------------------------------------------------------------------------------