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