%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS148+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 : n025.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:40 EDT 2024 % Result : Theorem 27.73s 27.77s % Output : CNFRefutation 27.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : KRS148+1 : TPTP v8.2.0. Released v3.1.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 12:05:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.45/0.57 start to proof:theBenchmark % 27.63/27.74 %------------------------------------------- % 27.63/27.74 % File :CSE---1.7 % 27.63/27.74 % Problem :theBenchmark % 27.63/27.74 % Transform :cnf % 27.63/27.74 % Format :tptp:raw % 27.63/27.74 % Command :java -jar mcs_scs.jar %d %s % 27.63/27.74 % 27.63/27.74 % Result :Theorem 27.090000s % 27.63/27.74 % Output :CNFRefutation 27.090000s % 27.63/27.74 %------------------------------------------- % 27.63/27.75 %------------------------------------------------------------------------------ % 27.63/27.75 % File : KRS148+1 : TPTP v8.2.0. Released v3.1.0. % 27.63/27.75 % Domain : Knowledge Representation (Semantic Web) % 27.63/27.75 % Problem : DL Test: k_dum ABox test from DL98 systems comparison % 27.63/27.75 % Version : Especial. % 27.63/27.75 % English : % 27.63/27.75 % 27.63/27.75 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 27.63/27.75 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 27.63/27.75 % Source : [Bec03] % 27.63/27.75 % Names : positive_description-logic-Manifest203 [Bec03] % 27.63/27.75 % 27.63/27.75 % Status : Theorem % 27.63/27.75 % Rating : 0.00 v6.1.0, 0.12 v6.0.0, 0.50 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.10 v4.1.0, 0.06 v4.0.1, 0.00 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.17 v3.3.0, 0.00 v3.2.0, 0.11 v3.1.0 % 27.63/27.75 % Syntax : Number of formulae : 90 ( 13 unt; 0 def) % 27.63/27.75 % Number of atoms : 243 ( 0 equ) % 27.63/27.75 % Maximal formula atoms : 8 ( 2 avg) % 27.63/27.75 % Number of connectives : 207 ( 54 ~; 0 |; 77 &) % 27.63/27.75 % ( 72 <=>; 4 =>; 0 <=; 0 <~>) % 27.63/27.75 % Maximal formula depth : 6 ( 4 avg) % 27.63/27.75 % Maximal term depth : 1 ( 1 avg) % 27.63/27.75 % Number of predicates : 77 ( 77 usr; 0 prp; 1-2 aty) % 27.63/27.75 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 27.63/27.75 % Number of variables : 116 ( 78 !; 38 ?) % 27.63/27.75 % SPC : FOF_THM_RFO_NEQ % 27.63/27.75 % 27.63/27.75 % Comments : Sean Bechhofer says there are some errors in the encoding of % 27.63/27.75 % datatypes, so this problem may not be perfect. At least it's % 27.63/27.75 % still representative of the type of reasoning required for OWL. % 27.63/27.75 %------------------------------------------------------------------------------ % 27.63/27.75 %----Thing and Nothing % 27.63/27.75 fof(axiom_0,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cowlThing(X) % 27.63/27.75 & ~ cowlNothing(X) ) ). % 27.63/27.75 % 27.63/27.75 %----String and Integer disjoint % 27.63/27.75 fof(axiom_1,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( xsd_string(X) % 27.63/27.75 <=> ~ xsd_integer(X) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC10 % 27.63/27.75 fof(axiom_2,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC10(X) % 27.63/27.75 <=> ( ~ cC8(X) % 27.63/27.75 & ~ cC2(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC100 % 27.63/27.75 fof(axiom_3,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC100(X) % 27.63/27.75 <=> ( ~ cC98(X) % 27.63/27.75 & cC94(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC102 % 27.63/27.75 fof(axiom_4,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC102(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & cC100(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC104 % 27.63/27.75 fof(axiom_5,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC104(X) % 27.63/27.75 <=> ( ~ cC102(X) % 27.63/27.75 & cC88(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC106 % 27.63/27.75 fof(axiom_6,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC106(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & cC104(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC108 % 27.63/27.75 fof(axiom_7,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC108(X) % 27.63/27.75 <=> ( cC84(X) % 27.63/27.75 & ~ cC106(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC110 % 27.63/27.75 fof(axiom_8,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC110(X) % 27.63/27.75 <=> ( cC62(X) % 27.63/27.75 & ~ cC108(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC112 % 27.63/27.75 fof(axiom_9,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC112(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & ~ cC110(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC114 % 27.63/27.75 fof(axiom_10,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC114(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & cC112(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC116 % 27.63/27.75 fof(axiom_11,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC116(X) % 27.63/27.75 <=> ( cTOP(X) % 27.63/27.75 & ~ cC114(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC118 % 27.63/27.75 fof(axiom_12,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC118(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & ~ cC2(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC12 % 27.63/27.75 fof(axiom_13,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC12(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & cC10(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC120 % 27.63/27.75 fof(axiom_14,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC120(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & ~ cC118(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC122 % 27.63/27.75 fof(axiom_15,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC122(X) % 27.63/27.75 <=> ( ~ cC2(X) % 27.63/27.75 & cC120(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC124 % 27.63/27.75 fof(axiom_16,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC124(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & ~ cC2(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC126 % 27.63/27.75 fof(axiom_17,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC126(X) % 27.63/27.75 <=> ( cC124(X) % 27.63/27.75 & cC2(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC128 % 27.63/27.75 fof(axiom_18,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC128(X) % 27.63/27.75 <=> ? [Y] : % 27.63/27.75 ( rR1(X,Y) % 27.63/27.75 & cC126(Y) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC130 % 27.63/27.75 fof(axiom_19,axiom, % 27.63/27.75 ! [X] : % 27.63/27.75 ( cC130(X) % 27.63/27.75 <=> ( ~ cC2(X) % 27.63/27.75 & ~ cC128(X) ) ) ). % 27.63/27.75 % 27.63/27.75 %----Equality cC132 % 27.63/27.75 fof(axiom_20,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC132(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC130(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC134 % 27.63/27.76 fof(axiom_21,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC134(X) % 27.63/27.76 <=> ( cC122(X) % 27.63/27.76 & ~ cC132(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC136 % 27.63/27.76 fof(axiom_22,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC136(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC134(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC138 % 27.63/27.76 fof(axiom_23,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC138(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC136(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC14 % 27.63/27.76 fof(axiom_24,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC14(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC12(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC140 % 27.63/27.76 fof(axiom_25,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC140(X) % 27.63/27.76 <=> ( cTOP(X) % 27.63/27.76 & cC138(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC16 % 27.63/27.76 fof(axiom_26,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC16(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC18 % 27.63/27.76 fof(axiom_27,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC18(X) % 27.63/27.76 <=> ( cC16(X) % 27.63/27.76 & cC2(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC20 % 27.63/27.76 fof(axiom_28,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC20(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC18(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC22 % 27.63/27.76 fof(axiom_29,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC22(X) % 27.63/27.76 <=> ( ~ cC20(X) % 27.63/27.76 & ~ cC2(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC24 % 27.63/27.76 fof(axiom_30,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC24(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC22(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC26 % 27.63/27.76 fof(axiom_31,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC26(X) % 27.63/27.76 <=> ( cC14(X) % 27.63/27.76 & ~ cC24(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC28 % 27.63/27.76 fof(axiom_32,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC28(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC30 % 27.63/27.76 fof(axiom_33,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC30(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC28(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC32 % 27.63/27.76 fof(axiom_34,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC32(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC34 % 27.63/27.76 fof(axiom_35,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC34(X) % 27.63/27.76 <=> ( cC30(X) % 27.63/27.76 & ~ cC32(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC36 % 27.63/27.76 fof(axiom_36,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC36(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC34(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC38 % 27.63/27.76 fof(axiom_37,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC38(X) % 27.63/27.76 <=> ( ~ cC36(X) % 27.63/27.76 & ~ cC26(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC4 % 27.63/27.76 fof(axiom_38,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC4(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC40 % 27.63/27.76 fof(axiom_39,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC40(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC42 % 27.63/27.76 fof(axiom_40,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC42(X) % 27.63/27.76 <=> ( ~ cC2(X) % 27.63/27.76 & cC40(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC44 % 27.63/27.76 fof(axiom_41,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC44(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC46 % 27.63/27.76 fof(axiom_42,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC46(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC44(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC48 % 27.63/27.76 fof(axiom_43,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC48(X) % 27.63/27.76 <=> ( cC42(X) % 27.63/27.76 & cC46(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC50 % 27.63/27.76 fof(axiom_44,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC50(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC52 % 27.63/27.76 fof(axiom_45,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC52(X) % 27.63/27.76 <=> ( cC2(X) % 27.63/27.76 & cC50(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC54 % 27.63/27.76 fof(axiom_46,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC54(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC52(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC56 % 27.63/27.76 fof(axiom_47,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC56(X) % 27.63/27.76 <=> ( ~ cC54(X) % 27.63/27.76 & ~ cC2(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC58 % 27.63/27.76 fof(axiom_48,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC58(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC56(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC6 % 27.63/27.76 fof(axiom_49,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC6(X) % 27.63/27.76 <=> ( cC2(X) % 27.63/27.76 & cC4(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC60 % 27.63/27.76 fof(axiom_50,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC60(X) % 27.63/27.76 <=> ( cC48(X) % 27.63/27.76 & ~ cC58(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC62 % 27.63/27.76 fof(axiom_51,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC62(X) % 27.63/27.76 <=> ( cC38(X) % 27.63/27.76 & ~ cC60(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC64 % 27.63/27.76 fof(axiom_52,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC64(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC66 % 27.63/27.76 fof(axiom_53,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC66(X) % 27.63/27.76 <=> ( cC64(X) % 27.63/27.76 & cC2(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC68 % 27.63/27.76 fof(axiom_54,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC68(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC70 % 27.63/27.76 fof(axiom_55,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC70(X) % 27.63/27.76 <=> ( cC2(X) % 27.63/27.76 & cC68(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC72 % 27.63/27.76 fof(axiom_56,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC72(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & cC70(Y) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC74 % 27.63/27.76 fof(axiom_57,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC74(X) % 27.63/27.76 <=> ( cC66(X) % 27.63/27.76 & cC72(X) ) ) ). % 27.63/27.76 % 27.63/27.76 %----Equality cC76 % 27.63/27.76 fof(axiom_58,axiom, % 27.63/27.76 ! [X] : % 27.63/27.76 ( cC76(X) % 27.63/27.76 <=> ? [Y] : % 27.63/27.76 ( rR1(X,Y) % 27.63/27.76 & ~ cC2(Y) ) ) ). % 27.63/27.76 % 27.63/27.77 %----Equality cC78 % 27.63/27.77 fof(axiom_59,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC78(X) % 27.63/27.77 <=> ( cC76(X) % 27.63/27.77 & cC2(X) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC8 % 27.63/27.77 fof(axiom_60,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC8(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & cC6(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC80 % 27.63/27.77 fof(axiom_61,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC80(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & cC78(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC82 % 27.63/27.77 fof(axiom_62,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC82(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & ~ cC80(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC84 % 27.63/27.77 fof(axiom_63,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC84(X) % 27.63/27.77 <=> ( cC82(X) % 27.63/27.77 & cC74(X) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC86 % 27.63/27.77 fof(axiom_64,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC86(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & ~ cC2(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC88 % 27.63/27.77 fof(axiom_65,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC88(X) % 27.63/27.77 <=> ( cC86(X) % 27.63/27.77 & cC2(X) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC90 % 27.63/27.77 fof(axiom_66,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC90(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & ~ cC2(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC92 % 27.63/27.77 fof(axiom_67,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC92(X) % 27.63/27.77 <=> ( cC2(X) % 27.63/27.77 & cC90(X) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC94 % 27.63/27.77 fof(axiom_68,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC94(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & cC92(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC96 % 27.63/27.77 fof(axiom_69,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC96(X) % 27.63/27.77 <=> ? [Y] : % 27.63/27.77 ( rR1(X,Y) % 27.63/27.77 & ~ cC2(Y) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cC98 % 27.63/27.77 fof(axiom_70,axiom, % 27.63/27.77 ! [X] : % 27.63/27.77 ( cC98(X) % 27.63/27.77 <=> ( cC96(X) % 27.63/27.77 & cC2(X) ) ) ). % 27.63/27.77 % 27.63/27.77 %----Equality cTEST % 27.73/27.77 fof(axiom_71,axiom, % 27.73/27.77 ! [X] : % 27.73/27.77 ( cTEST(X) % 27.73/27.77 <=> ( cC140(X) % 27.73/27.77 & cC116(X) ) ) ). % 27.73/27.77 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(axiom_72,axiom, % 27.73/27.77 cTEST(iV5475) ). % 27.73/27.77 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(axiom_73,axiom, % 27.73/27.77 cTOP(iV5475) ). % 27.73/27.77 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(axiom_74,axiom, % 27.73/27.77 cowlThing(iV5475) ). % 27.73/27.77 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(axiom_75,axiom, % 27.73/27.77 ! [X] : % 27.73/27.77 ( rR1(iV5475,X) % 27.73/27.77 => ~ cC112(X) ) ). % 27.73/27.77 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(axiom_76,axiom, % 27.73/27.77 ~ cC114(iV5475) ). % 27.73/27.77 % 27.73/27.77 fof(axiom_77,axiom, % 27.73/27.77 rR1(iV5475,iV5476) ). % 27.73/27.77 % 27.73/27.77 %----iV5476 % 27.73/27.77 fof(axiom_78,axiom, % 27.73/27.77 cowlThing(iV5476) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_79,axiom, % 27.73/27.77 ~ cC34(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_80,axiom, % 27.73/27.77 ~ cC12(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_81,axiom, % 27.73/27.77 ! [X] : % 27.73/27.77 ( rR1(iV5478,X) % 27.73/27.77 => cC2(X) ) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_82,axiom, % 27.73/27.77 ~ cC30(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_83,axiom, % 27.73/27.77 ~ cC130(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_84,axiom, % 27.73/27.77 ~ cC118(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_85,axiom, % 27.73/27.77 cowlThing(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_86,axiom, % 27.73/27.77 cC2(iV5478) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_87,axiom, % 27.73/27.77 ! [X] : % 27.73/27.77 ( rR1(iV5478,X) % 27.73/27.77 => ~ cC28(X) ) ). % 27.73/27.77 % 27.73/27.77 %----iV5478 % 27.73/27.77 fof(axiom_88,axiom, % 27.73/27.77 ! [X] : % 27.73/27.77 ( rR1(iV5478,X) % 27.73/27.77 => ~ cC10(X) ) ). % 27.73/27.77 % 27.73/27.77 %----Thing and Nothing % 27.73/27.77 %----String and Integer disjoint % 27.73/27.77 %----iV5475 % 27.73/27.77 %----iV5475 % 27.73/27.77 %----iV5475 % 27.73/27.77 %----iV5475 % 27.73/27.77 fof(the_axiom,conjecture, % 27.73/27.77 ( ! [X] : % 27.73/27.77 ( cowlThing(X) % 27.73/27.77 & ~ cowlNothing(X) ) % 27.73/27.77 & ! [X] : % 27.73/27.77 ( xsd_string(X) % 27.73/27.77 <=> ~ xsd_integer(X) ) % 27.73/27.77 & cC138(iV5475) % 27.73/27.77 & cowlThing(iV5475) % 27.73/27.77 & cC116(iV5475) % 27.73/27.77 & cC140(iV5475) ) ). % 27.73/27.77 % 27.73/27.77 %------------------------------------------------------------------------------ % 27.73/27.77 %------------------------------------------- % 27.73/27.77 % Proof found % 27.73/27.77 % SZS status Theorem for theBenchmark % 27.73/27.77 % SZS output start Proof % 27.73/27.77 %ClaNum:229(EqnAxiom:0) % 27.73/27.77 %VarNum:579(SingletonVarNum:255) % 27.73/27.77 %MaxLitNum:6 % 27.73/27.77 %MaxfuncDepth:1 % 27.73/27.77 %SharedTerms:23 % 27.73/27.77 %goalClause: 149 150 % 27.73/27.77 [1]P1(a1) % 27.73/27.77 [2]P28(a2) % 27.73/27.77 [3]P29(a2) % 27.73/27.77 [4]P73(a2,a43) % 27.73/27.77 [5]~P2(a2) % 27.73/27.77 [6]~P11(a1) % 27.73/27.77 [7]~P13(a1) % 27.73/27.77 [8]~P14(a1) % 27.73/27.77 [9]~P30(a1) % 27.73/27.77 [10]~P36(a1) % 27.73/27.77 [11]~P74(x111) % 27.73/27.77 [12]P76(x121)+P75(x121) % 27.73/27.77 [13]~P38(x131)+P1(x131) % 27.73/27.77 [14]~P39(x141)+P1(x141) % 27.73/27.77 [15]~P15(x151)+P1(x151) % 27.73/27.77 [16]~P20(x161)+P1(x161) % 27.73/27.77 [17]~P40(x171)+P1(x171) % 27.73/27.77 [18]~P50(x181)+P1(x181) % 27.73/27.77 [19]~P54(x191)+P1(x191) % 27.73/27.77 [20]~P58(x201)+P1(x201) % 27.73/27.77 [21]~P60(x211)+P1(x211) % 27.73/27.77 [22]~P69(x221)+P1(x221) % 27.73/27.77 [23]~P3(x231)+P71(x231) % 27.73/27.77 [24]~P5(x241)+P39(x241) % 27.73/27.77 [25]~P7(x251)+P64(x251) % 27.73/27.77 [26]~P9(x261)+P55(x261) % 27.73/27.77 [27]~P29(x271)+P12(x271) % 27.73/27.77 [28]~P12(x281)+P28(x281) % 27.73/27.77 [29]~P21(x291)+P28(x291) % 27.73/27.77 [30]~P17(x301)+P16(x301) % 27.73/27.77 [31]~P22(x311)+P17(x311) % 27.73/27.77 [32]~P15(x321)+P18(x321) % 27.73/27.77 [33]~P21(x331)+P24(x331) % 27.73/27.77 [34]~P31(x341)+P26(x341) % 27.73/27.77 [35]~P29(x351)+P21(x351) % 27.73/27.77 [36]~P20(x361)+P27(x361) % 27.73/27.77 [37]~P36(x371)+P30(x371) % 27.73/27.77 [38]~P55(x381)+P41(x381) % 27.73/27.77 [39]~P50(x391)+P43(x391) % 27.73/27.77 [40]~P45(x401)+P44(x401) % 27.73/27.77 [41]~P46(x411)+P45(x411) % 27.73/27.77 [42]~P46(x421)+P47(x421) % 27.73/27.77 [43]~P56(x431)+P46(x431) % 27.73/27.77 [44]~P40(x441)+P49(x441) % 27.73/27.77 [45]~P54(x451)+P57(x451) % 27.73/27.77 [46]~P61(x461)+P54(x461) % 27.73/27.77 [47]~P58(x471)+P59(x471) % 27.73/27.77 [48]~P61(x481)+P62(x481) % 27.73/27.77 [49]~P64(x491)+P61(x491) % 27.73/27.77 [50]~P60(x501)+P63(x501) % 27.73/27.77 [51]~P64(x511)+P65(x511) % 27.73/27.77 [52]~P39(x521)+P68(x521) % 27.73/27.77 [53]~P69(x531)+P70(x531) % 27.73/27.77 [54]~P38(x541)+P72(x541) % 27.73/27.77 [60]~P76(x601)+~P75(x601) % 27.73/27.77 [61]~P66(x611)+~P4(x611) % 27.73/27.77 [62]~P1(x621)+~P4(x621) % 27.73/27.77 [63]~P17(x631)+~P1(x631) % 27.73/27.77 [64]~P14(x641)+~P1(x641) % 27.73/27.77 [65]~P33(x651)+~P1(x651) % 27.73/27.77 [66]~P45(x661)+~P1(x661) % 27.73/27.77 [67]~P52(x671)+~P1(x671) % 27.73/27.77 [68]~P38(x681)+~P3(x681) % 27.73/27.77 [69]~P5(x691)+~P6(x691) % 27.73/27.77 [70]~P7(x701)+~P8(x701) % 27.73/27.77 [71]~P9(x711)+~P7(x711) % 27.73/27.77 [72]~P56(x721)+~P55(x721) % 27.73/27.77 [73]~P12(x731)+~P2(x731) % 27.73/27.77 [74]~P14(x741)+~P19(x741) % 27.73/27.77 [75]~P22(x751)+~P23(x751) % 27.73/27.77 [76]~P33(x761)+~P32(x761) % 27.73/27.77 [77]~P31(x771)+~P34(x771) % 27.73/27.77 [78]~P41(x781)+~P31(x781) % 27.73/27.77 [79]~P36(x791)+~P37(x791) % 27.73/27.77 [80]~P41(x801)+~P42(x801) % 27.73/27.77 [81]~P52(x811)+~P51(x811) % 27.73/27.77 [82]~P56(x821)+~P53(x821) % 27.73/27.77 [148]P1(x1481)+~P73(a1,x1481) % 27.73/27.77 [151]~P4(x1511)+~P73(a1,x1511) % 27.73/27.77 [152]~P10(x1521)+~P73(a2,x1521) % 27.73/27.77 [153]~P35(x1531)+~P73(a1,x1531) % 27.73/27.77 [95]~P13(x951)+P4(f3(x951)) % 27.73/27.77 [96]~P6(x961)+P3(f4(x961)) % 27.73/27.77 [97]~P8(x971)+P5(f15(x971)) % 27.73/27.77 [98]~P2(x981)+P10(f26(x981)) % 27.73/27.77 [99]~P26(x991)+P13(f5(x991)) % 27.73/27.77 [100]~P19(x1001)+P15(f40(x1001)) % 27.73/27.77 [101]~P23(x1011)+P14(f6(x1011)) % 27.73/27.77 [102]~P25(x1021)+P22(f7(x1021)) % 27.73/27.77 [103]~P24(x1031)+P25(f8(x1031)) % 27.73/27.77 [104]~P32(x1041)+P20(f9(x1041)) % 27.73/27.77 [105]~P34(x1051)+P33(f11(x1051)) % 27.73/27.77 [106]~P30(x1061)+P35(f12(x1061)) % 27.73/27.77 [107]~P42(x1071)+P36(f16(x1071)) % 27.73/27.77 [108]~P51(x1081)+P40(f17(x1081)) % 27.73/27.77 [109]~P53(x1091)+P52(f23(x1091)) % 27.73/27.77 [110]~P66(x1101)+P50(f27(x1101)) % 27.73/27.77 [111]~P62(x1111)+P58(f28(x1111)) % 27.73/27.77 [112]~P67(x1121)+P60(f30(x1121)) % 27.73/27.77 [113]~P71(x1131)+P69(f31(x1131)) % 27.73/27.77 [129]~P10(x1291)+~P9(f35(x1291)) % 27.73/27.77 [130]~P11(x1301)+~P1(f39(x1301)) % 27.73/27.77 [131]~P16(x1311)+~P11(f41(x1311)) % 27.73/27.77 [132]~P18(x1321)+~P1(f42(x1321)) % 27.73/27.77 [133]~P27(x1331)+~P1(f10(x1331)) % 27.73/27.77 [134]~P35(x1341)+~P1(f13(x1341)) % 27.73/27.77 [135]~P37(x1351)+~P1(f14(x1351)) % 27.73/27.77 [136]~P43(x1361)+~P1(f18(x1361)) % 27.73/27.77 [137]~P44(x1371)+~P1(f19(x1371)) % 27.73/27.77 [138]~P48(x1381)+~P1(f20(x1381)) % 27.73/27.77 [139]~P47(x1391)+~P48(f21(x1391)) % 27.73/27.77 [140]~P49(x1401)+~P1(f22(x1401)) % 27.73/27.77 [141]~P57(x1411)+~P1(f24(x1411)) % 27.73/27.77 [142]~P59(x1421)+~P1(f25(x1421)) % 27.73/27.77 [143]~P63(x1431)+~P1(f29(x1431)) % 27.73/27.77 [144]~P65(x1441)+~P67(f32(x1441)) % 27.73/27.77 [145]~P68(x1451)+~P1(f33(x1451)) % 27.73/27.77 [146]~P70(x1461)+~P1(f34(x1461)) % 27.73/27.77 [147]~P72(x1471)+~P1(f36(x1471)) % 27.73/27.77 [154]~P6(x1541)+P73(x1541,f4(x1541)) % 27.73/27.77 [155]~P8(x1551)+P73(x1551,f15(x1551)) % 27.73/27.77 [156]~P10(x1561)+P73(x1561,f35(x1561)) % 27.73/27.77 [157]~P2(x1571)+P73(x1571,f26(x1571)) % 27.73/27.77 [158]~P11(x1581)+P73(x1581,f39(x1581)) % 27.73/27.77 [159]~P13(x1591)+P73(x1591,f3(x1591)) % 27.73/27.77 [160]~P16(x1601)+P73(x1601,f41(x1601)) % 27.73/27.77 [161]~P18(x1611)+P73(x1611,f42(x1611)) % 27.73/27.77 [162]~P19(x1621)+P73(x1621,f40(x1621)) % 27.73/27.77 [163]~P23(x1631)+P73(x1631,f6(x1631)) % 27.73/27.77 [164]~P25(x1641)+P73(x1641,f7(x1641)) % 27.73/27.77 [165]~P24(x1651)+P73(x1651,f8(x1651)) % 27.73/27.77 [166]~P26(x1661)+P73(x1661,f5(x1661)) % 27.73/27.77 [167]~P27(x1671)+P73(x1671,f10(x1671)) % 27.73/27.77 [168]~P32(x1681)+P73(x1681,f9(x1681)) % 27.73/27.77 [169]~P34(x1691)+P73(x1691,f11(x1691)) % 27.73/27.77 [170]~P35(x1701)+P73(x1701,f13(x1701)) % 27.73/27.77 [171]~P30(x1711)+P73(x1711,f12(x1711)) % 27.73/27.77 [172]~P37(x1721)+P73(x1721,f14(x1721)) % 27.73/27.77 [173]~P42(x1731)+P73(x1731,f16(x1731)) % 27.73/27.77 [174]~P43(x1741)+P73(x1741,f18(x1741)) % 27.73/27.77 [175]~P44(x1751)+P73(x1751,f19(x1751)) % 27.73/27.77 [176]~P48(x1761)+P73(x1761,f20(x1761)) % 27.73/27.77 [177]~P47(x1771)+P73(x1771,f21(x1771)) % 27.73/27.77 [178]~P49(x1781)+P73(x1781,f22(x1781)) % 27.73/27.77 [179]~P51(x1791)+P73(x1791,f17(x1791)) % 27.73/27.77 [180]~P53(x1801)+P73(x1801,f23(x1801)) % 27.73/27.77 [181]~P57(x1811)+P73(x1811,f24(x1811)) % 27.73/27.77 [182]~P59(x1821)+P73(x1821,f25(x1821)) % 27.73/27.77 [183]~P62(x1831)+P73(x1831,f28(x1831)) % 27.73/27.77 [184]~P63(x1841)+P73(x1841,f29(x1841)) % 27.73/27.77 [185]~P66(x1851)+P73(x1851,f27(x1851)) % 27.73/27.77 [186]~P67(x1861)+P73(x1861,f30(x1861)) % 27.73/27.77 [187]~P65(x1871)+P73(x1871,f32(x1871)) % 27.73/27.77 [188]~P68(x1881)+P73(x1881,f33(x1881)) % 27.73/27.77 [189]~P70(x1891)+P73(x1891,f34(x1891)) % 27.73/27.77 [190]~P71(x1901)+P73(x1901,f31(x1901)) % 27.73/27.77 [191]~P72(x1911)+P73(x1911,f36(x1911)) % 27.73/27.77 [55]P66(x551)+P1(x551)+P4(x551) % 27.73/27.77 [56]P19(x561)+P14(x561)+P1(x561) % 27.73/27.77 [57]P32(x571)+P33(x571)+P1(x571) % 27.73/27.77 [58]P51(x581)+P52(x581)+P1(x581) % 27.73/27.77 [59]P42(x591)+P41(x591)+P31(x591) % 27.73/27.77 [83]P17(x831)+~P16(x831)+P1(x831) % 27.73/27.77 [84]P45(x841)+~P44(x841)+P1(x841) % 27.73/27.77 [85]P38(x851)+~P71(x851)+P3(x851) % 27.73/27.77 [86]P5(x861)+~P39(x861)+P6(x861) % 27.73/27.77 [87]P7(x871)+~P64(x871)+P8(x871) % 27.73/27.77 [88]P9(x881)+~P55(x881)+P7(x881) % 27.73/27.77 [89]P56(x891)+~P41(x891)+P55(x891) % 27.73/27.77 [90]P12(x901)+~P28(x901)+P2(x901) % 27.73/27.77 [91]P22(x911)+~P17(x911)+P23(x911) % 27.73/27.77 [92]P31(x921)+~P26(x921)+P34(x921) % 27.73/27.77 [93]P36(x931)+~P30(x931)+P37(x931) % 27.73/27.77 [94]P56(x941)+~P46(x941)+P53(x941) % 27.73/27.77 [114]~P1(x1141)+~P72(x1141)+P38(x1141) % 27.73/27.77 [115]~P1(x1151)+~P68(x1151)+P39(x1151) % 27.73/27.77 [116]~P61(x1161)+~P65(x1161)+P64(x1161) % 27.73/27.77 [117]~P1(x1171)+~P18(x1171)+P15(x1171) % 27.73/27.77 [118]~P28(x1181)+~P24(x1181)+P21(x1181) % 27.73/27.77 [119]~P1(x1191)+~P27(x1191)+P20(x1191) % 27.73/27.77 [120]~P45(x1201)+~P47(x1201)+P46(x1201) % 27.73/27.77 [121]~P1(x1211)+~P49(x1211)+P40(x1211) % 27.73/27.77 [122]~P1(x1221)+~P43(x1221)+P50(x1221) % 27.73/27.77 [123]~P1(x1231)+~P57(x1231)+P54(x1231) % 27.73/27.77 [124]~P1(x1241)+~P59(x1241)+P58(x1241) % 27.73/27.77 [125]~P54(x1251)+~P62(x1251)+P61(x1251) % 27.73/27.77 [126]~P1(x1261)+~P63(x1261)+P60(x1261) % 27.73/27.77 [127]~P1(x1271)+~P70(x1271)+P69(x1271) % 27.73/27.77 [128]~P12(x1281)+~P21(x1281)+P29(x1281) % 27.73/27.77 [192]~P73(x1922,x1921)+P1(x1921)+P11(x1922) % 27.73/27.77 [193]~P73(x1932,x1931)+P1(x1931)+P18(x1932) % 27.73/27.77 [194]~P73(x1942,x1941)+P1(x1941)+P27(x1942) % 27.73/27.77 [195]~P73(x1952,x1951)+P1(x1951)+P35(x1952) % 27.73/27.77 [196]~P73(x1962,x1961)+P1(x1961)+P37(x1962) % 27.73/27.77 [197]~P73(x1972,x1971)+P1(x1971)+P43(x1972) % 27.73/27.77 [198]~P73(x1982,x1981)+P1(x1981)+P44(x1982) % 27.73/27.77 [199]~P73(x1992,x1991)+P1(x1991)+P48(x1992) % 27.73/27.77 [200]~P73(x2002,x2001)+P1(x2001)+P49(x2002) % 27.73/27.77 [201]~P73(x2012,x2011)+P1(x2011)+P57(x2012) % 27.73/27.77 [202]~P73(x2022,x2021)+P1(x2021)+P59(x2022) % 27.73/27.77 [203]~P73(x2032,x2031)+P1(x2031)+P63(x2032) % 27.73/27.77 [204]~P73(x2042,x2041)+P1(x2041)+P68(x2042) % 27.73/27.77 [205]~P73(x2052,x2051)+P1(x2051)+P70(x2052) % 27.73/27.77 [206]~P73(x2062,x2061)+P1(x2061)+P72(x2062) % 27.73/27.77 [207]~P73(x2072,x2071)+P9(x2071)+P10(x2072) % 27.73/27.77 [208]~P73(x2082,x2081)+P11(x2081)+P16(x2082) % 27.73/27.77 [209]~P73(x2092,x2091)+P48(x2091)+P47(x2092) % 27.73/27.77 [210]~P73(x2102,x2101)+P67(x2101)+P65(x2102) % 27.73/27.77 [211]~P73(x2111,x2112)+P66(x2111)+~P50(x2112) % 27.73/27.77 [212]~P73(x2121,x2122)+P71(x2121)+~P69(x2122) % 27.73/27.77 [213]~P73(x2131,x2132)+P6(x2131)+~P3(x2132) % 27.73/27.77 [214]~P73(x2141,x2142)+P8(x2141)+~P5(x2142) % 27.73/27.77 [215]~P73(x2151,x2152)+P2(x2151)+~P10(x2152) % 27.73/27.77 [216]~P73(x2161,x2162)+P13(x2161)+~P4(x2162) % 27.73/27.77 [217]~P73(x2171,x2172)+P19(x2171)+~P15(x2172) % 27.73/27.77 [218]~P73(x2181,x2182)+P23(x2181)+~P14(x2182) % 27.73/27.77 [219]~P73(x2191,x2192)+P25(x2191)+~P22(x2192) % 27.73/27.77 [220]~P73(x2201,x2202)+P24(x2201)+~P25(x2202) % 27.73/27.77 [221]~P73(x2211,x2212)+P26(x2211)+~P13(x2212) % 27.73/27.77 [222]~P73(x2221,x2222)+P32(x2221)+~P20(x2222) % 27.73/27.77 [223]~P73(x2231,x2232)+P34(x2231)+~P33(x2232) % 27.73/27.77 [224]~P73(x2241,x2242)+P30(x2241)+~P35(x2242) % 27.73/27.77 [225]~P73(x2251,x2252)+P42(x2251)+~P36(x2252) % 27.73/27.77 [226]~P73(x2261,x2262)+P51(x2261)+~P40(x2262) % 27.73/27.77 [227]~P73(x2271,x2272)+P53(x2271)+~P52(x2272) % 27.73/27.77 [228]~P73(x2281,x2282)+P62(x2281)+~P58(x2282) % 27.73/27.77 [229]~P73(x2291,x2292)+P67(x2291)+~P60(x2292) % 27.73/27.77 [149]P74(a37)+P75(a38)+~P76(a38)+~P12(a2)+~P24(a2)+~P21(a2) % 27.73/27.77 [150]P74(a37)+P76(a38)+~P75(a38)+~P12(a2)+~P24(a2)+~P21(a2) % 27.73/27.77 %EqnAxiom % 27.73/27.77 % 27.73/27.77 %------------------------------------------- % 27.73/27.77 cnf(246,plain, % 27.73/27.77 (P12(a2)), % 27.73/27.77 inference(scs_inference,[],[1,2,4,5,152,63,65,66,67,31,41,43,90])). % 27.73/27.77 cnf(253,plain, % 27.73/27.77 (P75(a38)+~P76(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[11,246,149])). % 27.73/27.77 cnf(254,plain, % 27.73/27.77 (P76(a38)+~P75(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[11,246,150])). % 27.73/27.77 cnf(20511,plain, % 27.73/27.77 (P76(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[12,254])). % 27.73/27.77 cnf(20542,plain, % 27.73/27.77 (~P75(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[20511,60])). % 27.73/27.77 cnf(20573,plain, % 27.73/27.77 (~P76(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[20542,253])). % 27.73/27.77 cnf(20604,plain, % 27.73/27.77 (P75(a38)+~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[20573,12])). % 27.73/27.77 cnf(20635,plain, % 27.73/27.77 (~P24(a2)+~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[20604,20542])). % 27.73/27.77 cnf(20666,plain, % 27.73/27.77 (~P21(a2)), % 27.73/27.77 inference(scs_inference,[],[20635,33])). % 27.73/27.77 cnf(20668,plain, % 27.73/27.77 ($false), % 27.73/27.77 inference(scs_inference,[],[20666,3,35]), % 27.73/27.77 ['proof']). % 27.73/27.79 % SZS output end Proof % 27.73/27.79 % Total time :27.090000s %------------------------------------------------------------------------------