%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS156+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 : n020.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:42 EDT 2024 % Result : Theorem 9.82s 9.80s % Output : CNFRefutation 9.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : KRS156+1 : TPTP v8.2.0. Released v3.1.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.14/0.34 % Computer : n020.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Jun 19 13:13:54 EDT 2024 % 0.14/0.35 % CPUTime : % 0.50/0.58 start to proof:theBenchmark % 9.70/9.76 %------------------------------------------- % 9.70/9.76 % File :CSE---1.7 % 9.70/9.76 % Problem :theBenchmark % 9.70/9.76 % Transform :cnf % 9.70/9.76 % Format :tptp:raw % 9.70/9.76 % Command :java -jar mcs_scs.jar %d %s % 9.70/9.76 % 9.70/9.76 % Result :Theorem 9.110000s % 9.70/9.76 % Output :CNFRefutation 9.110000s % 9.70/9.76 %------------------------------------------- % 9.70/9.77 %------------------------------------------------------------------------------ % 9.70/9.77 % File : KRS156+1 : TPTP v8.2.0. Released v3.1.0. % 9.70/9.77 % Domain : Knowledge Representation (Semantic Web) % 9.70/9.77 % Problem : DL Test: k_dum ABox test from DL98 systems comparison % 9.70/9.77 % Version : Especial. % 9.70/9.77 % English : % 9.70/9.77 % 9.70/9.77 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 9.70/9.77 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 9.70/9.77 % Source : [Bec03] % 9.70/9.77 % Names : positive_description-logic-Manifest663 [Bec03] % 9.70/9.77 % 9.70/9.77 % Status : Theorem % 9.70/9.77 % Rating : 0.00 v6.1.0, 0.08 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.07 v5.0.0, 0.10 v4.1.0, 0.06 v4.0.1, 0.00 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.17 v3.3.0, 0.00 v3.2.0, 0.11 v3.1.0 % 9.70/9.77 % Syntax : Number of formulae : 146 ( 13 unt; 0 def) % 9.70/9.77 % Number of atoms : 355 ( 0 equ) % 9.70/9.77 % Maximal formula atoms : 8 ( 2 avg) % 9.70/9.77 % Number of connectives : 241 ( 32 ~; 0 |; 77 &) % 9.70/9.77 % ( 128 <=>; 4 =>; 0 <=; 0 <~>) % 9.70/9.77 % Maximal formula depth : 6 ( 4 avg) % 9.70/9.77 % Maximal term depth : 1 ( 1 avg) % 9.70/9.77 % Number of predicates : 133 ( 133 usr; 0 prp; 1-2 aty) % 9.70/9.77 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 9.70/9.77 % Number of variables : 228 ( 134 !; 94 ?) % 9.70/9.77 % SPC : FOF_THM_RFO_NEQ % 9.70/9.77 % 9.70/9.77 % Comments : Sean Bechhofer says there are some errors in the encoding of % 9.70/9.77 % datatypes, so this problem may not be perfect. At least it's % 9.70/9.77 % still representative of the type of reasoning required for OWL. % 9.70/9.77 %------------------------------------------------------------------------------ % 9.70/9.77 %----Thing and Nothing % 9.70/9.77 fof(axiom_0,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cowlThing(X) % 9.70/9.77 & ~ cowlNothing(X) ) ). % 9.70/9.77 % 9.70/9.77 %----String and Integer disjoint % 9.70/9.77 fof(axiom_1,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( xsd_string(X) % 9.70/9.77 <=> ~ xsd_integer(X) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC10 % 9.70/9.77 fof(axiom_2,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC10(X) % 9.70/9.77 <=> ? [Y0] : ra_Px50(X,Y0) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC10 % 9.70/9.77 fof(axiom_3,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC10(X) % 9.70/9.77 <=> ( cC2xcomp(X) % 9.70/9.77 & cC8xcomp(X) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC10xcomp % 9.70/9.77 fof(axiom_4,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC10xcomp(X) % 9.70/9.77 <=> ~ ? [Y] : ra_Px50(X,Y) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC100 % 9.70/9.77 fof(axiom_5,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC100(X) % 9.70/9.77 <=> ( cC98xcomp(X) % 9.70/9.77 & cC94(X) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC102 % 9.70/9.77 fof(axiom_6,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC102(X) % 9.70/9.77 <=> ? [Y] : % 9.70/9.77 ( rR1(X,Y) % 9.70/9.77 & cC100(Y) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC102 % 9.70/9.77 fof(axiom_7,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC102(X) % 9.70/9.77 <=> ? [Y0] : ra_Px30(X,Y0) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC102xcomp % 9.70/9.77 fof(axiom_8,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC102xcomp(X) % 9.70/9.77 <=> ~ ? [Y] : ra_Px30(X,Y) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC104 % 9.70/9.77 fof(axiom_9,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC104(X) % 9.70/9.77 <=> ( cC102xcomp(X) % 9.70/9.77 & cC88(X) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC106 % 9.70/9.77 fof(axiom_10,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC106(X) % 9.70/9.77 <=> ? [Y] : % 9.70/9.77 ( rR1(X,Y) % 9.70/9.77 & cC104(Y) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC106 % 9.70/9.77 fof(axiom_11,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC106(X) % 9.70/9.77 <=> ~ ? [Y] : ra_Px31(X,Y) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC106xcomp % 9.70/9.77 fof(axiom_12,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC106xcomp(X) % 9.70/9.77 <=> ? [Y0] : ra_Px31(X,Y0) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC108 % 9.70/9.77 fof(axiom_13,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC108(X) % 9.70/9.77 <=> ? [Y0] : ra_Px32(X,Y0) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC108 % 9.70/9.77 fof(axiom_14,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC108(X) % 9.70/9.77 <=> ( cC84(X) % 9.70/9.77 & cC106xcomp(X) ) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC108xcomp % 9.70/9.77 fof(axiom_15,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC108xcomp(X) % 9.70/9.77 <=> ~ ? [Y] : ra_Px32(X,Y) ) ). % 9.70/9.77 % 9.70/9.77 %----Equality cC110 % 9.70/9.77 fof(axiom_16,axiom, % 9.70/9.77 ! [X] : % 9.70/9.77 ( cC110(X) % 9.70/9.77 <=> ( cC62(X) % 9.70/9.78 & cC108xcomp(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC110 % 9.70/9.78 fof(axiom_17,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC110(X) % 9.70/9.78 <=> ? [Y0] : ra_Px33(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC110xcomp % 9.70/9.78 fof(axiom_18,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC110xcomp(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px33(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC112 % 9.70/9.78 fof(axiom_19,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC112(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px43(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC112 % 9.70/9.78 fof(axiom_20,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC112(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC110xcomp(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC112xcomp % 9.70/9.78 fof(axiom_21,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC112xcomp(X) % 9.70/9.78 <=> ? [Y0] : ra_Px43(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC114 % 9.70/9.78 fof(axiom_22,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC114(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px34(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC114 % 9.70/9.78 fof(axiom_23,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC114(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC112(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC114xcomp % 9.70/9.78 fof(axiom_24,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC114xcomp(X) % 9.70/9.78 <=> ? [Y0] : ra_Px34(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC116 % 9.70/9.78 fof(axiom_25,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC116(X) % 9.70/9.78 <=> ( cTOP(X) % 9.70/9.78 & cC114xcomp(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC118 % 9.70/9.78 fof(axiom_26,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC118(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC2xcomp(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC118 % 9.70/9.78 fof(axiom_27,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC118(X) % 9.70/9.78 <=> ? [Y0] : ra_Px36(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC118xcomp % 9.70/9.78 fof(axiom_28,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC118xcomp(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px36(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC12 % 9.70/9.78 fof(axiom_29,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC12(X) % 9.70/9.78 <=> ? [Y0] : ra_Px45(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC12 % 9.70/9.78 fof(axiom_30,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC12(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC10(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC12xcomp % 9.70/9.78 fof(axiom_31,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC12xcomp(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px45(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC120 % 9.70/9.78 fof(axiom_32,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC120(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC118xcomp(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC122 % 9.70/9.78 fof(axiom_33,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC122(X) % 9.70/9.78 <=> ( cC2xcomp(X) % 9.70/9.78 & cC120(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC124 % 9.70/9.78 fof(axiom_34,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC124(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC2xcomp(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC126 % 9.70/9.78 fof(axiom_35,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC126(X) % 9.70/9.78 <=> ( cC2(X) % 9.70/9.78 & cC124(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC128 % 9.70/9.78 fof(axiom_36,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC128(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px40(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC128 % 9.70/9.78 fof(axiom_37,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC128(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC126(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC128xcomp % 9.70/9.78 fof(axiom_38,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC128xcomp(X) % 9.70/9.78 <=> ? [Y0] : ra_Px40(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC130 % 9.70/9.78 fof(axiom_39,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC130(X) % 9.70/9.78 <=> ? [Y0] : ra_Px47(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC130 % 9.70/9.78 fof(axiom_40,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC130(X) % 9.70/9.78 <=> ( cC2xcomp(X) % 9.70/9.78 & cC128xcomp(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC130xcomp % 9.70/9.78 fof(axiom_41,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC130xcomp(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px47(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC132 % 9.70/9.78 fof(axiom_42,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC132(X) % 9.70/9.78 <=> ? [Y0] : ra_Px41(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC132 % 9.70/9.78 fof(axiom_43,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC132(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC130(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC132xcomp % 9.70/9.78 fof(axiom_44,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC132xcomp(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px41(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC134 % 9.70/9.78 fof(axiom_45,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC134(X) % 9.70/9.78 <=> ( cC132xcomp(X) % 9.70/9.78 & cC122(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC136 % 9.70/9.78 fof(axiom_46,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC136(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC134(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC138 % 9.70/9.78 fof(axiom_47,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC138(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC136(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC14 % 9.70/9.78 fof(axiom_48,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC14(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC12(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC140 % 9.70/9.78 fof(axiom_49,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC140(X) % 9.70/9.78 <=> ( cTOP(X) % 9.70/9.78 & cC138(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC16 % 9.70/9.78 fof(axiom_50,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC16(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC2xcomp(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC18 % 9.70/9.78 fof(axiom_51,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC18(X) % 9.70/9.78 <=> ( cC16(X) % 9.70/9.78 & cC2(X) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC2 % 9.70/9.78 fof(axiom_52,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC2(X) % 9.70/9.78 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC2xcomp % 9.70/9.78 fof(axiom_53,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC2xcomp(X) % 9.70/9.78 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC20 % 9.70/9.78 fof(axiom_54,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC20(X) % 9.70/9.78 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC20 % 9.70/9.78 fof(axiom_55,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC20(X) % 9.70/9.78 <=> ? [Y] : % 9.70/9.78 ( rR1(X,Y) % 9.70/9.78 & cC18(Y) ) ) ). % 9.70/9.78 % 9.70/9.78 %----Equality cC20xcomp % 9.70/9.78 fof(axiom_56,axiom, % 9.70/9.78 ! [X] : % 9.70/9.78 ( cC20xcomp(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC22 % 9.70/9.79 fof(axiom_57,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC22(X) % 9.70/9.79 <=> ( cC2xcomp(X) % 9.70/9.79 & cC20xcomp(X) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC24 % 9.70/9.79 fof(axiom_58,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC24(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC22(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC24 % 9.70/9.79 fof(axiom_59,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC24(X) % 9.70/9.79 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC24xcomp % 9.70/9.79 fof(axiom_60,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC24xcomp(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC26 % 9.70/9.79 fof(axiom_61,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC26(X) % 9.70/9.79 <=> ( cC14(X) % 9.70/9.79 & cC24xcomp(X) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC26 % 9.70/9.79 fof(axiom_62,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC26(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px10(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC26xcomp % 9.70/9.79 fof(axiom_63,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC26xcomp(X) % 9.70/9.79 <=> ? [Y0] : ra_Px10(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC28 % 9.70/9.79 fof(axiom_64,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC28(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC2xcomp(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC28 % 9.70/9.79 fof(axiom_65,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC28(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px49(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC28xcomp % 9.70/9.79 fof(axiom_66,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC28xcomp(X) % 9.70/9.79 <=> ? [Y0] : ra_Px49(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC30 % 9.70/9.79 fof(axiom_67,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC30(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC28(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC30 % 9.70/9.79 fof(axiom_68,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC30(X) % 9.70/9.79 <=> ? [Y0] : ra_Px44(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC30xcomp % 9.70/9.79 fof(axiom_69,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC30xcomp(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px44(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC32 % 9.70/9.79 fof(axiom_70,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC32(X) % 9.70/9.79 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC32 % 9.70/9.79 fof(axiom_71,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC32(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC2xcomp(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC32xcomp % 9.70/9.79 fof(axiom_72,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC32xcomp(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC34 % 9.70/9.79 fof(axiom_73,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC34(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px46(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC34 % 9.70/9.79 fof(axiom_74,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC34(X) % 9.70/9.79 <=> ( cC32xcomp(X) % 9.70/9.79 & cC30(X) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC34xcomp % 9.70/9.79 fof(axiom_75,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC34xcomp(X) % 9.70/9.79 <=> ? [Y0] : ra_Px46(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC36 % 9.70/9.79 fof(axiom_76,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC36(X) % 9.70/9.79 <=> ? [Y0] : ra_Px11(X,Y0) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC36 % 9.70/9.79 fof(axiom_77,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC36(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC34(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC36xcomp % 9.70/9.79 fof(axiom_78,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC36xcomp(X) % 9.70/9.79 <=> ~ ? [Y] : ra_Px11(X,Y) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC38 % 9.70/9.79 fof(axiom_79,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC38(X) % 9.70/9.79 <=> ( cC26xcomp(X) % 9.70/9.79 & cC36xcomp(X) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC4 % 9.70/9.79 fof(axiom_80,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC4(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC2xcomp(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC40 % 9.70/9.79 fof(axiom_81,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC40(X) % 9.70/9.79 <=> ? [Y] : % 9.70/9.79 ( rR1(X,Y) % 9.70/9.79 & cC2xcomp(Y) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC42 % 9.70/9.79 fof(axiom_82,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC42(X) % 9.70/9.79 <=> ( cC2xcomp(X) % 9.70/9.79 & cC40(X) ) ) ). % 9.70/9.79 % 9.70/9.79 %----Equality cC44 % 9.70/9.79 fof(axiom_83,axiom, % 9.70/9.79 ! [X] : % 9.70/9.79 ( cC44(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC44 % 9.82/9.79 fof(axiom_84,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC44(X) % 9.82/9.79 <=> ? [Y0] : ra_Px15(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC44xcomp % 9.82/9.79 fof(axiom_85,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC44xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px15(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC46 % 9.82/9.79 fof(axiom_86,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC46(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC44xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC48 % 9.82/9.79 fof(axiom_87,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC48(X) % 9.82/9.79 <=> ( cC42(X) % 9.82/9.79 & cC46(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC50 % 9.82/9.79 fof(axiom_88,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC50(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC52 % 9.82/9.79 fof(axiom_89,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC52(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC50(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC54 % 9.82/9.79 fof(axiom_90,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC54(X) % 9.82/9.79 <=> ? [Y0] : ra_Px18(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC54 % 9.82/9.79 fof(axiom_91,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC54(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC52(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC54xcomp % 9.82/9.79 fof(axiom_92,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC54xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px18(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC56 % 9.82/9.79 fof(axiom_93,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC56(X) % 9.82/9.79 <=> ( cC2xcomp(X) % 9.82/9.79 & cC54xcomp(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC58 % 9.82/9.79 fof(axiom_94,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC58(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC56(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC58 % 9.82/9.79 fof(axiom_95,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC58(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px19(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC58xcomp % 9.82/9.79 fof(axiom_96,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC58xcomp(X) % 9.82/9.79 <=> ? [Y0] : ra_Px19(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC6 % 9.82/9.79 fof(axiom_97,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC6(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC4(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC60 % 9.82/9.79 fof(axiom_98,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC60(X) % 9.82/9.79 <=> ( cC48(X) % 9.82/9.79 & cC58xcomp(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC60 % 9.82/9.79 fof(axiom_99,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC60(X) % 9.82/9.79 <=> ? [Y0] : ra_Px20(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC60xcomp % 9.82/9.79 fof(axiom_100,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC60xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px20(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC62 % 9.82/9.79 fof(axiom_101,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC62(X) % 9.82/9.79 <=> ( cC38(X) % 9.82/9.79 & cC60xcomp(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC64 % 9.82/9.79 fof(axiom_102,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC64(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC66 % 9.82/9.79 fof(axiom_103,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC66(X) % 9.82/9.79 <=> ( cC64(X) % 9.82/9.79 & cC2(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC68 % 9.82/9.79 fof(axiom_104,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC68(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC70 % 9.82/9.79 fof(axiom_105,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC70(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC68(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC72 % 9.82/9.79 fof(axiom_106,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC72(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC70(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC74 % 9.82/9.79 fof(axiom_107,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC74(X) % 9.82/9.79 <=> ( cC66(X) % 9.82/9.79 & cC72(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC76 % 9.82/9.79 fof(axiom_108,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC76(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC78 % 9.82/9.79 fof(axiom_109,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC78(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC76(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC8 % 9.82/9.79 fof(axiom_110,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC8(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC6(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC8 % 9.82/9.79 fof(axiom_111,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC8(X) % 9.82/9.79 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC8xcomp % 9.82/9.79 fof(axiom_112,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC8xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC80 % 9.82/9.79 fof(axiom_113,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC80(X) % 9.82/9.79 <=> ? [Y0] : ra_Px24(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC80 % 9.82/9.79 fof(axiom_114,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC80(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC78(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC80xcomp % 9.82/9.79 fof(axiom_115,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC80xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px24(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC82 % 9.82/9.79 fof(axiom_116,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC82(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC80xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC84 % 9.82/9.79 fof(axiom_117,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC84(X) % 9.82/9.79 <=> ( cC82(X) % 9.82/9.79 & cC74(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC86 % 9.82/9.79 fof(axiom_118,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC86(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC88 % 9.82/9.79 fof(axiom_119,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC88(X) % 9.82/9.79 <=> ( cC86(X) % 9.82/9.79 & cC2(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC90 % 9.82/9.79 fof(axiom_120,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC90(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC92 % 9.82/9.79 fof(axiom_121,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC92(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC90(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC94 % 9.82/9.79 fof(axiom_122,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC94(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC92(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC96 % 9.82/9.79 fof(axiom_123,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC96(X) % 9.82/9.79 <=> ? [Y] : % 9.82/9.79 ( rR1(X,Y) % 9.82/9.79 & cC2xcomp(Y) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC98 % 9.82/9.79 fof(axiom_124,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC98(X) % 9.82/9.79 <=> ( cC2(X) % 9.82/9.79 & cC96(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC98 % 9.82/9.79 fof(axiom_125,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC98(X) % 9.82/9.79 <=> ? [Y0] : ra_Px29(X,Y0) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cC98xcomp % 9.82/9.79 fof(axiom_126,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cC98xcomp(X) % 9.82/9.79 <=> ~ ? [Y] : ra_Px29(X,Y) ) ). % 9.82/9.79 % 9.82/9.79 %----Equality cTEST % 9.82/9.79 fof(axiom_127,axiom, % 9.82/9.79 ! [X] : % 9.82/9.79 ( cTEST(X) % 9.82/9.79 <=> ( cC140(X) % 9.82/9.79 & cC116(X) ) ) ). % 9.82/9.79 % 9.82/9.79 %----iV5475 % 9.82/9.79 fof(axiom_128,axiom, % 9.82/9.79 cTOP(iV5475) ). % 9.82/9.80 % 9.82/9.80 %----iV5475 % 9.82/9.80 fof(axiom_129,axiom, % 9.82/9.80 cowlThing(iV5475) ). % 9.82/9.80 % 9.82/9.80 %----iV5475 % 9.82/9.80 fof(axiom_130,axiom, % 9.82/9.80 cC114xcomp(iV5475) ). % 9.82/9.80 % 9.82/9.80 %----iV5475 % 9.82/9.80 fof(axiom_131,axiom, % 9.82/9.80 cTEST(iV5475) ). % 9.82/9.80 % 9.82/9.80 %----iV5475 % 9.82/9.80 fof(axiom_132,axiom, % 9.82/9.80 ! [X] : % 9.82/9.80 ( rR1(iV5475,X) % 9.82/9.80 => cC112xcomp(X) ) ). % 9.82/9.80 % 9.82/9.80 fof(axiom_133,axiom, % 9.82/9.80 rR1(iV5475,iV5476) ). % 9.82/9.80 % 9.82/9.80 %----iV5476 % 9.82/9.80 fof(axiom_134,axiom, % 9.82/9.80 cowlThing(iV5476) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_135,axiom, % 9.82/9.80 cC12xcomp(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_136,axiom, % 9.82/9.80 cC30xcomp(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_137,axiom, % 9.82/9.80 cC2(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_138,axiom, % 9.82/9.80 cowlThing(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_139,axiom, % 9.82/9.80 cC118xcomp(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_140,axiom, % 9.82/9.80 ! [X] : % 9.82/9.80 ( rR1(iV5478,X) % 9.82/9.80 => cC2(X) ) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_141,axiom, % 9.82/9.80 cC130xcomp(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_142,axiom, % 9.82/9.80 cC34xcomp(iV5478) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_143,axiom, % 9.82/9.80 ! [X] : % 9.82/9.80 ( rR1(iV5478,X) % 9.82/9.80 => cC10xcomp(X) ) ). % 9.82/9.80 % 9.82/9.80 %----iV5478 % 9.82/9.80 fof(axiom_144,axiom, % 9.82/9.80 ! [X] : % 9.82/9.80 ( rR1(iV5478,X) % 9.82/9.80 => cC28xcomp(X) ) ). % 9.82/9.80 % 9.82/9.80 %----Thing and Nothing % 9.82/9.80 %----String and Integer disjoint % 9.82/9.80 %----iV5475 % 9.82/9.80 %----iV5475 % 9.82/9.80 %----iV5475 % 9.82/9.80 %----iV5475 % 9.82/9.80 fof(the_axiom,conjecture, % 9.82/9.80 ( ! [X] : % 9.82/9.80 ( cowlThing(X) % 9.82/9.80 & ~ cowlNothing(X) ) % 9.82/9.80 & ! [X] : % 9.82/9.80 ( xsd_string(X) % 9.82/9.80 <=> ~ xsd_integer(X) ) % 9.82/9.80 & cC116(iV5475) % 9.82/9.80 & cC140(iV5475) % 9.82/9.80 & cowlThing(iV5475) % 9.82/9.80 & cC138(iV5475) ) ). % 9.82/9.80 % 9.82/9.80 %------------------------------------------------------------------------------ % 9.82/9.80 %------------------------------------------- % 9.82/9.80 % Proof found % 9.82/9.80 % SZS status Theorem for theBenchmark % 9.82/9.80 % SZS output start Proof % 9.82/9.80 %ClaNum:341(EqnAxiom:0) % 9.82/9.80 %VarNum:915(SingletonVarNum:423) % 9.82/9.80 %MaxLitNum:6 % 9.82/9.80 %MaxfuncDepth:1 % 9.82/9.80 %SharedTerms:23 % 9.82/9.80 %goalClause: 180 181 % 9.82/9.80 [1]P1(a1) % 9.82/9.80 [2]P17(a1) % 9.82/9.80 [3]P18(a98) % 9.82/9.80 [4]P21(a98) % 9.82/9.80 [5]P29(a98) % 9.82/9.80 [6]P30(a98) % 9.82/9.80 [7]P41(a98) % 9.82/9.80 [8]P53(a98) % 9.82/9.80 [9]P57(a1) % 9.82/9.80 [10]P101(a1,a99) % 9.82/9.80 [11]~P102(x111) % 9.82/9.80 [12]P104(x121)+P103(x121) % 9.82/9.80 [13]~P2(x131)+P42(x131) % 9.82/9.80 [14]~P22(x141)+P42(x141) % 9.82/9.80 [15]~P31(x151)+P42(x151) % 9.82/9.80 [16]~P43(x161)+P42(x161) % 9.82/9.80 [17]~P58(x171)+P42(x171) % 9.82/9.80 [18]~P64(x181)+P42(x181) % 9.82/9.80 [19]~P2(x191)+P73(x191) % 9.82/9.80 [20]~P3(x201)+P95(x201) % 9.82/9.80 [21]~P3(x211)+P96(x211) % 9.82/9.80 [22]~P6(x221)+P4(x221) % 9.82/9.80 [23]~P6(x231)+P74(x231) % 9.82/9.80 [24]~P9(x241)+P7(x241) % 9.82/9.80 [25]~P9(x251)+P75(x251) % 9.82/9.80 [26]~P11(x261)+P10(x261) % 9.82/9.80 [27]~P11(x271)+P76(x271) % 9.82/9.80 [28]~P19(x281)+P1(x281) % 9.82/9.80 [29]~P57(x291)+P19(x291) % 9.82/9.80 [30]~P19(x301)+P17(x301) % 9.82/9.80 [31]~P32(x311)+P17(x311) % 9.82/9.80 [32]~P22(x321)+P23(x321) % 9.82/9.80 [33]~P33(x331)+P22(x331) % 9.82/9.80 [34]~P26(x341)+P25(x341) % 9.82/9.80 [35]~P74(x351)+P29(x351) % 9.82/9.80 [36]~P26(x361)+P29(x361) % 9.82/9.80 [37]~P39(x371)+P29(x371) % 9.82/9.80 [38]~P65(x381)+P29(x381) % 9.82/9.80 [39]~P77(x391)+P29(x391) % 9.82/9.80 [40]~P82(x401)+P29(x401) % 9.82/9.80 [41]~P84(x411)+P29(x411) % 9.82/9.80 [42]~P86(x421)+P29(x421) % 9.82/9.80 [43]~P97(x431)+P29(x431) % 9.82/9.80 [44]~P99(x441)+P29(x441) % 9.82/9.80 [45]~P31(x451)+P27(x451) % 9.82/9.80 [46]~P33(x461)+P34(x461) % 9.82/9.80 [47]~P32(x471)+P36(x471) % 9.82/9.80 [48]~P46(x481)+P38(x481) % 9.82/9.80 [49]~P57(x491)+P32(x491) % 9.82/9.80 [50]~P39(x501)+P40(x501) % 9.82/9.80 [51]~P43(x511)+P44(x511) % 9.82/9.80 [52]~P46(x521)+P47(x521) % 9.82/9.80 [53]~P59(x531)+P49(x531) % 9.82/9.80 [54]~P54(x541)+P52(x541) % 9.82/9.80 [55]~P54(x551)+P55(x551) % 9.82/9.80 [56]~P59(x561)+P60(x561) % 9.82/9.80 [57]~P76(x571)+P59(x571) % 9.82/9.80 [58]~P77(x581)+P62(x581) % 9.82/9.80 [59]~P58(x591)+P63(x591) % 9.82/9.80 [60]~P66(x601)+P58(x601) % 9.82/9.80 [61]~P66(x611)+P67(x611) % 9.82/9.80 [62]~P80(x621)+P66(x621) % 9.82/9.80 [63]~P65(x631)+P70(x631) % 9.82/9.80 [64]~P64(x641)+P71(x641) % 9.82/9.80 [65]~P80(x651)+P78(x651) % 9.82/9.80 [66]~P76(x661)+P81(x661) % 9.82/9.80 [67]~P82(x671)+P83(x671) % 9.82/9.80 [68]~P87(x681)+P82(x681) % 9.82/9.80 [69]~P84(x691)+P85(x691) % 9.82/9.80 [70]~P87(x701)+P88(x701) % 9.82/9.80 [71]~P75(x711)+P87(x711) % 9.82/9.80 [72]~P86(x721)+P89(x721) % 9.82/9.80 [73]~P75(x731)+P90(x731) % 9.82/9.80 [74]~P74(x741)+P94(x741) % 9.82/9.80 [75]~P97(x751)+P98(x751) % 9.82/9.80 [76]~P99(x761)+P100(x761) % 9.82/9.80 [77]~P104(x771)+~P103(x771) % 9.82/9.80 [148]P12(x1481)+~P101(a98,x1481) % 9.82/9.80 [149]P16(x1491)+~P101(a1,x1491) % 9.82/9.80 [150]P29(x1501)+~P101(a98,x1501) % 9.82/9.80 [151]P51(x1511)+~P101(a98,x1511) % 9.82/9.80 [78]~P24(x781)+P2(f2(x781)) % 9.82/9.80 [79]~P20(x791)+P42(f3(x791)) % 9.82/9.80 [80]~P25(x801)+P42(f17(x801)) % 9.82/9.80 [81]~P40(x811)+P42(f20(x811)) % 9.82/9.80 [82]~P50(x821)+P42(f33(x821)) % 9.82/9.80 [83]~P56(x831)+P42(f45(x831)) % 9.82/9.80 [84]~P62(x841)+P42(f53(x841)) % 9.82/9.80 [85]~P63(x851)+P42(f61(x851)) % 9.82/9.80 [86]~P68(x861)+P42(f62(x861)) % 9.82/9.80 [87]~P70(x871)+P42(f63(x871)) % 9.82/9.80 [88]~P83(x881)+P42(f67(x881)) % 9.82/9.80 [89]~P85(x891)+P42(f77(x891)) % 9.82/9.80 [90]~P89(x901)+P42(f78(x901)) % 9.82/9.80 [91]~P94(x911)+P42(f81(x911)) % 9.82/9.80 [92]~P98(x921)+P42(f89(x921)) % 9.82/9.80 [93]~P100(x931)+P42(f91(x931)) % 9.82/9.80 [94]~P5(x941)+P3(f34(x941)) % 9.82/9.80 [95]~P8(x951)+P6(f68(x951)) % 9.82/9.80 [96]~P14(x961)+P13(f4(x961)) % 9.82/9.80 [97]~P15(x971)+P14(f9(x971)) % 9.82/9.80 [98]~P23(x981)+P18(f18(x981)) % 9.82/9.80 [99]~P38(x991)+P24(f21(x991)) % 9.82/9.80 [100]~P28(x1001)+P26(f22(x1001)) % 9.82/9.80 [101]~P35(x1011)+P31(f24(x1011)) % 9.82/9.80 [102]~P37(x1021)+P33(f30(x1021)) % 9.82/9.80 [103]~P36(x1031)+P37(f32(x1031)) % 9.82/9.80 [104]~P45(x1041)+P39(f36(x1041)) % 9.82/9.80 [105]~P48(x1051)+P43(f39(x1051)) % 9.82/9.80 [106]~P52(x1061)+P50(f46(x1061)) % 9.82/9.80 [107]~P61(x1071)+P54(f54(x1071)) % 9.82/9.80 [108]~P67(x1081)+P69(f64(x1081)) % 9.82/9.80 [109]~P72(x1091)+P65(f69(x1091)) % 9.82/9.80 [110]~P79(x1101)+P64(f71(x1101)) % 9.82/9.80 [111]~P91(x1111)+P77(f82(x1111)) % 9.82/9.80 [112]~P88(x1121)+P84(f79(x1121)) % 9.82/9.80 [113]~P92(x1131)+P86(f83(x1131)) % 9.82/9.80 [114]~P90(x1141)+P93(f87(x1141)) % 9.82/9.80 [115]~P96(x1151)+P97(f92(x1151)) % 9.82/9.80 [152]P73(x1521)+P105(x1521,f84(x1521)) % 9.82/9.80 [153]P12(x1531)+P112(x1531,f25(x1531)) % 9.82/9.80 [154]P95(x1541)+P113(x1541,f93(x1541)) % 9.82/9.80 [155]P4(x1551)+P116(x1551,f55(x1551)) % 9.82/9.80 [156]P8(x1561)+P117(x1561,f80(x1561)) % 9.82/9.80 [157]P10(x1571)+P118(x1571,f5(x1571)) % 9.82/9.80 [158]P13(x1581)+P119(x1581,f6(x1581)) % 9.82/9.80 [159]P14(x1591)+P120(x1591,f8(x1591)) % 9.82/9.80 [160]P15(x1601)+P121(x1601,f10(x1601)) % 9.82/9.80 [161]P18(x1611)+P122(x1611,f13(x1611)) % 9.82/9.80 [162]P21(x1621)+P125(x1621,f19(x1621)) % 9.82/9.80 [163]P29(x1631)+P106(x1631,f35(x1631)) % 9.82/9.80 [164]P28(x1641)+P123(x1641,f23(x1641)) % 9.82/9.80 [165]P30(x1651)+P127(x1651,f27(x1651)) % 9.82/9.80 [166]P34(x1661)+P124(x1661,f31(x1661)) % 9.82/9.80 [167]P44(x1671)+P129(x1671,f40(x1671)) % 9.82/9.80 [168]P47(x1681)+P131(x1681,f41(x1681)) % 9.82/9.80 [169]P46(x1691)+P107(x1691,f43(x1691)) % 9.82/9.80 [170]P50(x1701)+P130(x1701,f47(x1701)) % 9.82/9.80 [171]P41(x1711)+P126(x1711,f50(x1711)) % 9.82/9.80 [172]P55(x1721)+P132(x1721,f56(x1721)) % 9.82/9.80 [173]P54(x1731)+P128(x1731,f57(x1731)) % 9.82/9.80 [174]P60(x1741)+P108(x1741,f60(x1741)) % 9.82/9.80 [175]P69(x1751)+P109(x1751,f65(x1751)) % 9.82/9.80 [176]P71(x1761)+P110(x1761,f72(x1761)) % 9.82/9.80 [177]P79(x1771)+P111(x1771,f73(x1771)) % 9.82/9.80 [178]P81(x1781)+P114(x1781,f74(x1781)) % 9.82/9.80 [179]P93(x1791)+P115(x1791,f88(x1791)) % 9.82/9.80 [210]~P2(x2101)+P112(x2101,f14(x2101)) % 9.82/9.80 [211]~P5(x2111)+P101(x2111,f34(x2111)) % 9.82/9.80 [212]~P8(x2121)+P101(x2121,f68(x2121)) % 9.82/9.80 [213]~P14(x2131)+P101(x2131,f4(x2131)) % 9.82/9.80 [214]~P15(x2141)+P101(x2141,f9(x2141)) % 9.82/9.80 [215]~P20(x2151)+P101(x2151,f3(x2151)) % 9.82/9.80 [216]~P24(x2161)+P101(x2161,f2(x2161)) % 9.82/9.80 [217]~P23(x2171)+P101(x2171,f18(x2171)) % 9.82/9.80 [218]~P25(x2181)+P101(x2181,f17(x2181)) % 9.82/9.80 [219]~P28(x2191)+P101(x2191,f22(x2191)) % 9.82/9.80 [220]~P35(x2201)+P101(x2201,f24(x2201)) % 9.82/9.80 [221]~P37(x2211)+P101(x2211,f30(x2211)) % 9.82/9.80 [222]~P36(x2221)+P101(x2221,f32(x2221)) % 9.82/9.80 [223]~P38(x2231)+P101(x2231,f21(x2231)) % 9.82/9.80 [224]~P40(x2241)+P101(x2241,f20(x2241)) % 9.82/9.80 [225]~P45(x2251)+P101(x2251,f36(x2251)) % 9.82/9.80 [226]~P48(x2261)+P101(x2261,f39(x2261)) % 9.82/9.80 [227]~P50(x2271)+P101(x2271,f33(x2271)) % 9.82/9.80 [228]~P52(x2281)+P101(x2281,f46(x2281)) % 9.82/9.80 [229]~P56(x2291)+P101(x2291,f45(x2291)) % 9.82/9.80 [230]~P61(x2301)+P101(x2301,f54(x2301)) % 9.82/9.80 [231]~P62(x2311)+P101(x2311,f53(x2311)) % 9.82/9.80 [232]~P63(x2321)+P101(x2321,f61(x2321)) % 9.82/9.80 [233]~P68(x2331)+P101(x2331,f62(x2331)) % 9.82/9.80 [234]~P67(x2341)+P101(x2341,f64(x2341)) % 9.82/9.80 [235]~P70(x2351)+P101(x2351,f63(x2351)) % 9.82/9.80 [236]~P72(x2361)+P101(x2361,f69(x2361)) % 9.82/9.80 [237]~P79(x2371)+P101(x2371,f71(x2371)) % 9.82/9.80 [238]~P83(x2381)+P101(x2381,f67(x2381)) % 9.82/9.80 [239]~P85(x2391)+P101(x2391,f77(x2391)) % 9.82/9.80 [240]~P88(x2401)+P101(x2401,f79(x2401)) % 9.82/9.80 [241]~P89(x2411)+P101(x2411,f78(x2411)) % 9.82/9.80 [242]~P91(x2421)+P101(x2421,f82(x2421)) % 9.82/9.80 [243]~P92(x2431)+P101(x2431,f83(x2431)) % 9.82/9.80 [244]~P90(x2441)+P101(x2441,f87(x2441)) % 9.82/9.80 [245]~P94(x2451)+P101(x2451,f81(x2451)) % 9.82/9.80 [246]~P98(x2461)+P101(x2461,f89(x2461)) % 9.82/9.80 [247]~P96(x2471)+P101(x2471,f92(x2471)) % 9.82/9.80 [248]~P100(x2481)+P101(x2481,f91(x2481)) % 9.82/9.80 [249]~P5(x2491)+P116(x2491,f48(x2491)) % 9.82/9.80 [250]~P7(x2501)+P117(x2501,f90(x2501)) % 9.82/9.80 [251]~P9(x2511)+P118(x2511,f97(x2511)) % 9.82/9.80 [252]~P11(x2521)+P119(x2521,f7(x2521)) % 9.82/9.80 [253]~P16(x2531)+P120(x2531,f11(x2531)) % 9.82/9.80 [254]~P1(x2541)+P121(x2541,f12(x2541)) % 9.82/9.80 [255]~P20(x2551)+P122(x2551,f15(x2551)) % 9.82/9.80 [256]~P24(x2561)+P125(x2561,f16(x2561)) % 9.82/9.80 [257]~P27(x2571)+P123(x2571,f26(x2571)) % 9.82/9.80 [258]~P31(x2581)+P127(x2581,f28(x2581)) % 9.82/9.80 [259]~P35(x2591)+P124(x2591,f29(x2591)) % 9.82/9.80 [260]~P42(x2601)+P106(x2601,f37(x2601)) % 9.82/9.80 [261]~P45(x2611)+P129(x2611,f38(x2611)) % 9.82/9.80 [262]~P48(x2621)+P131(x2621,f42(x2621)) % 9.82/9.80 [263]~P49(x2631)+P107(x2631,f44(x2631)) % 9.82/9.80 [264]~P51(x2641)+P130(x2641,f49(x2641)) % 9.82/9.80 [265]~P52(x2651)+P126(x2651,f51(x2651)) % 9.82/9.80 [266]~P56(x2661)+P132(x2661,f52(x2661)) % 9.82/9.80 [267]~P53(x2671)+P128(x2671,f58(x2671)) % 9.82/9.80 [268]~P61(x2681)+P108(x2681,f59(x2681)) % 9.82/9.80 [269]~P68(x2691)+P109(x2691,f66(x2691)) % 9.82/9.80 [270]~P72(x2701)+P110(x2701,f70(x2701)) % 9.82/9.80 [271]~P78(x2711)+P111(x2711,f75(x2711)) % 9.82/9.80 [272]~P80(x2721)+P114(x2721,f76(x2721)) % 9.82/9.80 [273]~P91(x2731)+P105(x2731,f85(x2731)) % 9.82/9.80 [274]~P92(x2741)+P115(x2741,f86(x2741)) % 9.82/9.80 [275]~P99(x2751)+P113(x2751,f94(x2751)) % 9.82/9.80 [182]P2(x1821)+~P112(x1821,x1822) % 9.82/9.80 [183]P42(x1831)+~P106(x1831,x1832) % 9.82/9.80 [184]P5(x1841)+~P116(x1841,x1842) % 9.82/9.80 [185]P7(x1851)+~P117(x1851,x1852) % 9.82/9.80 [186]P9(x1861)+~P118(x1861,x1862) % 9.82/9.80 [187]P11(x1871)+~P119(x1871,x1872) % 9.82/9.80 [188]P16(x1881)+~P120(x1881,x1882) % 9.82/9.80 [189]P1(x1891)+~P121(x1891,x1892) % 9.82/9.80 [190]P20(x1901)+~P122(x1901,x1902) % 9.82/9.80 [191]P24(x1911)+~P125(x1911,x1912) % 9.82/9.80 [192]P27(x1921)+~P123(x1921,x1922) % 9.82/9.80 [193]P31(x1931)+~P127(x1931,x1932) % 9.82/9.80 [194]P35(x1941)+~P124(x1941,x1942) % 9.82/9.80 [195]P45(x1951)+~P129(x1951,x1952) % 9.82/9.80 [196]P48(x1961)+~P131(x1961,x1962) % 9.82/9.80 [197]P49(x1971)+~P107(x1971,x1972) % 9.82/9.80 [198]P51(x1981)+~P130(x1981,x1982) % 9.82/9.80 [199]P52(x1991)+~P126(x1991,x1992) % 9.82/9.80 [200]P56(x2001)+~P132(x2001,x2002) % 9.82/9.80 [201]P53(x2011)+~P128(x2011,x2012) % 9.82/9.80 [202]P61(x2021)+~P108(x2021,x2022) % 9.82/9.80 [203]P68(x2031)+~P109(x2031,x2032) % 9.82/9.80 [204]P72(x2041)+~P110(x2041,x2042) % 9.82/9.80 [205]P78(x2051)+~P111(x2051,x2052) % 9.82/9.80 [206]P80(x2061)+~P114(x2061,x2062) % 9.82/9.80 [207]P91(x2071)+~P105(x2071,x2072) % 9.82/9.80 [208]P92(x2081)+~P115(x2081,x2082) % 9.82/9.80 [209]P99(x2091)+~P113(x2091,x2092) % 9.82/9.80 [276]~P73(x2761)+~P105(x2761,x2762) % 9.82/9.80 [277]~P12(x2771)+~P112(x2771,x2772) % 9.82/9.80 [278]~P95(x2781)+~P113(x2781,x2782) % 9.82/9.80 [279]~P4(x2791)+~P116(x2791,x2792) % 9.82/9.80 [280]~P8(x2801)+~P117(x2801,x2802) % 9.82/9.80 [281]~P10(x2811)+~P118(x2811,x2812) % 9.82/9.80 [282]~P13(x2821)+~P119(x2821,x2822) % 9.82/9.80 [283]~P14(x2831)+~P120(x2831,x2832) % 9.82/9.80 [284]~P15(x2841)+~P121(x2841,x2842) % 9.82/9.80 [285]~P18(x2851)+~P122(x2851,x2852) % 9.82/9.80 [286]~P21(x2861)+~P125(x2861,x2862) % 9.82/9.80 [287]~P29(x2871)+~P106(x2871,x2872) % 9.82/9.80 [288]~P28(x2881)+~P123(x2881,x2882) % 9.82/9.80 [289]~P30(x2891)+~P127(x2891,x2892) % 9.82/9.80 [290]~P34(x2901)+~P124(x2901,x2902) % 9.82/9.80 [291]~P44(x2911)+~P129(x2911,x2912) % 9.82/9.80 [292]~P47(x2921)+~P131(x2921,x2922) % 9.82/9.80 [293]~P46(x2931)+~P107(x2931,x2932) % 9.82/9.80 [294]~P50(x2941)+~P130(x2941,x2942) % 9.82/9.80 [295]~P41(x2951)+~P126(x2951,x2952) % 9.82/9.80 [296]~P55(x2961)+~P132(x2961,x2962) % 9.82/9.80 [297]~P54(x2971)+~P128(x2971,x2972) % 9.82/9.80 [298]~P60(x2981)+~P108(x2981,x2982) % 9.82/9.80 [299]~P69(x2991)+~P109(x2991,x2992) % 9.82/9.80 [300]~P71(x3001)+~P110(x3001,x3002) % 9.82/9.80 [301]~P79(x3011)+~P111(x3011,x3012) % 9.82/9.80 [302]~P81(x3021)+~P114(x3021,x3022) % 9.82/9.80 [303]~P93(x3031)+~P115(x3031,x3032) % 9.82/9.80 [116]~P42(x1161)+~P73(x1161)+P2(x1161) % 9.82/9.80 [117]~P95(x1171)+~P96(x1171)+P3(x1171) % 9.82/9.80 [118]~P4(x1181)+~P74(x1181)+P6(x1181) % 9.82/9.80 [119]~P29(x1191)+~P94(x1191)+P74(x1191) % 9.82/9.80 [120]~P7(x1201)+~P75(x1201)+P9(x1201) % 9.82/9.80 [121]~P87(x1211)+~P90(x1211)+P75(x1211) % 9.82/9.80 [122]~P10(x1221)+~P76(x1221)+P11(x1221) % 9.82/9.80 [123]~P59(x1231)+~P81(x1231)+P76(x1231) % 9.82/9.80 [124]~P1(x1241)+~P17(x1241)+P19(x1241) % 9.82/9.80 [125]~P42(x1251)+~P23(x1251)+P22(x1251) % 9.82/9.80 [126]~P25(x1261)+~P29(x1261)+P26(x1261) % 9.82/9.80 [127]~P42(x1271)+~P27(x1271)+P31(x1271) % 9.82/9.80 [128]~P22(x1281)+~P34(x1281)+P33(x1281) % 9.82/9.80 [129]~P17(x1291)+~P36(x1291)+P32(x1291) % 9.82/9.80 [130]~P29(x1301)+~P40(x1301)+P39(x1301) % 9.82/9.80 [131]~P42(x1311)+~P44(x1311)+P43(x1311) % 9.82/9.80 [132]~P38(x1321)+~P47(x1321)+P46(x1321) % 9.82/9.80 [133]~P52(x1331)+~P55(x1331)+P54(x1331) % 9.82/9.80 [134]~P49(x1341)+~P60(x1341)+P59(x1341) % 9.82/9.80 [135]~P42(x1351)+~P63(x1351)+P58(x1351) % 9.82/9.80 [136]~P58(x1361)+~P67(x1361)+P66(x1361) % 9.82/9.80 [137]~P29(x1371)+~P70(x1371)+P65(x1371) % 9.82/9.80 [138]~P42(x1381)+~P71(x1381)+P64(x1381) % 9.82/9.80 [139]~P29(x1391)+~P62(x1391)+P77(x1391) % 9.82/9.80 [140]~P66(x1401)+~P78(x1401)+P80(x1401) % 9.82/9.80 [141]~P29(x1411)+~P83(x1411)+P82(x1411) % 9.82/9.80 [142]~P29(x1421)+~P85(x1421)+P84(x1421) % 9.82/9.80 [143]~P82(x1431)+~P88(x1431)+P87(x1431) % 9.82/9.80 [144]~P29(x1441)+~P89(x1441)+P86(x1441) % 9.82/9.80 [145]~P29(x1451)+~P98(x1451)+P97(x1451) % 9.82/9.80 [146]~P29(x1461)+~P100(x1461)+P99(x1461) % 9.82/9.80 [147]~P19(x1471)+~P32(x1471)+P57(x1471) % 9.82/9.80 [304]~P101(x3041,x3042)+P96(x3041)+~P97(x3042) % 9.82/9.80 [305]~P101(x3051,x3052)+P5(x3051)+~P3(x3052) % 9.82/9.80 [306]~P101(x3061,x3062)+P8(x3061)+~P6(x3062) % 9.82/9.80 [307]~P101(x3071,x3072)+P14(x3071)+~P13(x3072) % 9.82/9.80 [308]~P101(x3081,x3082)+P15(x3081)+~P14(x3082) % 9.82/9.80 [309]~P101(x3091,x3092)+P20(x3091)+~P42(x3092) % 9.82/9.80 [310]~P101(x3101,x3102)+P24(x3101)+~P2(x3102) % 9.82/9.80 [311]~P101(x3111,x3112)+P23(x3111)+~P18(x3112) % 9.82/9.80 [312]~P101(x3121,x3122)+P25(x3121)+~P42(x3122) % 9.82/9.80 [313]~P101(x3131,x3132)+P28(x3131)+~P26(x3132) % 9.82/9.80 [314]~P101(x3141,x3142)+P35(x3141)+~P31(x3142) % 9.82/9.80 [315]~P101(x3151,x3152)+P37(x3151)+~P33(x3152) % 9.82/9.80 [316]~P101(x3161,x3162)+P36(x3161)+~P37(x3162) % 9.82/9.80 [317]~P101(x3171,x3172)+P38(x3171)+~P24(x3172) % 9.82/9.80 [318]~P101(x3181,x3182)+P40(x3181)+~P42(x3182) % 9.82/9.80 [319]~P101(x3191,x3192)+P45(x3191)+~P39(x3192) % 9.82/9.80 [320]~P101(x3201,x3202)+P48(x3201)+~P43(x3202) % 9.82/9.80 [321]~P101(x3211,x3212)+P50(x3211)+~P42(x3212) % 9.82/9.80 [322]~P101(x3221,x3222)+P52(x3221)+~P50(x3222) % 9.82/9.80 [323]~P101(x3231,x3232)+P56(x3231)+~P42(x3232) % 9.82/9.80 [324]~P101(x3241,x3242)+P61(x3241)+~P54(x3242) % 9.82/9.80 [325]~P101(x3251,x3252)+P62(x3251)+~P42(x3252) % 9.82/9.80 [326]~P101(x3261,x3262)+P63(x3261)+~P42(x3262) % 9.82/9.80 [327]~P101(x3271,x3272)+P68(x3271)+~P42(x3272) % 9.82/9.80 [328]~P101(x3281,x3282)+P67(x3281)+~P69(x3282) % 9.82/9.80 [329]~P101(x3291,x3292)+P70(x3291)+~P42(x3292) % 9.82/9.80 [330]~P101(x3301,x3302)+P72(x3301)+~P65(x3302) % 9.82/9.80 [331]~P101(x3311,x3312)+P79(x3311)+~P64(x3312) % 9.82/9.80 [332]~P101(x3321,x3322)+P83(x3321)+~P42(x3322) % 9.82/9.80 [333]~P101(x3331,x3332)+P85(x3331)+~P42(x3332) % 9.82/9.80 [334]~P101(x3341,x3342)+P88(x3341)+~P84(x3342) % 9.82/9.80 [335]~P101(x3351,x3352)+P89(x3351)+~P42(x3352) % 9.82/9.80 [336]~P101(x3361,x3362)+P91(x3361)+~P77(x3362) % 9.82/9.80 [337]~P101(x3371,x3372)+P92(x3371)+~P86(x3372) % 9.82/9.80 [338]~P101(x3381,x3382)+P90(x3381)+~P93(x3382) % 9.82/9.80 [339]~P101(x3391,x3392)+P94(x3391)+~P42(x3392) % 9.82/9.80 [340]~P101(x3401,x3402)+P98(x3401)+~P42(x3402) % 9.82/9.80 [341]~P101(x3411,x3412)+P100(x3411)+~P42(x3412) % 9.82/9.80 [180]P102(a95)+P103(a96)+~P104(a96)+~P19(a1)+~P36(a1)+~P32(a1) % 9.82/9.80 [181]P102(a95)+P104(a96)+~P103(a96)+~P19(a1)+~P36(a1)+~P32(a1) % 9.82/9.80 %EqnAxiom % 9.82/9.80 % 9.82/9.80 %------------------------------------------- % 9.82/9.80 cnf(354,plain, % 9.82/9.80 (P19(a1)), % 9.82/9.80 inference(scs_inference,[],[1,2,10,3,5,4,7,149,287,260,285,286,295,124])). % 9.82/9.80 cnf(399,plain, % 9.82/9.80 (P103(a96)+~P104(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[11,354,180])). % 9.82/9.80 cnf(400,plain, % 9.82/9.80 (P104(a96)+~P103(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[11,354,181])). % 9.82/9.80 cnf(1741,plain, % 9.82/9.80 (P104(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[12,400])). % 9.82/9.80 cnf(1742,plain, % 9.82/9.80 (~P103(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[1741,77])). % 9.82/9.80 cnf(1743,plain, % 9.82/9.80 (~P104(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[1742,399])). % 9.82/9.80 cnf(1744,plain, % 9.82/9.80 (P103(a96)+~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[1743,12])). % 9.82/9.80 cnf(1745,plain, % 9.82/9.80 (~P36(a1)+~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[1744,1742])). % 9.82/9.80 cnf(1746,plain, % 9.82/9.80 (~P32(a1)), % 9.82/9.80 inference(scs_inference,[],[1745,47])). % 9.82/9.80 cnf(1748,plain, % 9.82/9.80 ($false), % 9.82/9.80 inference(scs_inference,[],[1746,9,49]), % 9.82/9.80 ['proof']). % 9.82/9.80 % SZS output end Proof % 9.82/9.80 % Total time :9.110000s %------------------------------------------------------------------------------