%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS154+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 : n002.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 1.18s 1.29s % Output : CNFRefutation 1.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.10 % Problem : KRS154+1 : TPTP v8.2.0. Released v3.1.0. % 0.08/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n002.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:03:38 EDT 2024 % 0.10/0.31 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 1.14/1.27 %------------------------------------------- % 1.14/1.27 % File :CSE---1.7 % 1.14/1.27 % Problem :theBenchmark % 1.14/1.27 % Transform :cnf % 1.14/1.27 % Format :tptp:raw % 1.14/1.27 % Command :java -jar mcs_scs.jar %d %s % 1.14/1.27 % 1.14/1.27 % Result :Theorem 0.630000s % 1.14/1.27 % Output :CNFRefutation 0.630000s % 1.14/1.27 %------------------------------------------- % 1.18/1.28 %------------------------------------------------------------------------------ % 1.18/1.28 % File : KRS154+1 : TPTP v8.2.0. Released v3.1.0. % 1.18/1.28 % Domain : Knowledge Representation (Semantic Web) % 1.18/1.28 % Problem : DL Test: k_branch ABox test from DL98 systems comparison % 1.18/1.28 % Version : Especial. % 1.18/1.28 % English : % 1.18/1.28 % 1.18/1.28 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.18/1.28 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.18/1.28 % Source : [Bec03] % 1.18/1.28 % Names : positive_description-logic-Manifest661 [Bec03] % 1.18/1.28 % 1.18/1.28 % Status : Theorem % 1.18/1.28 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.11 v4.0.0, 0.10 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.17 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0 % 1.18/1.28 % Syntax : Number of formulae : 170 ( 20 unt; 0 def) % 1.18/1.28 % Number of atoms : 397 ( 0 equ) % 1.18/1.28 % Maximal formula atoms : 13 ( 2 avg) % 1.18/1.28 % Number of connectives : 270 ( 43 ~; 0 |; 78 &) % 1.18/1.28 % ( 146 <=>; 3 =>; 0 <=; 0 <~>) % 1.18/1.28 % Maximal formula depth : 11 ( 4 avg) % 1.18/1.28 % Maximal term depth : 1 ( 1 avg) % 1.18/1.28 % Number of predicates : 154 ( 154 usr; 0 prp; 1-2 aty) % 1.18/1.28 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 1.18/1.28 % Number of variables : 242 ( 151 !; 91 ?) % 1.18/1.28 % SPC : FOF_THM_RFO_NEQ % 1.18/1.28 % 1.18/1.28 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.18/1.28 % datatypes, so this problem may not be perfect. At least it's % 1.18/1.28 % still representative of the type of reasoning required for OWL. % 1.18/1.28 %------------------------------------------------------------------------------ % 1.18/1.28 %----Thing and Nothing % 1.18/1.28 fof(axiom_0,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cowlThing(X) % 1.18/1.28 & ~ cowlNothing(X) ) ). % 1.18/1.28 % 1.18/1.28 %----String and Integer disjoint % 1.18/1.28 fof(axiom_1,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( xsd_string(X) % 1.18/1.28 <=> ~ xsd_integer(X) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC10 % 1.18/1.28 fof(axiom_2,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC10(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px16(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC10xcomp % 1.18/1.28 fof(axiom_3,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC10xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px16(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC100 % 1.18/1.28 fof(axiom_4,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC100(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC98(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC100 % 1.18/1.28 fof(axiom_5,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC100(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px49(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC100xcomp % 1.18/1.28 fof(axiom_6,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC100xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px49(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC102 % 1.18/1.28 fof(axiom_7,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC102(X) % 1.18/1.28 <=> ? [Y0] : ra_Px35(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC102 % 1.18/1.28 fof(axiom_8,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC102(X) % 1.18/1.28 <=> ( cC34(X) % 1.18/1.28 & cC100(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC102xcomp % 1.18/1.28 fof(axiom_9,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC102xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px35(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC104 % 1.18/1.28 fof(axiom_10,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC104(X) % 1.18/1.28 <=> ( cC4(X) % 1.18/1.28 & cC34(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC106 % 1.18/1.28 fof(axiom_11,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC106(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC104(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC108 % 1.18/1.28 fof(axiom_12,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC108(X) % 1.18/1.28 <=> ( cC34xcomp(X) % 1.18/1.28 & cC106(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC108 % 1.18/1.28 fof(axiom_13,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC108(X) % 1.18/1.28 <=> ? [Y0] : ra_Px36(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC108xcomp % 1.18/1.28 fof(axiom_14,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC108xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px36(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC110 % 1.18/1.28 fof(axiom_15,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC110(X) % 1.18/1.28 <=> ( cC102xcomp(X) % 1.18/1.28 & cC108xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC110 % 1.18/1.28 fof(axiom_16,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC110(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px37(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC110xcomp % 1.18/1.28 fof(axiom_17,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC110xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px37(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC112 % 1.18/1.28 fof(axiom_18,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC112(X) % 1.18/1.28 <=> ( cC4(X) % 1.18/1.28 & cC110xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC112 % 1.18/1.28 fof(axiom_19,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC112(X) % 1.18/1.28 <=> ? [Y0] : ra_Px39(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC112xcomp % 1.18/1.28 fof(axiom_20,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC112xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px39(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC114 % 1.18/1.28 fof(axiom_21,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC114(X) % 1.18/1.28 <=> ( cC112xcomp(X) % 1.18/1.28 & cC96xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC116 % 1.18/1.28 fof(axiom_22,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC116(X) % 1.18/1.28 <=> ( cC114(X) % 1.18/1.28 & cC80(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC118 % 1.18/1.28 fof(axiom_23,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC118(X) % 1.18/1.28 <=> ( cC4(X) % 1.18/1.28 & cC10xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC12 % 1.18/1.28 fof(axiom_24,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC12(X) % 1.18/1.28 <=> ( cC10(X) % 1.18/1.28 & cC4xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC12 % 1.18/1.28 fof(axiom_25,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC12(X) % 1.18/1.28 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC12xcomp % 1.18/1.28 fof(axiom_26,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC12xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC120 % 1.18/1.28 fof(axiom_27,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC120(X) % 1.18/1.28 <=> ( cC118(X) % 1.18/1.28 & cC34(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC122 % 1.18/1.28 fof(axiom_28,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC122(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC120(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC124 % 1.18/1.28 fof(axiom_29,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC124(X) % 1.18/1.28 <=> ( cC4(X) % 1.18/1.28 & cC10xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC126 % 1.18/1.28 fof(axiom_30,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC126(X) % 1.18/1.28 <=> ( cC34xcomp(X) % 1.18/1.28 & cC124(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC128 % 1.18/1.28 fof(axiom_31,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC128(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC126(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC130 % 1.18/1.28 fof(axiom_32,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC130(X) % 1.18/1.28 <=> ( cC128(X) % 1.18/1.28 & cC122(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC130 % 1.18/1.28 fof(axiom_33,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC130(X) % 1.18/1.28 <=> ? [Y0] : ra_Px44(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC130xcomp % 1.18/1.28 fof(axiom_34,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC130xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px44(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC132 % 1.18/1.28 fof(axiom_35,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC132(X) % 1.18/1.28 <=> ( cC2(X) % 1.18/1.28 & cC4xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC132 % 1.18/1.28 fof(axiom_36,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC132(X) % 1.18/1.28 <=> ? [Y0] : ra_Px48(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC132xcomp % 1.18/1.28 fof(axiom_37,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC132xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px48(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC134 % 1.18/1.28 fof(axiom_38,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC134(X) % 1.18/1.28 <=> ( cC130xcomp(X) % 1.18/1.28 & cC132(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC134 % 1.18/1.28 fof(axiom_39,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC134(X) % 1.18/1.28 <=> ? [Y0] : ra_Px45(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC134xcomp % 1.18/1.28 fof(axiom_40,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC134xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px45(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC136 % 1.18/1.28 fof(axiom_41,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC136(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px46(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC136 % 1.18/1.28 fof(axiom_42,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC136(X) % 1.18/1.28 <=> ( cC134xcomp(X) % 1.18/1.28 & cC116(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC136xcomp % 1.18/1.28 fof(axiom_43,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC136xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px46(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC138 % 1.18/1.28 fof(axiom_44,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC138(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC136xcomp(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC138 % 1.18/1.28 fof(axiom_45,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC138(X) % 1.18/1.28 <=> ? [Y0] : ra_Px47(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC138xcomp % 1.18/1.28 fof(axiom_46,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC138xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px47(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC14 % 1.18/1.28 fof(axiom_47,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC14(X) % 1.18/1.28 <=> ( cC12xcomp(X) % 1.18/1.28 & cC8xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC140 % 1.18/1.28 fof(axiom_48,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC140(X) % 1.18/1.28 <=> ( cC74(X) % 1.18/1.28 & cC138xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC16 % 1.18/1.28 fof(axiom_49,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC16(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px4(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC16xcomp % 1.18/1.28 fof(axiom_50,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC16xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px4(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC18 % 1.18/1.28 fof(axiom_51,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC18(X) % 1.18/1.28 <=> ( cC2(X) % 1.18/1.28 & cC16xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC18 % 1.18/1.28 fof(axiom_52,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC18(X) % 1.18/1.28 <=> ? [Y0] : ra_Px56(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC18xcomp % 1.18/1.28 fof(axiom_53,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC18xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px56(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC2 % 1.18/1.28 fof(axiom_54,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC2(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px22(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC2xcomp % 1.18/1.28 fof(axiom_55,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC2xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px22(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC20 % 1.18/1.28 fof(axiom_56,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC20(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC18(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC22 % 1.18/1.28 fof(axiom_57,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC22(X) % 1.18/1.28 <=> ( cC16(X) % 1.18/1.28 & cC20(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC22 % 1.18/1.28 fof(axiom_58,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC22(X) % 1.18/1.28 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC22xcomp % 1.18/1.28 fof(axiom_59,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC22xcomp(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC24 % 1.18/1.28 fof(axiom_60,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC24(X) % 1.18/1.28 <=> ( cC16(X) % 1.18/1.28 & cC2(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC26 % 1.18/1.28 fof(axiom_61,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC26(X) % 1.18/1.28 <=> ? [Y] : % 1.18/1.28 ( rR1(X,Y) % 1.18/1.28 & cC24(Y) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC28 % 1.18/1.28 fof(axiom_62,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC28(X) % 1.18/1.28 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC28 % 1.18/1.28 fof(axiom_63,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC28(X) % 1.18/1.28 <=> ( cC26(X) % 1.18/1.28 & cC16xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC28xcomp % 1.18/1.28 fof(axiom_64,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC28xcomp(X) % 1.18/1.28 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC30 % 1.18/1.28 fof(axiom_65,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC30(X) % 1.18/1.28 <=> ? [Y0] : ra_Px8(X,Y0) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC30 % 1.18/1.28 fof(axiom_66,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC30(X) % 1.18/1.28 <=> ( cC22xcomp(X) % 1.18/1.28 & cC28xcomp(X) ) ) ). % 1.18/1.28 % 1.18/1.28 %----Equality cC30xcomp % 1.18/1.28 fof(axiom_67,axiom, % 1.18/1.28 ! [X] : % 1.18/1.28 ( cC30xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px8(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC32 % 1.18/1.29 fof(axiom_68,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC32(X) % 1.18/1.29 <=> ( cC2(X) % 1.18/1.29 & cC30xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC32 % 1.18/1.29 fof(axiom_69,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC32(X) % 1.18/1.29 <=> ? [Y0] : ra_Px14(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC32xcomp % 1.18/1.29 fof(axiom_70,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC32xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px14(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC34 % 1.18/1.29 fof(axiom_71,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC34(X) % 1.18/1.29 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC34xcomp % 1.18/1.29 fof(axiom_72,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC34xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC36 % 1.18/1.29 fof(axiom_73,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC36(X) % 1.18/1.29 <=> ( cC34xcomp(X) % 1.18/1.29 & cC4(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC38 % 1.18/1.29 fof(axiom_74,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC38(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC36(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC4 % 1.18/1.29 fof(axiom_75,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC4(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC4xcomp % 1.18/1.29 fof(axiom_76,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC4xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC40 % 1.18/1.29 fof(axiom_77,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC40(X) % 1.18/1.29 <=> ? [Y0] : ra_Px11(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC40 % 1.18/1.29 fof(axiom_78,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC40(X) % 1.18/1.29 <=> ( cC34(X) % 1.18/1.29 & cC38(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC40xcomp % 1.18/1.29 fof(axiom_79,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC40xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px11(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC42 % 1.18/1.29 fof(axiom_80,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC42(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC34(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC44 % 1.18/1.29 fof(axiom_81,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC44(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC42(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC46 % 1.18/1.29 fof(axiom_82,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC46(X) % 1.18/1.29 <=> ? [Y0] : ra_Px12(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC46 % 1.18/1.29 fof(axiom_83,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC46(X) % 1.18/1.29 <=> ( cC34xcomp(X) % 1.18/1.29 & cC44(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC46xcomp % 1.18/1.29 fof(axiom_84,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC46xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px12(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC48 % 1.18/1.29 fof(axiom_85,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC48(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px13(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC48 % 1.18/1.29 fof(axiom_86,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC48(X) % 1.18/1.29 <=> ( cC40xcomp(X) % 1.18/1.29 & cC46xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC48xcomp % 1.18/1.29 fof(axiom_87,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC48xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px13(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC50 % 1.18/1.29 fof(axiom_88,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC50(X) % 1.18/1.29 <=> ? [Y0] : ra_Px15(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC50 % 1.18/1.29 fof(axiom_89,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC50(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC48xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC50xcomp % 1.18/1.29 fof(axiom_90,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC50xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px15(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC52 % 1.18/1.29 fof(axiom_91,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC52(X) % 1.18/1.29 <=> ( cC32xcomp(X) % 1.18/1.29 & cC50xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC54 % 1.18/1.29 fof(axiom_92,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC54(X) % 1.18/1.29 <=> ( cC14(X) % 1.18/1.29 & cC52(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC56 % 1.18/1.29 fof(axiom_93,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC56(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC10xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC58 % 1.18/1.29 fof(axiom_94,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC58(X) % 1.18/1.29 <=> ( cC34(X) % 1.18/1.29 & cC56(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC6 % 1.18/1.29 fof(axiom_95,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC6(X) % 1.18/1.29 <=> ( cC2(X) % 1.18/1.29 & cC4xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC60 % 1.18/1.29 fof(axiom_96,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC60(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC58(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC62 % 1.18/1.29 fof(axiom_97,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC62(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC10xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC64 % 1.18/1.29 fof(axiom_98,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC64(X) % 1.18/1.29 <=> ( cC34xcomp(X) % 1.18/1.29 & cC62(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC66 % 1.18/1.29 fof(axiom_99,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC66(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC64(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC68 % 1.18/1.29 fof(axiom_100,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC68(X) % 1.18/1.29 <=> ( cC66(X) % 1.18/1.29 & cC60(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC68 % 1.18/1.29 fof(axiom_101,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC68(X) % 1.18/1.29 <=> ? [Y0] : ra_Px20(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC68xcomp % 1.18/1.29 fof(axiom_102,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC68xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px20(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC70 % 1.18/1.29 fof(axiom_103,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC70(X) % 1.18/1.29 <=> ( cC2(X) % 1.18/1.29 & cC4xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC72 % 1.18/1.29 fof(axiom_104,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC72(X) % 1.18/1.29 <=> ? [Y0] : ra_Px21(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC72 % 1.18/1.29 fof(axiom_105,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC72(X) % 1.18/1.29 <=> ( cC70(X) % 1.18/1.29 & cC68xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC72xcomp % 1.18/1.29 fof(axiom_106,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC72xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px21(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC74 % 1.18/1.29 fof(axiom_107,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC74(X) % 1.18/1.29 <=> ( cC54(X) % 1.18/1.29 & cC72xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC76 % 1.18/1.29 fof(axiom_108,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC76(X) % 1.18/1.29 <=> ? [Y0] : ra_Px24(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC76 % 1.18/1.29 fof(axiom_109,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC76(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC2xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC76xcomp % 1.18/1.29 fof(axiom_110,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC76xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px24(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC78 % 1.18/1.29 fof(axiom_111,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC78(X) % 1.18/1.29 <=> ( cC10(X) % 1.18/1.29 & cC4xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC78 % 1.18/1.29 fof(axiom_112,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC78(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px25(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC78xcomp % 1.18/1.29 fof(axiom_113,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC78xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px25(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC8 % 1.18/1.29 fof(axiom_114,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC8(X) % 1.18/1.29 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC8 % 1.18/1.29 fof(axiom_115,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC8(X) % 1.18/1.29 <=> ( cC4(X) % 1.18/1.29 & cC2xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC8xcomp % 1.18/1.29 fof(axiom_116,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC8xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC80 % 1.18/1.29 fof(axiom_117,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC80(X) % 1.18/1.29 <=> ( cC78xcomp(X) % 1.18/1.29 & cC76xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC82 % 1.18/1.29 fof(axiom_118,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC82(X) % 1.18/1.29 <=> ? [Y0] : ra_Px65(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC82 % 1.18/1.29 fof(axiom_119,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC82(X) % 1.18/1.29 <=> ( cC2(X) % 1.18/1.29 & cC16xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC82xcomp % 1.18/1.29 fof(axiom_120,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC82xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px65(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC84 % 1.18/1.29 fof(axiom_121,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC84(X) % 1.18/1.29 <=> ? [Y0] : ra_Px53(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC84 % 1.18/1.29 fof(axiom_122,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC84(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC82(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC84xcomp % 1.18/1.29 fof(axiom_123,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC84xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px53(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC86 % 1.18/1.29 fof(axiom_124,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC86(X) % 1.18/1.29 <=> ( cC16(X) % 1.18/1.29 & cC84(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC86 % 1.18/1.29 fof(axiom_125,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC86(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px28(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC86xcomp % 1.18/1.29 fof(axiom_126,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC86xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px28(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC88 % 1.18/1.29 fof(axiom_127,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC88(X) % 1.18/1.29 <=> ( cC16(X) % 1.18/1.29 & cC2(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC88 % 1.18/1.29 fof(axiom_128,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC88(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px64(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC88xcomp % 1.18/1.29 fof(axiom_129,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC88xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px64(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC90 % 1.18/1.29 fof(axiom_130,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC90(X) % 1.18/1.29 <=> ? [Y] : % 1.18/1.29 ( rR1(X,Y) % 1.18/1.29 & cC88(Y) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC90 % 1.18/1.29 fof(axiom_131,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC90(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px52(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC90xcomp % 1.18/1.29 fof(axiom_132,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC90xcomp(X) % 1.18/1.29 <=> ? [Y0] : ra_Px52(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC92 % 1.18/1.29 fof(axiom_133,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC92(X) % 1.18/1.29 <=> ? [Y0] : ra_Px29(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC92 % 1.18/1.29 fof(axiom_134,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC92(X) % 1.18/1.29 <=> ( cC90(X) % 1.18/1.29 & cC16xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC92xcomp % 1.18/1.29 fof(axiom_135,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC92xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px29(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC94 % 1.18/1.29 fof(axiom_136,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC94(X) % 1.18/1.29 <=> ( cC86xcomp(X) % 1.18/1.29 & cC92xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC94 % 1.18/1.29 fof(axiom_137,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC94(X) % 1.18/1.29 <=> ? [Y0] : ra_Px30(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC94xcomp % 1.18/1.29 fof(axiom_138,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC94xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px30(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC96 % 1.18/1.29 fof(axiom_139,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC96(X) % 1.18/1.29 <=> ? [Y0] : ra_Px38(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC96 % 1.18/1.29 fof(axiom_140,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC96(X) % 1.18/1.29 <=> ( cC2(X) % 1.18/1.29 & cC94xcomp(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC96xcomp % 1.18/1.29 fof(axiom_141,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC96xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px38(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC98 % 1.18/1.29 fof(axiom_142,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC98(X) % 1.18/1.29 <=> ? [Y0] : ra_Px63(X,Y0) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC98 % 1.18/1.29 fof(axiom_143,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC98(X) % 1.18/1.29 <=> ( cC34xcomp(X) % 1.18/1.29 & cC4(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cC98xcomp % 1.18/1.29 fof(axiom_144,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cC98xcomp(X) % 1.18/1.29 <=> ~ ? [Y] : ra_Px63(X,Y) ) ). % 1.18/1.29 % 1.18/1.29 %----Equality cTEST % 1.18/1.29 fof(axiom_145,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( cTEST(X) % 1.18/1.29 <=> ( cC6(X) % 1.18/1.29 & cC140(X) ) ) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_146,axiom, % 1.18/1.29 cC16(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_147,axiom, % 1.18/1.29 cC102xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_148,axiom, % 1.18/1.29 cC108xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_149,axiom, % 1.18/1.29 cC4(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_150,axiom, % 1.18/1.29 cC18xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_151,axiom, % 1.18/1.29 cC112xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_152,axiom, % 1.18/1.29 cC76xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_153,axiom, % 1.18/1.29 cC96xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_154,axiom, % 1.18/1.29 cC132xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_155,axiom, % 1.18/1.29 cC100xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_156,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( rR1(iV822576,X) % 1.18/1.29 => cC98xcomp(X) ) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_157,axiom, % 1.18/1.29 cC90xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_158,axiom, % 1.18/1.29 cC78xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_159,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( rR1(iV822576,X) % 1.18/1.29 => cC82xcomp(X) ) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_160,axiom, % 1.18/1.29 cC134xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_161,axiom, % 1.18/1.29 cC86xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_162,axiom, % 1.18/1.29 cC34(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_163,axiom, % 1.18/1.29 cC84xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_164,axiom, % 1.18/1.29 ! [X] : % 1.18/1.29 ( rR1(iV822576,X) % 1.18/1.29 => cC88xcomp(X) ) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_165,axiom, % 1.18/1.29 cC2(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_166,axiom, % 1.18/1.29 cowlThing(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_167,axiom, % 1.18/1.29 cC10xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(axiom_168,axiom, % 1.18/1.29 cC92xcomp(iV822576) ). % 1.18/1.29 % 1.18/1.29 %----Thing and Nothing % 1.18/1.29 %----String and Integer disjoint % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 %----iV822576 % 1.18/1.29 fof(the_axiom,conjecture, % 1.18/1.29 ( ! [X] : % 1.18/1.29 ( cowlThing(X) % 1.18/1.29 & ~ cowlNothing(X) ) % 1.18/1.29 & ! [X] : % 1.18/1.29 ( xsd_string(X) % 1.18/1.29 <=> ~ xsd_integer(X) ) % 1.18/1.29 & cC58(iV822576) % 1.18/1.29 & cC116(iV822576) % 1.18/1.29 & cC114(iV822576) % 1.18/1.29 & cowlThing(iV822576) % 1.18/1.29 & cC94(iV822576) % 1.18/1.29 & cC80(iV822576) % 1.18/1.29 & cC110(iV822576) % 1.18/1.29 & cC136(iV822576) % 1.18/1.29 & cC56(iV822576) ) ). % 1.18/1.29 % 1.18/1.29 %------------------------------------------------------------------------------ % 1.18/1.29 %------------------------------------------- % 1.18/1.29 % Proof found % 1.18/1.29 % SZS status Theorem for theBenchmark % 1.18/1.29 % SZS output start Proof % 1.18/1.29 %ClaNum:381(EqnAxiom:0) % 1.18/1.29 %VarNum:967(SingletonVarNum:451) % 1.18/1.29 %MaxLitNum:11 % 1.18/1.29 %MaxfuncDepth:1 % 1.18/1.29 %SharedTerms:35 % 1.18/1.29 %goalClause: 380 381 % 1.18/1.29 [1]P1(a1) % 1.18/1.29 [2]P2(a1) % 1.18/1.29 [3]P11(a1) % 1.18/1.29 [4]P5(a1) % 1.18/1.29 [5]P55(a1) % 1.18/1.29 [6]P7(a1) % 1.18/1.29 [7]P12(a1) % 1.18/1.29 [8]P59(a1) % 1.18/1.29 [9]P16(a1) % 1.18/1.29 [10]P17(a1) % 1.18/1.29 [11]P31(a1) % 1.18/1.29 [12]P33(a1) % 1.18/1.29 [13]P40(a1) % 1.18/1.29 [14]P60(a1) % 1.18/1.29 [15]P88(a1) % 1.18/1.29 [16]P90(a1) % 1.18/1.29 [17]P96(a1) % 1.18/1.29 [18]P98(a1) % 1.18/1.29 [19]P103(a1) % 1.18/1.29 [20]~P108(x201) % 1.18/1.29 [21]P113(x211)+P112(x211) % 1.18/1.29 [22]~P18(x221)+P3(x221) % 1.18/1.29 [23]~P89(x231)+P3(x231) % 1.18/1.29 [24]~P19(x241)+P1(x241) % 1.18/1.29 [25]~P22(x251)+P1(x251) % 1.18/1.29 [26]~P61(x261)+P1(x261) % 1.18/1.29 [27]~P75(x271)+P1(x271) % 1.18/1.29 [28]~P6(x281)+P4(x281) % 1.18/1.29 [29]~P6(x291)+P11(x291) % 1.18/1.29 [30]~P8(x301)+P11(x301) % 1.18/1.29 [31]~P23(x311)+P11(x311) % 1.18/1.29 [32]~P62(x321)+P11(x321) % 1.18/1.29 [33]~P63(x331)+P11(x331) % 1.18/1.29 [34]~P76(x341)+P11(x341) % 1.18/1.29 [35]~P13(x351)+P5(x351) % 1.18/1.29 [36]~P109(x361)+P55(x361) % 1.18/1.29 [37]~P8(x371)+P55(x371) % 1.18/1.29 [38]~P14(x381)+P55(x381) % 1.18/1.29 [39]~P19(x391)+P55(x391) % 1.18/1.29 [40]~P22(x401)+P55(x401) % 1.18/1.29 [41]~P56(x411)+P55(x411) % 1.18/1.29 [42]~P63(x421)+P55(x421) % 1.18/1.29 [43]~P65(x431)+P55(x431) % 1.18/1.29 [44]~P61(x441)+P55(x441) % 1.18/1.29 [45]~P75(x451)+P55(x451) % 1.18/1.29 [46]~P79(x461)+P55(x461) % 1.18/1.29 [47]~P91(x471)+P55(x471) % 1.18/1.29 [48]~P10(x481)+P9(x481) % 1.18/1.29 [49]~P109(x491)+P57(x491) % 1.18/1.29 [50]~P10(x501)+P57(x501) % 1.18/1.29 [51]~P25(x511)+P57(x511) % 1.18/1.29 [52]~P56(x521)+P57(x521) % 1.18/1.29 [53]~P66(x531)+P57(x531) % 1.18/1.29 [54]~P80(x541)+P57(x541) % 1.18/1.29 [55]~P13(x551)+P7(x551) % 1.18/1.29 [56]~P14(x561)+P15(x561) % 1.18/1.29 [57]~P20(x571)+P12(x571) % 1.18/1.29 [58]~P21(x581)+P20(x581) % 1.18/1.29 [59]~P20(x591)+P59(x591) % 1.18/1.29 [60]~P34(x601)+P21(x601) % 1.18/1.29 [61]~P21(x611)+P92(x611) % 1.18/1.29 [62]~P23(x621)+P19(x621) % 1.18/1.29 [63]~P18(x631)+P68(x631) % 1.18/1.29 [64]~P26(x641)+P68(x641) % 1.18/1.29 [65]~P77(x651)+P68(x651) % 1.18/1.29 [66]~P81(x661)+P68(x661) % 1.18/1.29 [67]~P89(x671)+P68(x671) % 1.18/1.29 [68]~P35(x681)+P27(x681) % 1.18/1.29 [69]~P29(x691)+P24(x691) % 1.18/1.29 [70]~P25(x701)+P22(x701) % 1.18/1.29 [71]~P29(x711)+P28(x711) % 1.18/1.29 [72]~P32(x721)+P30(x721) % 1.18/1.29 [73]~P32(x731)+P26(x731) % 1.18/1.29 [74]~P26(x741)+P16(x741) % 1.18/1.29 [75]~P41(x751)+P16(x751) % 1.18/1.29 [76]~P43(x761)+P16(x761) % 1.18/1.29 [77]~P47(x771)+P16(x771) % 1.18/1.29 [78]~P77(x781)+P16(x781) % 1.18/1.29 [79]~P81(x791)+P16(x791) % 1.18/1.29 [80]~P93(x801)+P16(x801) % 1.18/1.29 [81]~P99(x811)+P16(x811) % 1.18/1.29 [82]~P105(x821)+P16(x821) % 1.18/1.29 [83]~P34(x831)+P31(x831) % 1.18/1.29 [84]~P39(x841)+P36(x841) % 1.18/1.29 [85]~P72(x851)+P35(x851) % 1.18/1.29 [86]~P35(x861)+P100(x861) % 1.18/1.29 [87]~P110(x871)+P39(x871) % 1.18/1.29 [88]~P39(x881)+P85(x881) % 1.18/1.29 [89]~P44(x891)+P33(x891) % 1.18/1.29 [90]~P43(x901)+P33(x901) % 1.18/1.29 [91]~P97(x911)+P33(x911) % 1.18/1.29 [92]~P99(x921)+P33(x921) % 1.18/1.29 [93]~P41(x931)+P42(x931) % 1.18/1.29 [94]~P48(x941)+P42(x941) % 1.18/1.29 [95]~P93(x951)+P42(x951) % 1.18/1.29 [96]~P104(x961)+P42(x961) % 1.18/1.29 [97]~P79(x971)+P50(x971) % 1.18/1.29 [98]~P91(x981)+P50(x981) % 1.18/1.29 [99]~P44(x991)+P45(x991) % 1.18/1.29 [100]~P52(x1001)+P46(x1001) % 1.18/1.29 [101]~P48(x1011)+P49(x1011) % 1.18/1.29 [102]~P52(x1021)+P51(x1021) % 1.18/1.29 [103]~P47(x1031)+P53(x1031) % 1.18/1.29 [104]~P73(x1041)+P54(x1041) % 1.18/1.29 [105]~P62(x1051)+P58(x1051) % 1.18/1.29 [106]~P69(x1061)+P64(x1061) % 1.18/1.29 [107]~P66(x1071)+P67(x1071) % 1.18/1.29 [108]~P69(x1081)+P70(x1081) % 1.18/1.29 [109]~P65(x1091)+P71(x1091) % 1.18/1.29 [110]~P73(x1101)+P74(x1101) % 1.18/1.29 [111]~P72(x1111)+P73(x1111) % 1.18/1.29 [112]~P85(x1121)+P72(x1121) % 1.18/1.29 [113]~P76(x1131)+P61(x1131) % 1.18/1.29 [114]~P110(x1141)+P77(x1141) % 1.18/1.29 [115]~P82(x1151)+P78(x1151) % 1.18/1.29 [116]~P80(x1161)+P75(x1161) % 1.18/1.29 [117]~P82(x1171)+P83(x1171) % 1.18/1.29 [118]~P86(x1181)+P84(x1181) % 1.18/1.29 [119]~P86(x1191)+P81(x1191) % 1.18/1.29 [120]~P85(x1201)+P87(x1201) % 1.18/1.29 [121]~P92(x1211)+P60(x1211) % 1.18/1.29 [122]~P92(x1221)+P88(x1221) % 1.18/1.29 [123]~P97(x1231)+P94(x1231) % 1.18/1.29 [124]~P106(x1241)+P96(x1241) % 1.18/1.29 [125]~P104(x1251)+P102(x1251) % 1.18/1.29 [126]~P106(x1261)+P103(x1261) % 1.18/1.29 [127]~P105(x1271)+P107(x1271) % 1.18/1.29 [128]~P113(x1281)+~P112(x1281) % 1.18/1.29 [195]P95(x1951)+~P114(a1,x1951) % 1.18/1.29 [196]P101(x1961)+~P114(a1,x1961) % 1.18/1.29 [197]P111(x1971)+~P114(a1,x1971) % 1.18/1.29 [129]~P4(x1291)+P109(f2(x1291)) % 1.18/1.29 [130]~P9(x1301)+P8(f35(x1301)) % 1.18/1.29 [131]~P24(x1311)+P23(f3(x1311)) % 1.18/1.29 [132]~P28(x1321)+P25(f11(x1321)) % 1.18/1.29 [133]~P38(x1331)+P37(f12(x1331)) % 1.18/1.29 [134]~P45(x1341)+P41(f22(x1341)) % 1.18/1.29 [135]~P49(x1351)+P43(f32(x1351)) % 1.18/1.29 [136]~P58(x1361)+P56(f36(x1361)) % 1.18/1.29 [137]~P67(x1371)+P63(f45(x1371)) % 1.18/1.29 [138]~P78(x1381)+P76(f51(x1381)) % 1.18/1.29 [139]~P83(x1391)+P80(f59(x1391)) % 1.18/1.29 [140]~P94(x1401)+P93(f60(x1401)) % 1.18/1.29 [141]~P102(x1411)+P99(f75(x1411)) % 1.18/1.29 [198]P3(x1981)+P115(x1981,f13(x1981)) % 1.18/1.29 [199]P4(x1991)+P122(x1991,f46(x1991)) % 1.18/1.29 [200]P5(x2001)+P123(x2001,f76(x2001)) % 1.18/1.29 [201]P55(x2011)+P116(x2011,f47(x2011)) % 1.18/1.29 [202]P57(x2021)+P144(x2021,f37(x2021)) % 1.18/1.29 [203]P7(x2031)+P134(x2031,f4(x2031)) % 1.18/1.29 [204]P13(x2041)+P135(x2041,f5(x2041)) % 1.18/1.29 [205]P12(x2051)+P136(x2051,f6(x2051)) % 1.18/1.29 [206]P59(x2061)+P137(x2061,f82(x2061)) % 1.18/1.29 [207]P27(x2071)+P124(x2071,f9(x2071)) % 1.18/1.29 [208]P30(x2081)+P138(x2081,f15(x2081)) % 1.18/1.29 [209]P16(x2091)+P125(x2091,f23(x2091)) % 1.18/1.29 [210]P17(x2101)+P140(x2101,f16(x2101)) % 1.18/1.29 [211]P31(x2111)+P141(x2111,f18(x2111)) % 1.18/1.29 [212]P34(x2121)+P142(x2121,f20(x2121)) % 1.18/1.29 [213]P36(x2131)+P143(x2131,f24(x2131)) % 1.18/1.29 [214]P100(x2141)+P126(x2141,f61(x2141)) % 1.18/1.29 [215]P33(x2151)+P139(x2151,f26(x2151)) % 1.18/1.29 [216]P40(x2161)+P145(x2161,f28(x2161)) % 1.18/1.29 [217]P46(x2171)+P148(x2171,f33(x2171)) % 1.18/1.29 [218]P48(x2181)+P149(x2181,f38(x2181)) % 1.18/1.29 [219]P53(x2191)+P153(x2191,f39(x2191)) % 1.18/1.29 [220]P54(x2201)+P117(x2201,f42(x2201)) % 1.18/1.29 [221]P64(x2211)+P118(x2211,f48(x2211)) % 1.18/1.29 [222]P70(x2221)+P119(x2221,f52(x2221)) % 1.18/1.29 [223]P69(x2231)+P120(x2231,f54(x2231)) % 1.18/1.29 [224]P74(x2241)+P121(x2241,f55(x2241)) % 1.18/1.29 [225]P84(x2251)+P127(x2251,f62(x2251)) % 1.18/1.29 [226]P87(x2261)+P128(x2261,f64(x2261)) % 1.18/1.29 [227]P60(x2271)+P129(x2271,f66(x2271)) % 1.18/1.29 [228]P89(x2281)+P130(x2281,f68(x2281)) % 1.18/1.29 [229]P95(x2291)+P150(x2291,f72(x2291)) % 1.18/1.29 [230]P90(x2301)+P146(x2301,f77(x2301)) % 1.18/1.29 [231]P97(x2311)+P131(x2311,f78(x2311)) % 1.18/1.29 [232]P99(x2321)+P151(x2321,f79(x2321)) % 1.18/1.29 [233]P102(x2331)+P147(x2331,f83(x2331)) % 1.18/1.29 [234]P103(x2341)+P132(x2341,f84(x2341)) % 1.18/1.29 [235]P107(x2351)+P133(x2351,f87(x2351)) % 1.18/1.29 [236]P111(x2361)+P152(x2361,f90(x2361)) % 1.18/1.29 [276]~P1(x2761)+P115(x2761,f27(x2761)) % 1.18/1.29 [277]~P4(x2771)+P114(x2771,f2(x2771)) % 1.18/1.29 [278]~P9(x2781)+P114(x2781,f35(x2781)) % 1.18/1.29 [279]~P24(x2791)+P114(x2791,f3(x2791)) % 1.18/1.29 [280]~P28(x2801)+P114(x2801,f11(x2801)) % 1.18/1.29 [281]~P38(x2811)+P114(x2811,f12(x2811)) % 1.18/1.29 [282]~P45(x2821)+P114(x2821,f22(x2821)) % 1.18/1.29 [283]~P49(x2831)+P114(x2831,f32(x2831)) % 1.18/1.29 [284]~P58(x2841)+P114(x2841,f36(x2841)) % 1.18/1.29 [285]~P67(x2851)+P114(x2851,f45(x2851)) % 1.18/1.29 [286]~P78(x2861)+P114(x2861,f51(x2861)) % 1.18/1.29 [287]~P83(x2871)+P114(x2871,f59(x2871)) % 1.18/1.29 [288]~P94(x2881)+P114(x2881,f60(x2881)) % 1.18/1.29 [289]~P102(x2891)+P114(x2891,f75(x2891)) % 1.18/1.29 [290]~P2(x2901)+P122(x2901,f58(x2901)) % 1.18/1.29 [291]~P6(x2911)+P123(x2911,f69(x2911)) % 1.18/1.29 [292]~P10(x2921)+P134(x2921,f92(x2921)) % 1.18/1.29 [293]~P15(x2931)+P135(x2931,f7(x2931)) % 1.18/1.29 [294]~P14(x2941)+P136(x2941,f8(x2941)) % 1.18/1.29 [295]~P18(x2951)+P124(x2951,f10(x2951)) % 1.18/1.29 [296]~P29(x2961)+P138(x2961,f14(x2961)) % 1.18/1.29 [297]~P26(x2971)+P140(x2971,f17(x2971)) % 1.18/1.29 [298]~P32(x2981)+P141(x2981,f19(x2981)) % 1.18/1.29 [299]~P37(x2991)+P142(x2991,f21(x2991)) % 1.18/1.29 [300]~P38(x3001)+P143(x3001,f25(x3001)) % 1.18/1.29 [301]~P42(x3011)+P139(x3011,f29(x3011)) % 1.18/1.29 [302]~P41(x3021)+P145(x3021,f30(x3021)) % 1.18/1.29 [303]~P50(x3031)+P125(x3031,f31(x3031)) % 1.18/1.29 [304]~P44(x3041)+P148(x3041,f34(x3041)) % 1.18/1.29 [305]~P51(x3051)+P149(x3051,f40(x3051)) % 1.18/1.29 [306]~P52(x3061)+P153(x3061,f41(x3061)) % 1.18/1.29 [307]~P47(x3071)+P117(x3071,f43(x3071)) % 1.18/1.29 [308]~P11(x3081)+P144(x3081,f44(x3081)) % 1.18/1.29 [309]~P68(x3091)+P116(x3091,f49(x3091)) % 1.18/1.29 [310]~P62(x3101)+P118(x3101,f50(x3101)) % 1.18/1.29 [311]~P66(x3111)+P119(x3111,f53(x3111)) % 1.18/1.29 [312]~P71(x3121)+P120(x3121,f56(x3121)) % 1.18/1.29 [313]~P65(x3131)+P121(x3131,f57(x3131)) % 1.18/1.30 [314]~P82(x3141)+P127(x3141,f63(x3141)) % 1.18/1.30 [315]~P86(x3151)+P128(x3151,f65(x3151)) % 1.18/1.30 [316]~P79(x3161)+P129(x3161,f67(x3161)) % 1.18/1.30 [317]~P88(x3171)+P130(x3171,f70(x3171)) % 1.18/1.30 [318]~P91(x3181)+P126(x3181,f71(x3181)) % 1.18/1.30 [319]~P93(x3191)+P150(x3191,f73(x3191)) % 1.18/1.30 [320]~P94(x3201)+P146(x3201,f74(x3201)) % 1.18/1.30 [321]~P96(x3211)+P131(x3211,f80(x3211)) % 1.18/1.30 [322]~P101(x3221)+P151(x3221,f81(x3221)) % 1.18/1.30 [323]~P98(x3231)+P147(x3231,f85(x3231)) % 1.18/1.30 [324]~P104(x3241)+P132(x3241,f86(x3241)) % 1.18/1.30 [325]~P106(x3251)+P133(x3251,f88(x3251)) % 1.18/1.30 [326]~P105(x3261)+P137(x3261,f89(x3261)) % 1.18/1.30 [327]~P109(x3271)+P152(x3271,f91(x3271)) % 1.18/1.30 [237]P1(x2371)+~P115(x2371,x2372) % 1.18/1.30 [238]P109(x2381)+~P152(x2381,x2382) % 1.18/1.30 [239]P2(x2391)+~P122(x2391,x2392) % 1.18/1.30 [240]P6(x2401)+~P123(x2401,x2402) % 1.18/1.30 [241]P11(x2411)+~P144(x2411,x2412) % 1.18/1.30 [242]P10(x2421)+~P134(x2421,x2422) % 1.18/1.30 [243]P15(x2431)+~P135(x2431,x2432) % 1.18/1.30 [244]P14(x2441)+~P136(x2441,x2442) % 1.18/1.30 [245]P18(x2451)+~P124(x2451,x2452) % 1.18/1.30 [246]P68(x2461)+~P116(x2461,x2462) % 1.18/1.30 [247]P29(x2471)+~P138(x2471,x2472) % 1.18/1.30 [248]P26(x2481)+~P140(x2481,x2482) % 1.18/1.30 [249]P32(x2491)+~P141(x2491,x2492) % 1.18/1.30 [250]P37(x2501)+~P142(x2501,x2502) % 1.18/1.30 [251]P38(x2511)+~P143(x2511,x2512) % 1.18/1.30 [252]P42(x2521)+~P139(x2521,x2522) % 1.18/1.30 [253]P41(x2531)+~P145(x2531,x2532) % 1.18/1.30 [254]P50(x2541)+~P125(x2541,x2542) % 1.18/1.30 [255]P44(x2551)+~P148(x2551,x2552) % 1.18/1.30 [256]P51(x2561)+~P149(x2561,x2562) % 1.18/1.30 [257]P52(x2571)+~P153(x2571,x2572) % 1.18/1.30 [258]P47(x2581)+~P117(x2581,x2582) % 1.18/1.30 [259]P62(x2591)+~P118(x2591,x2592) % 1.18/1.30 [260]P66(x2601)+~P119(x2601,x2602) % 1.18/1.30 [261]P71(x2611)+~P120(x2611,x2612) % 1.18/1.30 [262]P65(x2621)+~P121(x2621,x2622) % 1.18/1.30 [263]P82(x2631)+~P127(x2631,x2632) % 1.18/1.30 [264]P86(x2641)+~P128(x2641,x2642) % 1.18/1.30 [265]P79(x2651)+~P129(x2651,x2652) % 1.18/1.30 [266]P88(x2661)+~P130(x2661,x2662) % 1.18/1.30 [267]P91(x2671)+~P126(x2671,x2672) % 1.18/1.30 [268]P93(x2681)+~P150(x2681,x2682) % 1.18/1.30 [269]P94(x2691)+~P146(x2691,x2692) % 1.18/1.30 [270]P96(x2701)+~P131(x2701,x2702) % 1.18/1.30 [271]P101(x2711)+~P151(x2711,x2712) % 1.18/1.30 [272]P98(x2721)+~P147(x2721,x2722) % 1.18/1.30 [273]P104(x2731)+~P132(x2731,x2732) % 1.18/1.30 [274]P106(x2741)+~P133(x2741,x2742) % 1.18/1.30 [275]P105(x2751)+~P137(x2751,x2752) % 1.18/1.30 [328]~P3(x3281)+~P115(x3281,x3282) % 1.18/1.30 [329]~P4(x3291)+~P122(x3291,x3292) % 1.18/1.30 [330]~P5(x3301)+~P123(x3301,x3302) % 1.18/1.30 [331]~P55(x3311)+~P116(x3311,x3312) % 1.18/1.30 [332]~P57(x3321)+~P144(x3321,x3322) % 1.18/1.30 [333]~P7(x3331)+~P134(x3331,x3332) % 1.18/1.30 [334]~P13(x3341)+~P135(x3341,x3342) % 1.18/1.30 [335]~P12(x3351)+~P136(x3351,x3352) % 1.18/1.30 [336]~P59(x3361)+~P137(x3361,x3362) % 1.18/1.30 [337]~P27(x3371)+~P124(x3371,x3372) % 1.18/1.30 [338]~P30(x3381)+~P138(x3381,x3382) % 1.18/1.30 [339]~P16(x3391)+~P125(x3391,x3392) % 1.18/1.30 [340]~P17(x3401)+~P140(x3401,x3402) % 1.18/1.30 [341]~P31(x3411)+~P141(x3411,x3412) % 1.18/1.30 [342]~P34(x3421)+~P142(x3421,x3422) % 1.18/1.30 [343]~P36(x3431)+~P143(x3431,x3432) % 1.18/1.30 [344]~P100(x3441)+~P126(x3441,x3442) % 1.18/1.30 [345]~P33(x3451)+~P139(x3451,x3452) % 1.18/1.30 [346]~P40(x3461)+~P145(x3461,x3462) % 1.18/1.30 [347]~P46(x3471)+~P148(x3471,x3472) % 1.18/1.30 [348]~P48(x3481)+~P149(x3481,x3482) % 1.18/1.30 [349]~P53(x3491)+~P153(x3491,x3492) % 1.18/1.30 [350]~P54(x3501)+~P117(x3501,x3502) % 1.18/1.30 [351]~P64(x3511)+~P118(x3511,x3512) % 1.18/1.30 [352]~P70(x3521)+~P119(x3521,x3522) % 1.18/1.30 [353]~P69(x3531)+~P120(x3531,x3532) % 1.18/1.30 [354]~P74(x3541)+~P121(x3541,x3542) % 1.18/1.30 [355]~P84(x3551)+~P127(x3551,x3552) % 1.18/1.30 [356]~P87(x3561)+~P128(x3561,x3562) % 1.18/1.30 [357]~P60(x3571)+~P129(x3571,x3572) % 1.18/1.30 [358]~P89(x3581)+~P130(x3581,x3582) % 1.18/1.30 [359]~P95(x3591)+~P150(x3591,x3592) % 1.18/1.30 [360]~P90(x3601)+~P146(x3601,x3602) % 1.18/1.30 [361]~P97(x3611)+~P131(x3611,x3612) % 1.18/1.30 [362]~P99(x3621)+~P151(x3621,x3622) % 1.18/1.30 [363]~P102(x3631)+~P147(x3631,x3632) % 1.18/1.30 [364]~P103(x3641)+~P132(x3641,x3642) % 1.18/1.30 [365]~P107(x3651)+~P133(x3651,x3652) % 1.18/1.30 [366]~P111(x3661)+~P152(x3661,x3662) % 1.18/1.30 [142]~P55(x1421)+~P57(x1421)+P109(x1421) % 1.18/1.30 [143]~P4(x1431)+~P11(x1431)+P6(x1431) % 1.18/1.30 [144]~P11(x1441)+~P55(x1441)+P8(x1441) % 1.18/1.30 [145]~P9(x1451)+~P57(x1451)+P10(x1451) % 1.18/1.30 [146]~P5(x1461)+~P7(x1461)+P13(x1461) % 1.18/1.30 [147]~P55(x1471)+~P15(x1471)+P14(x1471) % 1.18/1.30 [148]~P12(x1481)+~P59(x1481)+P20(x1481) % 1.18/1.30 [149]~P20(x1491)+~P92(x1491)+P21(x1491) % 1.18/1.30 [150]~P60(x1501)+~P88(x1501)+P92(x1501) % 1.18/1.30 [151]~P1(x1511)+~P55(x1511)+P19(x1511) % 1.18/1.30 [152]~P3(x1521)+~P68(x1521)+P18(x1521) % 1.18/1.30 [153]~P11(x1531)+~P19(x1531)+P23(x1531) % 1.18/1.30 [154]~P1(x1541)+~P55(x1541)+P22(x1541) % 1.18/1.30 [155]~P57(x1551)+~P22(x1551)+P25(x1551) % 1.18/1.30 [156]~P24(x1561)+~P28(x1561)+P29(x1561) % 1.18/1.30 [157]~P68(x1571)+~P16(x1571)+P26(x1571) % 1.18/1.30 [158]~P30(x1581)+~P26(x1581)+P32(x1581) % 1.18/1.30 [159]~P21(x1591)+~P31(x1591)+P34(x1591) % 1.18/1.30 [160]~P27(x1601)+~P100(x1601)+P35(x1601) % 1.18/1.30 [161]~P36(x1611)+~P85(x1611)+P39(x1611) % 1.18/1.30 [162]~P72(x1621)+~P87(x1621)+P85(x1621) % 1.18/1.30 [163]~P16(x1631)+~P42(x1631)+P41(x1631) % 1.18/1.30 [164]~P33(x1641)+~P45(x1641)+P44(x1641) % 1.18/1.30 [165]~P16(x1651)+~P33(x1651)+P43(x1651) % 1.18/1.30 [166]~P42(x1661)+~P49(x1661)+P48(x1661) % 1.18/1.30 [167]~P46(x1671)+~P51(x1671)+P52(x1671) % 1.18/1.30 [168]~P16(x1681)+~P53(x1681)+P47(x1681) % 1.18/1.30 [169]~P55(x1691)+~P57(x1691)+P56(x1691) % 1.18/1.30 [170]~P11(x1701)+~P58(x1701)+P62(x1701) % 1.18/1.30 [171]~P11(x1711)+~P55(x1711)+P63(x1711) % 1.18/1.30 [172]~P57(x1721)+~P67(x1721)+P66(x1721) % 1.18/1.30 [173]~P64(x1731)+~P70(x1731)+P69(x1731) % 1.18/1.30 [174]~P55(x1741)+~P71(x1741)+P65(x1741) % 1.18/1.30 [175]~P54(x1751)+~P74(x1751)+P73(x1751) % 1.18/1.30 [176]~P35(x1761)+~P73(x1761)+P72(x1761) % 1.18/1.30 [177]~P1(x1771)+~P55(x1771)+P61(x1771) % 1.18/1.30 [178]~P11(x1781)+~P61(x1781)+P76(x1781) % 1.18/1.30 [179]~P68(x1791)+~P16(x1791)+P77(x1791) % 1.18/1.30 [180]~P1(x1801)+~P55(x1801)+P75(x1801) % 1.18/1.30 [181]~P57(x1811)+~P75(x1811)+P80(x1811) % 1.18/1.30 [182]~P78(x1821)+~P83(x1821)+P82(x1821) % 1.18/1.30 [183]~P68(x1831)+~P16(x1831)+P81(x1831) % 1.18/1.30 [184]~P84(x1841)+~P81(x1841)+P86(x1841) % 1.18/1.30 [185]~P55(x1851)+~P50(x1851)+P79(x1851) % 1.18/1.30 [186]~P3(x1861)+~P68(x1861)+P89(x1861) % 1.18/1.30 [187]~P55(x1871)+~P50(x1871)+P91(x1871) % 1.18/1.30 [188]~P16(x1881)+~P42(x1881)+P93(x1881) % 1.18/1.30 [189]~P33(x1891)+~P94(x1891)+P97(x1891) % 1.18/1.30 [190]~P16(x1901)+~P33(x1901)+P99(x1901) % 1.18/1.30 [191]~P42(x1911)+~P102(x1911)+P104(x1911) % 1.18/1.30 [192]~P96(x1921)+~P103(x1921)+P106(x1921) % 1.18/1.30 [193]~P16(x1931)+~P107(x1931)+P105(x1931) % 1.18/1.30 [194]~P39(x1941)+~P77(x1941)+P110(x1941) % 1.18/1.30 [367]~P114(x3671,x3672)+P4(x3671)+~P109(x3672) % 1.18/1.30 [368]~P114(x3681,x3682)+P9(x3681)+~P8(x3682) % 1.18/1.30 [369]~P114(x3691,x3692)+P24(x3691)+~P23(x3692) % 1.18/1.30 [370]~P114(x3701,x3702)+P28(x3701)+~P25(x3702) % 1.18/1.30 [371]~P114(x3711,x3712)+P38(x3711)+~P37(x3712) % 1.18/1.30 [372]~P114(x3721,x3722)+P45(x3721)+~P41(x3722) % 1.18/1.30 [373]~P114(x3731,x3732)+P49(x3731)+~P43(x3732) % 1.18/1.30 [374]~P114(x3741,x3742)+P58(x3741)+~P56(x3742) % 1.18/1.30 [375]~P114(x3751,x3752)+P67(x3751)+~P63(x3752) % 1.18/1.30 [376]~P114(x3761,x3762)+P78(x3761)+~P76(x3762) % 1.18/1.30 [377]~P114(x3771,x3772)+P83(x3771)+~P80(x3772) % 1.18/1.30 [378]~P114(x3781,x3782)+P94(x3781)+~P93(x3782) % 1.18/1.30 [379]~P114(x3791,x3792)+P102(x3791)+~P99(x3792) % 1.18/1.30 [380]P108(a93)+P112(a94)+~P113(a94)+~P13(a1)+~P20(a1)+~P21(a1)+~P92(a1)+~P34(a1)+~P61(a1)+~P76(a1)+~P106(a1) % 1.18/1.30 [381]P108(a93)+P113(a94)+~P112(a94)+~P13(a1)+~P20(a1)+~P21(a1)+~P92(a1)+~P34(a1)+~P61(a1)+~P76(a1)+~P106(a1) % 1.18/1.30 %EqnAxiom % 1.18/1.30 % 1.18/1.30 %------------------------------------------- % 1.18/1.30 cnf(436,plain, % 1.18/1.30 (P13(a1)), % 1.18/1.30 inference(scs_inference,[],[4,5,6,7,8,11,14,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146])). % 1.18/1.30 cnf(438,plain, % 1.18/1.30 (P20(a1)), % 1.18/1.30 inference(scs_inference,[],[4,5,6,7,8,11,14,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148])). % 1.18/1.30 cnf(440,plain, % 1.18/1.30 (P92(a1)), % 1.18/1.30 inference(scs_inference,[],[4,5,6,7,8,11,14,15,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150])). % 1.18/1.30 cnf(442,plain, % 1.18/1.30 (P61(a1)), % 1.18/1.30 inference(scs_inference,[],[1,4,5,6,7,8,11,14,15,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177])). % 1.18/1.30 cnf(444,plain, % 1.18/1.30 (P76(a1)), % 1.18/1.30 inference(scs_inference,[],[1,3,4,5,6,7,8,11,14,15,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177,178])). % 1.18/1.30 cnf(446,plain, % 1.18/1.30 (P106(a1)), % 1.18/1.30 inference(scs_inference,[],[1,3,4,5,6,7,8,11,14,15,17,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177,178,192])). % 1.18/1.30 cnf(482,plain, % 1.18/1.30 (P21(a1)), % 1.18/1.30 inference(scs_inference,[],[1,3,4,5,6,7,8,11,14,15,17,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177,178,192,143,144,151,153,154,171,180,165,190,334,293,67,207,210,301,303,362,149])). % 1.18/1.30 cnf(484,plain, % 1.18/1.30 (P34(a1)), % 1.18/1.30 inference(scs_inference,[],[1,3,4,5,6,7,8,11,14,15,17,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177,178,192,143,144,151,153,154,171,180,165,190,334,293,67,207,210,301,303,362,149,159])). % 1.18/1.30 cnf(510,plain, % 1.18/1.30 (P112(a94)+~P113(a94)), % 1.18/1.30 inference(scs_inference,[],[1,20,3,4,5,6,7,8,11,14,15,17,19,9,12,330,291,331,333,335,336,341,357,364,292,294,298,309,316,324,326,63,64,65,66,114,119,245,248,264,339,345,146,148,150,177,178,192,143,144,151,153,154,171,180,165,190,334,293,67,207,210,301,303,362,149,159,155,342,299,98,93,94,95,253,268,322,181,367,380])). % 1.18/1.30 cnf(514,plain, % 1.18/1.30 (P113(a94)+~P112(a94)), % 1.18/1.30 inference(scs_inference,[],[20,436,438,482,440,484,442,444,446,381])). % 1.18/1.30 cnf(595,plain, % 1.18/1.30 (~P113(a94)), % 1.18/1.30 inference(scs_inference,[],[510,128])). % 1.18/1.30 cnf(596,plain, % 1.18/1.30 (~P112(a94)), % 1.18/1.30 inference(scs_inference,[],[595,514])). % 1.18/1.30 cnf(597,plain, % 1.18/1.30 ($false), % 1.18/1.30 inference(scs_inference,[],[596,595,21]), % 1.18/1.30 ['proof']). % 1.18/1.30 % SZS output end Proof % 1.18/1.30 % Total time :0.630000s %------------------------------------------------------------------------------