%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS147+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 : n012.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 58.99s 59.12s % Output : CNFRefutation 59.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS147+1 : TPTP v8.2.0. Released v3.1.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n012.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Wed Jun 19 13:26:38 EDT 2024 % 0.11/0.32 % CPUTime : % 0.44/0.57 start to proof:theBenchmark % 58.90/59.09 %------------------------------------------- % 58.90/59.09 % File :CSE---1.7 % 58.90/59.09 % Problem :theBenchmark % 58.90/59.09 % Transform :cnf % 58.90/59.09 % Format :tptp:raw % 58.90/59.09 % Command :java -jar mcs_scs.jar %d %s % 58.90/59.09 % 58.90/59.09 % Result :Theorem 58.400000s % 58.90/59.09 % Output :CNFRefutation 58.400000s % 58.90/59.09 %------------------------------------------- % 58.99/59.10 %------------------------------------------------------------------------------ % 58.99/59.10 % File : KRS147+1 : TPTP v8.2.0. Released v3.1.0. % 58.99/59.10 % Domain : Knowledge Representation (Semantic Web) % 58.99/59.10 % Problem : DL Test: k_d4 ABox test from DL98 systems comparison % 58.99/59.10 % Version : Especial. % 58.99/59.10 % English : % 58.99/59.10 % 58.99/59.10 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.99/59.10 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.99/59.10 % Source : [Bec03] % 58.99/59.10 % Names : positive_description-logic-Manifest202 [Bec03] % 58.99/59.10 % 58.99/59.10 % Status : Theorem % 58.99/59.10 % Rating : 0.00 v8.2.0, 0.07 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.1.0, 0.16 v6.0.0, 0.25 v5.4.0, 0.26 v5.3.0, 0.35 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.11 v4.0.1, 0.05 v3.7.0, 0.00 v3.4.0, 0.17 v3.3.0, 0.00 v3.2.0, 0.11 v3.1.0 % 58.99/59.10 % Syntax : Number of formulae : 87 ( 34 unt; 0 def) % 58.99/59.10 % Number of atoms : 204 ( 0 equ) % 58.99/59.10 % Maximal formula atoms : 19 ( 2 avg) % 58.99/59.10 % Number of connectives : 164 ( 47 ~; 0 |; 65 &) % 58.99/59.10 % ( 49 <=>; 3 =>; 0 <=; 0 <~>) % 58.99/59.10 % Maximal formula depth : 17 ( 4 avg) % 58.99/59.10 % Maximal term depth : 1 ( 1 avg) % 58.99/59.10 % Number of predicates : 54 ( 54 usr; 0 prp; 1-2 aty) % 58.99/59.10 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 58.99/59.10 % Number of variables : 85 ( 54 !; 31 ?) % 58.99/59.10 % SPC : FOF_THM_RFO_NEQ % 58.99/59.10 % 58.99/59.10 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.99/59.10 % datatypes, so this problem may not be perfect. At least it's % 58.99/59.10 % still representative of the type of reasoning required for OWL. % 58.99/59.10 %------------------------------------------------------------------------------ % 58.99/59.10 %----Thing and Nothing % 58.99/59.10 fof(axiom_0,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cowlThing(X) % 58.99/59.10 & ~ cowlNothing(X) ) ). % 58.99/59.10 % 58.99/59.10 %----String and Integer disjoint % 58.99/59.10 fof(axiom_1,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( xsd_string(X) % 58.99/59.10 <=> ~ xsd_integer(X) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC10 % 58.99/59.10 fof(axiom_2,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC10(X) % 58.99/59.10 <=> ( cC4(X) % 58.99/59.10 & cC8(X) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC12 % 58.99/59.10 fof(axiom_3,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC12(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & cC10(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC14 % 58.99/59.10 fof(axiom_4,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC14(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & cTOP(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC16 % 58.99/59.10 fof(axiom_5,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC16(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & ~ cC14(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC18 % 58.99/59.10 fof(axiom_6,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC18(X) % 58.99/59.10 <=> ( ~ cC16(X) % 58.99/59.10 & cC12(X) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC20 % 58.99/59.10 fof(axiom_7,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC20(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & ~ cC2(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC22 % 58.99/59.10 fof(axiom_8,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC22(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & ~ cC2(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC24 % 58.99/59.10 fof(axiom_9,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC24(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & cC22(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC26 % 58.99/59.10 fof(axiom_10,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC26(X) % 58.99/59.10 <=> ( ~ cC20(X) % 58.99/59.10 & cC24(X) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC28 % 58.99/59.10 fof(axiom_11,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC28(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & cC26(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC30 % 58.99/59.10 fof(axiom_12,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC30(X) % 58.99/59.10 <=> ( cC18(X) % 58.99/59.10 & ~ cC28(X) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC32 % 58.99/59.10 fof(axiom_13,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC32(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.10 & cC2(Y) ) ) ). % 58.99/59.10 % 58.99/59.10 %----Equality cC34 % 58.99/59.10 fof(axiom_14,axiom, % 58.99/59.10 ! [X] : % 58.99/59.10 ( cC34(X) % 58.99/59.10 <=> ? [Y] : % 58.99/59.10 ( rR1(X,Y) % 58.99/59.11 & ~ cC32(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC36 % 58.99/59.11 fof(axiom_15,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC36(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC38 % 58.99/59.11 fof(axiom_16,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC38(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC36(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC4 % 58.99/59.11 fof(axiom_17,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC4(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC40 % 58.99/59.11 fof(axiom_18,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC40(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC38(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC42 % 58.99/59.11 fof(axiom_19,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC42(X) % 58.99/59.11 <=> ( ~ cC34(X) % 58.99/59.11 & cC40(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC44 % 58.99/59.11 fof(axiom_20,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC44(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC42(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC46 % 58.99/59.11 fof(axiom_21,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC46(X) % 58.99/59.11 <=> ( ~ cC44(X) % 58.99/59.11 & cC30(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC48 % 58.99/59.11 fof(axiom_22,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC48(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC50 % 58.99/59.11 fof(axiom_23,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC50(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC52 % 58.99/59.11 fof(axiom_24,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC52(X) % 58.99/59.11 <=> ( ~ cC50(X) % 58.99/59.11 & ~ cC48(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC54 % 58.99/59.11 fof(axiom_25,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC54(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC52(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC56 % 58.99/59.11 fof(axiom_26,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC56(X) % 58.99/59.11 <=> ( ~ cC54(X) % 58.99/59.11 & cC46(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC58 % 58.99/59.11 fof(axiom_27,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC58(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC6 % 58.99/59.11 fof(axiom_28,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC6(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC60 % 58.99/59.11 fof(axiom_29,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC60(X) % 58.99/59.11 <=> ( cC58(X) % 58.99/59.11 & ~ cC2(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC62 % 58.99/59.11 fof(axiom_30,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC62(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC60(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC64 % 58.99/59.11 fof(axiom_31,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC64(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC66 % 58.99/59.11 fof(axiom_32,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC66(X) % 58.99/59.11 <=> ( ~ cC2(X) % 58.99/59.11 & cC64(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC68 % 58.99/59.11 fof(axiom_33,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC68(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC66(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC70 % 58.99/59.11 fof(axiom_34,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC70(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC68(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC72 % 58.99/59.11 fof(axiom_35,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC72(X) % 58.99/59.11 <=> ( ~ cC62(X) % 58.99/59.11 & cC70(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC74 % 58.99/59.11 fof(axiom_36,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC74(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC72(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC76 % 58.99/59.11 fof(axiom_37,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC76(X) % 58.99/59.11 <=> ( ~ cC74(X) % 58.99/59.11 & cC56(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC78 % 58.99/59.11 fof(axiom_38,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC78(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC8 % 58.99/59.11 fof(axiom_39,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC8(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC6(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC80 % 58.99/59.11 fof(axiom_40,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC80(X) % 58.99/59.11 <=> ( ~ cC2(X) % 58.99/59.11 & ~ cC78(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC82 % 58.99/59.11 fof(axiom_41,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC82(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC80(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC84 % 58.99/59.11 fof(axiom_42,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC84(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & ~ cC2(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC86 % 58.99/59.11 fof(axiom_43,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC86(X) % 58.99/59.11 <=> ( ~ cC84(X) % 58.99/59.11 & ~ cC2(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC88 % 58.99/59.11 fof(axiom_44,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC88(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC86(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC90 % 58.99/59.11 fof(axiom_45,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC90(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC88(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC92 % 58.99/59.11 fof(axiom_46,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC92(X) % 58.99/59.11 <=> ( ~ cC82(X) % 58.99/59.11 & cC90(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cC94 % 58.99/59.11 fof(axiom_47,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cC94(X) % 58.99/59.11 <=> ? [Y] : % 58.99/59.11 ( rR1(X,Y) % 58.99/59.11 & cC92(Y) ) ) ). % 58.99/59.11 % 58.99/59.11 %----Equality cTEST % 58.99/59.11 fof(axiom_48,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( cTEST(X) % 58.99/59.11 <=> ( ~ cC94(X) % 58.99/59.11 & cC76(X) ) ) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_49,axiom, % 58.99/59.11 ~ cC92(iV8467) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_50,axiom, % 58.99/59.11 ~ cC72(iV8467) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_51,axiom, % 58.99/59.11 ~ cC42(iV8467) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_52,axiom, % 58.99/59.11 cowlThing(iV8467) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_53,axiom, % 58.99/59.11 ~ cC52(iV8467) ). % 58.99/59.11 % 58.99/59.11 %----iV8467 % 58.99/59.11 fof(axiom_54,axiom, % 58.99/59.11 ~ cC26(iV8467) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_55,axiom, % 58.99/59.11 rR1(iV8467,iV8471) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_56,axiom, % 58.99/59.11 rR1(iV8467,iV8473) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_57,axiom, % 58.99/59.11 rR1(iV8467,iV8468) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_58,axiom, % 58.99/59.11 rR1(iV8467,iV8469) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_59,axiom, % 58.99/59.11 rR1(iV8467,iV8475) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_60,axiom, % 58.99/59.11 rR1(iV8467,iV8472) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_61,axiom, % 58.99/59.11 rR1(iV8467,iV8474) ). % 58.99/59.11 % 58.99/59.11 fof(axiom_62,axiom, % 58.99/59.11 rR1(iV8467,iV8470) ). % 58.99/59.11 % 58.99/59.11 %----iV8468 % 58.99/59.11 fof(axiom_63,axiom, % 58.99/59.11 ~ cC2(iV8468) ). % 58.99/59.11 % 58.99/59.11 %----iV8468 % 58.99/59.11 fof(axiom_64,axiom, % 58.99/59.11 cowlThing(iV8468) ). % 58.99/59.11 % 58.99/59.11 %----iV8469 % 58.99/59.11 fof(axiom_65,axiom, % 58.99/59.11 ~ cC6(iV8469) ). % 58.99/59.11 % 58.99/59.11 %----iV8469 % 58.99/59.11 fof(axiom_66,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( rR1(iV8469,X) % 58.99/59.11 => cC2(X) ) ). % 58.99/59.11 % 58.99/59.11 %----iV8469 % 58.99/59.11 fof(axiom_67,axiom, % 58.99/59.11 cowlThing(iV8469) ). % 58.99/59.11 % 58.99/59.11 %----iV8470 % 58.99/59.11 fof(axiom_68,axiom, % 58.99/59.11 cTOP(iV8470) ). % 58.99/59.11 % 58.99/59.11 %----iV8470 % 58.99/59.11 fof(axiom_69,axiom, % 58.99/59.11 cowlThing(iV8470) ). % 58.99/59.11 % 58.99/59.11 %----iV8471 % 58.99/59.11 fof(axiom_70,axiom, % 58.99/59.11 ~ cC2(iV8471) ). % 58.99/59.11 % 58.99/59.11 %----iV8471 % 58.99/59.11 fof(axiom_71,axiom, % 58.99/59.11 ~ cC78(iV8471) ). % 58.99/59.11 % 58.99/59.11 %----iV8471 % 58.99/59.11 fof(axiom_72,axiom, % 58.99/59.11 cowlThing(iV8471) ). % 58.99/59.11 % 58.99/59.11 %----iV8471 % 58.99/59.11 fof(axiom_73,axiom, % 58.99/59.11 ! [X] : % 58.99/59.11 ( rR1(iV8471,X) % 58.99/59.11 => cC2(X) ) ). % 58.99/59.11 % 58.99/59.12 %----iV8472 % 58.99/59.12 fof(axiom_74,axiom, % 58.99/59.12 ~ cC2(iV8472) ). % 58.99/59.12 % 58.99/59.12 %----iV8472 % 58.99/59.12 fof(axiom_75,axiom, % 58.99/59.12 cowlThing(iV8472) ). % 58.99/59.12 % 58.99/59.12 fof(axiom_76,axiom, % 58.99/59.12 rR1(iV8472,iV8476) ). % 58.99/59.12 % 58.99/59.12 %----iV8473 % 58.99/59.12 fof(axiom_77,axiom, % 58.99/59.12 ~ cC2(iV8473) ). % 58.99/59.12 % 58.99/59.12 %----iV8473 % 58.99/59.12 fof(axiom_78,axiom, % 58.99/59.12 cowlThing(iV8473) ). % 58.99/59.12 % 58.99/59.12 %----iV8474 % 58.99/59.12 fof(axiom_79,axiom, % 58.99/59.12 ! [X] : % 58.99/59.12 ( rR1(iV8474,X) % 58.99/59.12 => ~ cC2(X) ) ). % 58.99/59.12 % 58.99/59.12 %----iV8474 % 58.99/59.12 fof(axiom_80,axiom, % 58.99/59.12 ~ cC32(iV8474) ). % 58.99/59.12 % 58.99/59.12 %----iV8474 % 58.99/59.12 fof(axiom_81,axiom, % 58.99/59.12 cowlThing(iV8474) ). % 58.99/59.12 % 58.99/59.12 %----iV8475 % 58.99/59.12 fof(axiom_82,axiom, % 58.99/59.12 ~ cC2(iV8475) ). % 58.99/59.12 % 58.99/59.12 %----iV8475 % 58.99/59.12 fof(axiom_83,axiom, % 58.99/59.12 cowlThing(iV8475) ). % 58.99/59.12 % 58.99/59.12 %----iV8476 % 58.99/59.12 fof(axiom_84,axiom, % 58.99/59.12 cC2(iV8476) ). % 58.99/59.12 % 58.99/59.12 %----iV8476 % 58.99/59.12 fof(axiom_85,axiom, % 58.99/59.12 cowlThing(iV8476) ). % 58.99/59.12 % 58.99/59.12 %----Thing and Nothing % 58.99/59.12 %----String and Integer disjoint % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8467 % 58.99/59.12 %----iV8471 % 58.99/59.12 %----iV8471 % 58.99/59.12 %----iV8472 % 58.99/59.12 %----iV8472 % 58.99/59.12 %----iV8472 % 58.99/59.12 fof(the_axiom,conjecture, % 58.99/59.12 ( ! [X] : % 58.99/59.12 ( cowlThing(X) % 58.99/59.12 & ~ cowlNothing(X) ) % 58.99/59.12 & ! [X] : % 58.99/59.12 ( xsd_string(X) % 58.99/59.12 <=> ~ xsd_integer(X) ) % 58.99/59.12 & cC10(iV8467) % 58.99/59.12 & cC48(iV8467) % 58.99/59.12 & cC4(iV8467) % 58.99/59.12 & cC82(iV8467) % 58.99/59.12 & cC14(iV8467) % 58.99/59.12 & cC8(iV8467) % 58.99/59.12 & cC20(iV8467) % 58.99/59.12 & cowlThing(iV8467) % 58.99/59.12 & cC62(iV8467) % 58.99/59.12 & cC34(iV8467) % 58.99/59.12 & cowlThing(iV8471) % 58.99/59.12 & cC80(iV8471) % 58.99/59.12 & cC60(iV8472) % 58.99/59.12 & cowlThing(iV8472) % 58.99/59.12 & cC58(iV8472) ) ). % 58.99/59.12 % 58.99/59.12 %------------------------------------------------------------------------------ % 58.99/59.12 %------------------------------------------- % 58.99/59.12 % Proof found % 58.99/59.12 % SZS status Theorem for theBenchmark % 58.99/59.12 % SZS output start Proof % 58.99/59.12 %ClaNum:173(EqnAxiom:0) % 58.99/59.12 %VarNum:402(SingletonVarNum:178) % 58.99/59.12 %MaxLitNum:15 % 58.99/59.12 %MaxfuncDepth:1 % 58.99/59.12 %SharedTerms:53 % 58.99/59.12 %goalClause: 172 173 % 58.99/59.12 [1]P1(a1) % 58.99/59.12 [2]P2(a38) % 58.99/59.12 [3]P50(a2,a39) % 58.99/59.12 [4]P50(a2,a40) % 58.99/59.12 [5]P50(a2,a36) % 58.99/59.12 [6]P50(a2,a37) % 58.99/59.12 [7]P50(a2,a42) % 58.99/59.12 [8]P50(a2,a41) % 58.99/59.12 [9]P50(a2,a43) % 58.99/59.12 [10]P50(a2,a1) % 58.99/59.12 [11]P50(a41,a38) % 58.99/59.12 [12]~P2(a39) % 58.99/59.12 [13]~P2(a40) % 58.99/59.12 [14]~P2(a36) % 58.99/59.12 [15]~P2(a42) % 58.99/59.12 [16]~P2(a41) % 58.99/59.12 [17]~P8(a2) % 58.99/59.12 [18]~P12(a43) % 58.99/59.12 [19]~P15(a2) % 58.99/59.12 [20]~P21(a2) % 58.99/59.12 [21]~P26(a37) % 58.99/59.12 [22]~P30(a2) % 58.99/59.12 [23]~P37(a39) % 58.99/59.12 [24]~P40(a2) % 58.99/59.12 [25]~P51(x251) % 58.99/59.12 [26]P53(x261)+P52(x261) % 58.99/59.12 [27]~P3(x271)+P16(x271) % 58.99/59.12 [28]~P3(x281)+P41(x281) % 58.99/59.12 [29]~P5(x291)+P4(x291) % 58.99/59.12 [30]~P13(x301)+P5(x301) % 58.99/59.12 [31]~P8(x311)+P9(x311) % 58.99/59.12 [32]~P22(x321)+P13(x321) % 58.99/59.12 [33]~P15(x331)+P20(x331) % 58.99/59.12 [34]~P27(x341)+P22(x341) % 58.99/59.12 [35]~P38(x351)+P27(x351) % 58.99/59.12 [36]~P31(x361)+P29(x361) % 58.99/59.12 [37]~P34(x371)+P32(x371) % 58.99/59.12 [38]~P30(x381)+P35(x381) % 58.99/59.12 [39]~P48(x391)+P38(x391) % 58.99/59.12 [40]~P40(x401)+P42(x401) % 58.99/59.12 [44]~P53(x441)+~P52(x441) % 58.99/59.12 [45]~P5(x451)+~P6(x451) % 58.99/59.12 [46]~P8(x461)+~P10(x461) % 58.99/59.12 [47]~P31(x471)+~P2(x471) % 58.99/59.12 [48]~P34(x481)+~P2(x481) % 58.99/59.12 [49]~P43(x491)+~P2(x491) % 58.99/59.12 [50]~P46(x501)+~P2(x501) % 58.99/59.12 [51]~P13(x511)+~P14(x511) % 58.99/59.12 [52]~P15(x521)+~P17(x521) % 58.99/59.12 [53]~P22(x531)+~P23(x531) % 58.99/59.12 [54]~P21(x541)+~P24(x541) % 58.99/59.12 [55]~P21(x551)+~P25(x551) % 58.99/59.12 [56]~P27(x561)+~P28(x561) % 58.99/59.12 [57]~P30(x571)+~P33(x571) % 58.99/59.12 [58]~P38(x581)+~P39(x581) % 58.99/59.12 [59]~P43(x591)+~P37(x591) % 58.99/59.12 [60]~P40(x601)+~P45(x601) % 58.99/59.12 [61]~P46(x611)+~P44(x611) % 58.99/59.12 [62]~P48(x621)+~P49(x621) % 58.99/59.12 [107]P2(x1071)+~P50(a39,x1071) % 58.99/59.12 [108]P2(x1081)+~P50(a37,x1081) % 58.99/59.12 [109]~P2(x1091)+~P50(a43,x1091) % 58.99/59.12 [75]~P4(x751)+P3(f3(x751)) % 58.99/59.12 [76]~P7(x761)+P1(f14(x761)) % 58.99/59.12 [77]~P12(x771)+P2(f25(x771)) % 58.99/59.12 [78]~P18(x781)+P2(f4(x781)) % 58.99/59.12 [79]~P25(x791)+P2(f5(x791)) % 58.99/59.12 [80]~P29(x801)+P2(f11(x801)) % 58.99/59.12 [81]~P32(x811)+P2(f15(x811)) % 58.99/59.12 [82]~P9(x821)+P11(f26(x821)) % 58.99/59.12 [83]~P14(x831)+P8(f34(x831)) % 58.99/59.12 [84]~P20(x841)+P19(f6(x841)) % 58.99/59.12 [85]~P23(x851)+P15(f9(x851)) % 58.99/59.12 [86]~P28(x861)+P21(f12(x861)) % 58.99/59.12 [87]~P33(x871)+P31(f16(x871)) % 58.99/59.12 [88]~P36(x881)+P34(f17(x881)) % 58.99/59.12 [89]~P35(x891)+P36(f18(x891)) % 58.99/59.12 [90]~P39(x901)+P30(f19(x901)) % 58.99/59.12 [91]~P45(x911)+P43(f20(x911)) % 58.99/59.12 [92]~P47(x921)+P46(f23(x921)) % 58.99/59.12 [93]~P42(x931)+P47(f27(x931)) % 58.99/59.12 [94]~P49(x941)+P40(f28(x941)) % 58.99/59.12 [96]~P16(x961)+~P2(f7(x961)) % 58.99/59.12 [97]~P41(x971)+~P26(f21(x971)) % 58.99/59.12 [98]~P6(x981)+~P7(f29(x981)) % 58.99/59.12 [99]~P10(x991)+~P2(f32(x991)) % 58.99/59.12 [100]~P11(x1001)+~P2(f33(x1001)) % 58.99/59.12 [101]~P17(x1011)+~P12(f35(x1011)) % 58.99/59.12 [102]~P19(x1021)+~P18(f8(x1021)) % 58.99/59.12 [103]~P24(x1031)+~P2(f10(x1031)) % 58.99/59.12 [104]~P26(x1041)+~P2(f13(x1041)) % 58.99/59.12 [105]~P37(x1051)+~P2(f22(x1051)) % 58.99/59.12 [106]~P44(x1061)+~P2(f24(x1061)) % 58.99/59.12 [110]~P4(x1101)+P50(x1101,f3(x1101)) % 58.99/59.12 [111]~P7(x1111)+P50(x1111,f14(x1111)) % 58.99/59.12 [112]~P6(x1121)+P50(x1121,f29(x1121)) % 58.99/59.12 [113]~P10(x1131)+P50(x1131,f32(x1131)) % 58.99/59.12 [114]~P11(x1141)+P50(x1141,f33(x1141)) % 58.99/59.12 [115]~P9(x1151)+P50(x1151,f26(x1151)) % 58.99/59.12 [116]~P14(x1161)+P50(x1161,f34(x1161)) % 58.99/59.12 [117]~P12(x1171)+P50(x1171,f25(x1171)) % 58.99/59.12 [118]~P17(x1181)+P50(x1181,f35(x1181)) % 58.99/59.12 [119]~P18(x1191)+P50(x1191,f4(x1191)) % 58.99/59.12 [120]~P19(x1201)+P50(x1201,f8(x1201)) % 58.99/59.12 [121]~P16(x1211)+P50(x1211,f7(x1211)) % 58.99/59.12 [122]~P20(x1221)+P50(x1221,f6(x1221)) % 58.99/59.12 [123]~P23(x1231)+P50(x1231,f9(x1231)) % 58.99/59.12 [124]~P24(x1241)+P50(x1241,f10(x1241)) % 58.99/59.12 [125]~P25(x1251)+P50(x1251,f5(x1251)) % 58.99/59.12 [126]~P28(x1261)+P50(x1261,f12(x1261)) % 58.99/59.12 [127]~P29(x1271)+P50(x1271,f11(x1271)) % 58.99/59.12 [128]~P26(x1281)+P50(x1281,f13(x1281)) % 58.99/59.12 [129]~P33(x1291)+P50(x1291,f16(x1291)) % 58.99/59.12 [130]~P32(x1301)+P50(x1301,f15(x1301)) % 58.99/59.12 [131]~P36(x1311)+P50(x1311,f17(x1311)) % 58.99/59.12 [132]~P35(x1321)+P50(x1321,f18(x1321)) % 58.99/59.12 [133]~P39(x1331)+P50(x1331,f19(x1331)) % 58.99/59.12 [134]~P37(x1341)+P50(x1341,f22(x1341)) % 58.99/59.12 [135]~P41(x1351)+P50(x1351,f21(x1351)) % 58.99/59.12 [136]~P45(x1361)+P50(x1361,f20(x1361)) % 58.99/59.12 [137]~P44(x1371)+P50(x1371,f24(x1371)) % 58.99/59.12 [138]~P47(x1381)+P50(x1381,f23(x1381)) % 58.99/59.12 [139]~P42(x1391)+P50(x1391,f27(x1391)) % 58.99/59.12 [140]~P49(x1401)+P50(x1401,f28(x1401)) % 58.99/59.12 [41]P37(x411)+P43(x411)+P2(x411) % 58.99/59.12 [42]P44(x421)+P46(x421)+P2(x421) % 58.99/59.12 [43]P25(x431)+P21(x431)+P24(x431) % 58.99/59.12 [63]P5(x631)+~P4(x631)+P6(x631) % 58.99/59.12 [64]P8(x641)+~P9(x641)+P10(x641) % 58.99/59.12 [65]P31(x651)+~P29(x651)+P2(x651) % 58.99/59.12 [66]P34(x661)+~P32(x661)+P2(x661) % 58.99/59.12 [67]P13(x671)+~P5(x671)+P14(x671) % 58.99/59.12 [68]P15(x681)+~P20(x681)+P17(x681) % 58.99/59.12 [69]P22(x691)+~P13(x691)+P23(x691) % 58.99/59.12 [70]P27(x701)+~P22(x701)+P28(x701) % 58.99/59.12 [71]P30(x711)+~P35(x711)+P33(x711) % 58.99/59.12 [72]P38(x721)+~P27(x721)+P39(x721) % 58.99/59.12 [73]P40(x731)+~P42(x731)+P45(x731) % 58.99/59.12 [74]P48(x741)+~P38(x741)+P49(x741) % 58.99/59.12 [95]~P16(x951)+~P41(x951)+P3(x951) % 58.99/59.12 [141]~P50(x1411,x1412)+P16(x1411)+P2(x1412) % 58.99/59.12 [142]~P50(x1421,x1422)+P41(x1421)+P26(x1422) % 58.99/59.12 [143]~P50(x1432,x1431)+P7(x1431)+P6(x1432) % 58.99/59.12 [144]~P50(x1441,x1442)+P10(x1441)+P2(x1442) % 58.99/59.12 [145]~P50(x1452,x1451)+P2(x1451)+P11(x1452) % 58.99/59.12 [146]~P50(x1462,x1461)+P2(x1461)+P24(x1462) % 58.99/59.12 [147]~P50(x1472,x1471)+P2(x1471)+P26(x1472) % 58.99/59.12 [148]~P50(x1482,x1481)+P2(x1481)+P37(x1482) % 58.99/59.12 [149]~P50(x1492,x1491)+P2(x1491)+P44(x1492) % 58.99/59.12 [150]~P50(x1502,x1501)+P12(x1501)+P17(x1502) % 58.99/59.12 [151]~P50(x1512,x1511)+P18(x1511)+P19(x1512) % 58.99/59.12 [152]~P50(x1521,x1522)+P4(x1521)+~P3(x1522) % 58.99/59.12 [153]~P50(x1531,x1532)+P7(x1531)+~P1(x1532) % 58.99/59.12 [154]~P50(x1541,x1542)+P9(x1541)+~P11(x1542) % 58.99/59.12 [155]~P50(x1551,x1552)+P14(x1551)+~P8(x1552) % 58.99/59.12 [156]~P50(x1561,x1562)+P12(x1561)+~P2(x1562) % 58.99/59.12 [157]~P50(x1571,x1572)+P18(x1571)+~P2(x1572) % 58.99/59.12 [158]~P50(x1581,x1582)+P20(x1581)+~P19(x1582) % 58.99/59.12 [159]~P50(x1591,x1592)+P23(x1591)+~P15(x1592) % 58.99/59.12 [160]~P50(x1601,x1602)+P25(x1601)+~P2(x1602) % 58.99/59.12 [161]~P50(x1611,x1612)+P28(x1611)+~P21(x1612) % 58.99/59.12 [162]~P50(x1621,x1622)+P29(x1621)+~P2(x1622) % 58.99/59.12 [163]~P50(x1631,x1632)+P33(x1631)+~P31(x1632) % 58.99/59.12 [164]~P50(x1641,x1642)+P32(x1641)+~P2(x1642) % 58.99/59.12 [165]~P50(x1651,x1652)+P36(x1651)+~P34(x1652) % 58.99/59.12 [166]~P50(x1661,x1662)+P35(x1661)+~P36(x1662) % 58.99/59.12 [167]~P50(x1671,x1672)+P39(x1671)+~P30(x1672) % 58.99/59.12 [168]~P50(x1681,x1682)+P45(x1681)+~P43(x1682) % 58.99/59.12 [169]~P50(x1691,x1692)+P47(x1691)+~P46(x1692) % 58.99/59.12 [170]~P50(x1701,x1702)+P42(x1701)+~P47(x1702) % 58.99/59.12 [171]~P50(x1711,x1712)+P49(x1711)+~P40(x1712) % 58.99/59.12 [172]P51(a30)+P52(a31)+~P53(a31)+~P3(a2)+~P16(a2)+~P41(a2)+~P7(a2)+~P10(a2)+~P17(a2)+~P24(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2) % 58.99/59.12 [173]P51(a30)+P53(a31)+~P52(a31)+~P3(a2)+~P16(a2)+~P41(a2)+~P7(a2)+~P10(a2)+~P17(a2)+~P24(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2) % 58.99/59.12 %EqnAxiom % 58.99/59.12 % 58.99/59.12 %------------------------------------------- % 59.13/59.19 cnf(182,plain, % 59.13/59.19 (P24(a2)), % 59.13/59.19 inference(scs_inference,[],[2,3,12,47,48,49,50,146])). % 59.13/59.19 cnf(184,plain, % 59.13/59.19 (P17(a2)), % 59.13/59.19 inference(scs_inference,[],[2,3,9,12,18,47,48,49,50,146,150])). % 59.13/59.19 cnf(199,plain, % 59.13/59.19 (~P53(a31)+~P3(a2)+~P16(a2)+~P41(a2)+~P7(a2)+~P10(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)+P52(a31)), % 59.13/59.19 inference(scs_inference,[],[25,2,3,9,12,18,21,23,47,48,49,50,146,150,145,147,148,149,156,61,172])). % 59.13/59.19 cnf(200,plain, % 59.13/59.19 (P53(a31)+~P52(a31)+~P3(a2)+~P16(a2)+~P41(a2)+~P7(a2)+~P10(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)), % 59.13/59.19 inference(scs_inference,[],[25,184,182,173])). % 59.13/59.19 cnf(376,plain, % 59.13/59.19 (~P3(x3761)+~P2(f7(x3761))), % 59.13/59.19 inference(scs_inference,[],[27,96])). % 59.13/59.19 cnf(1286,plain, % 59.13/59.19 (~P34(x12861)+P2(f15(x12861))), % 59.13/59.19 inference(scs_inference,[],[37,81])). % 59.13/59.19 cnf(4942,plain, % 59.13/59.19 (P2(f4(a41))), % 59.13/59.19 inference(scs_inference,[],[2,11,78,157])). % 59.13/59.19 cnf(5595,plain, % 59.13/59.19 (~P2(f32(a2))), % 59.13/59.19 inference(scs_inference,[],[12,3,99,144])). % 59.13/59.19 cnf(5613,plain, % 59.13/59.19 (P44(x56131)+~P50(x56131,f32(a2))), % 59.13/59.19 inference(scs_inference,[],[2,15,18,5595,21,23,148,156,147,149])). % 59.13/59.19 cnf(5624,plain, % 59.13/59.19 (P11(x56241)+~P50(x56241,f32(a2))), % 59.13/59.19 inference(scs_inference,[],[2,12,18,5595,21,23,156,147,148,145])). % 59.13/59.19 cnf(5789,plain, % 59.13/59.19 (~P12(f35(a2))), % 59.13/59.19 inference(scs_inference,[],[18,9,101,150])). % 59.13/59.19 cnf(6067,plain, % 59.13/59.19 (~P50(x60671,f32(a2))+~P2(f24(x60671))), % 59.13/59.19 inference(scs_inference,[],[106,5613])). % 59.13/59.19 cnf(6340,plain, % 59.13/59.19 (~P3(x63401)+~P50(a39,f7(x63401))), % 59.13/59.19 inference(scs_inference,[],[376,107])). % 59.13/59.19 cnf(6886,plain, % 59.13/59.19 (~P34(x68861)+~P34(f15(x68861))), % 59.13/59.19 inference(scs_inference,[],[1286,48])). % 59.13/59.19 cnf(9798,plain, % 59.13/59.19 (P50(a2,f32(a2))), % 59.13/59.19 inference(scs_inference,[],[15,7,113,144])). % 59.13/59.19 cnf(9799,plain, % 59.13/59.19 (~P2(f24(a2))), % 59.13/59.19 inference(scs_inference,[],[9798,6067])). % 59.13/59.19 cnf(9829,plain, % 59.13/59.19 (P11(x98291)+~P50(x98291,f24(a2))), % 59.13/59.19 inference(scs_inference,[],[15,5789,2,9799,23,21,147,156,148,145])). % 59.13/59.19 cnf(10267,plain, % 59.13/59.19 (P50(a41,f4(a41))), % 59.13/59.19 inference(scs_inference,[],[2,11,119,157])). % 59.13/59.19 cnf(10358,plain, % 59.13/59.19 (P50(a2,f7(a2))), % 59.13/59.19 inference(scs_inference,[],[15,7,121,141])). % 59.13/59.19 cnf(11632,plain, % 59.13/59.19 (P50(a2,f24(a2))), % 59.13/59.19 inference(scs_inference,[],[9798,137,5613])). % 59.13/59.19 cnf(12269,plain, % 59.13/59.19 (P50(a2,f33(a2))), % 59.13/59.19 inference(scs_inference,[],[9798,5624,114])). % 59.13/59.19 cnf(13724,plain, % 59.13/59.19 (~P2(f33(a2))), % 59.13/59.19 inference(scs_inference,[],[11632,9829,100])). % 59.13/59.19 cnf(17361,plain, % 59.13/59.19 (P3(a2)+~P16(a2)), % 59.13/59.19 inference(scs_inference,[],[21,6,95,142])). % 59.13/59.19 cnf(20488,plain, % 59.13/59.19 (P41(a2)), % 59.13/59.19 inference(scs_inference,[],[5789,9799,2,10358,6,23,21,147,156,148,144,142])). % 59.13/59.19 cnf(20490,plain, % 59.13/59.19 (~P53(a31)+~P3(a2)+~P16(a2)+~P7(a2)+~P10(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)+P52(a31)), % 59.13/59.19 inference(scs_inference,[],[20488,199])). % 59.13/59.19 cnf(20491,plain, % 59.13/59.19 (P53(a31)+~P52(a31)+~P3(a2)+~P16(a2)+~P7(a2)+~P10(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)), % 59.13/59.19 inference(scs_inference,[],[20488,200])). % 59.13/59.19 cnf(20492,plain, % 59.13/59.19 (P16(a2)), % 59.13/59.19 inference(scs_inference,[],[5595,9798,141])). % 59.13/59.19 cnf(20494,plain, % 59.13/59.19 (P10(a2)), % 59.13/59.19 inference(scs_inference,[],[5595,9798,141,144])). % 59.13/59.19 cnf(20505,plain, % 59.13/59.19 (P3(a2)), % 59.13/59.19 inference(scs_inference,[],[20492,17361])). % 59.13/59.19 cnf(20516,plain, % 59.13/59.19 (~P53(a31)+~P7(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)+P52(a31)), % 59.13/59.19 inference(scs_inference,[],[20505,20492,20494,20490])). % 59.13/59.19 cnf(20517,plain, % 59.13/59.19 (P53(a31)+~P52(a31)+~P7(a2)+~P29(a41)+~P31(a41)+~P33(a2)+~P43(a39)+~P45(a2)), % 59.13/59.19 inference(scs_inference,[],[20505,20492,20494,20491])). % 59.13/59.19 cnf(56254,plain, % 59.13/59.19 (P7(a2)), % 59.13/59.19 inference(scs_inference,[],[1,184,20505,10,12,4942,107,108,109,118,6340,153])). % 59.13/59.19 cnf(56264,plain, % 59.13/59.20 (P29(a41)), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,10267,10,12,16,4942,107,108,109,118,6340,153,157,160,164,66,162])). % 59.13/59.20 cnf(56266,plain, % 59.13/59.20 (P43(a39)), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,10267,10,12,16,4942,23,107,108,109,118,6340,153,157,160,164,66,162,41])). % 59.13/59.20 cnf(56274,plain, % 59.13/59.20 (P2(f11(a41))), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,12269,10267,10,3,12,16,4942,23,13724,107,108,109,118,6340,153,157,160,164,66,162,41,148,147,156,80])). % 59.13/59.20 cnf(56278,plain, % 59.13/59.20 (~P2(f13(a2))), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,12269,10267,10,3,12,16,4942,23,13724,107,108,109,118,6340,153,157,160,164,66,162,41,148,147,156,80,81,104])). % 59.13/59.20 cnf(56292,plain, % 59.13/59.20 (P45(a2)), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,12269,10267,10,8,3,12,16,4942,23,13724,107,108,109,118,6340,153,157,160,164,66,162,41,148,147,156,80,81,104,105,6886,111,134,152,165,168])). % 59.13/59.20 cnf(56294,plain, % 59.13/59.20 (P31(a41)), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,12269,10267,10,8,3,12,16,4942,23,13724,107,108,109,118,6340,153,157,160,164,66,162,41,148,147,156,80,81,104,105,6886,111,134,152,165,168,65])). % 59.13/59.20 cnf(56296,plain, % 59.13/59.20 (P34(f17(a2))), % 59.13/59.20 inference(scs_inference,[],[1,184,20505,12269,10267,10,8,3,12,16,4942,23,13724,107,108,109,118,6340,153,157,160,164,66,162,41,148,147,156,80,81,104,105,6886,111,134,152,165,168,65,88])). % 59.13/59.20 cnf(56312,plain, % 59.13/59.20 (~P33(a2)+P52(a31)+~P53(a31)), % 59.13/59.20 inference(scs_inference,[],[56264,56294,56266,56292,56254,20516])). % 59.13/59.20 cnf(56313,plain, % 59.13/59.20 (~P33(a2)+~P52(a31)+P53(a31)), % 59.13/59.20 inference(scs_inference,[],[56254,56264,56294,56266,56292,20517])). % 59.13/59.20 cnf(56324,plain, % 59.13/59.20 (P33(a2)), % 59.13/59.20 inference(scs_inference,[],[56294,56274,56278,56296,20505,8,37,6340,108,109,107,163])). % 59.13/59.20 cnf(56350,plain, % 59.13/59.20 (~P53(a31)+P52(a31)), % 59.13/59.20 inference(scs_inference,[],[56324,56312])). % 59.13/59.20 cnf(56351,plain, % 59.13/59.20 (P53(a31)+~P52(a31)), % 59.13/59.20 inference(scs_inference,[],[56324,56313])). % 59.13/59.20 cnf(56493,plain, % 59.13/59.20 (P52(a31)), % 59.13/59.20 inference(scs_inference,[],[56350,26])). % 59.13/59.20 cnf(56494,plain, % 59.13/59.20 (P53(a31)), % 59.13/59.20 inference(scs_inference,[],[56493,56351])). % 59.13/59.20 cnf(56495,plain, % 59.13/59.20 (~P53(a31)), % 59.13/59.20 inference(scs_inference,[],[56493,44])). % 59.13/59.20 cnf(56509,plain, % 59.13/59.20 ($false), % 59.13/59.20 inference(scs_inference,[],[56494,56495]), % 59.13/59.20 ['proof']). % 59.21/59.26 % SZS output end Proof % 59.21/59.26 % Total time :58.400000s %------------------------------------------------------------------------------