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