%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS153+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 10:08:42 EDT 2024 % Result : Theorem 47.29s 47.37s % Output : CNFRefutation 47.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS153+1 : TPTP v8.2.0. Released v3.1.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jun 19 14:34:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 47.25/47.33 %------------------------------------------- % 47.25/47.33 % File :CSE---1.7 % 47.25/47.33 % Problem :theBenchmark % 47.25/47.33 % Transform :cnf % 47.25/47.33 % Format :tptp:raw % 47.25/47.33 % Command :java -jar mcs_scs.jar %d %s % 47.25/47.33 % 47.25/47.33 % Result :Theorem 46.700000s % 47.25/47.33 % Output :CNFRefutation 46.700000s % 47.25/47.33 %------------------------------------------- % 47.29/47.34 %------------------------------------------------------------------------------ % 47.29/47.34 % File : KRS153+1 : TPTP v8.2.0. Released v3.1.0. % 47.29/47.34 % Domain : Knowledge Representation (Semantic Web) % 47.29/47.34 % Problem : DL Test: k_poly ABox test from DL98 systems comparison % 47.29/47.34 % Version : Especial. % 47.29/47.34 % English : % 47.29/47.34 % 47.29/47.34 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 47.29/47.34 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 47.29/47.34 % Source : [Bec03] % 47.29/47.34 % Names : positive_description-logic-Manifest208 [Bec03] % 47.29/47.34 % 47.29/47.34 % Status : Theorem % 47.29/47.34 % 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.24 v6.0.0, 0.25 v5.4.0, 0.26 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.10 v4.1.0, 0.06 v4.0.1, 0.11 v4.0.0, 0.15 v3.7.0, 0.33 v3.5.0, 0.25 v3.3.0, 0.22 v3.2.0, 0.33 v3.1.0 % 47.29/47.34 % Syntax : Number of formulae : 201 ( 99 unt; 0 def) % 47.29/47.34 % Number of atoms : 408 ( 0 equ) % 47.29/47.34 % Maximal formula atoms : 49 ( 2 avg) % 47.29/47.34 % Number of connectives : 333 ( 126 ~; 0 |; 106 &) % 47.29/47.34 % ( 60 <=>; 41 =>; 0 <=; 0 <~>) % 47.29/47.34 % Maximal formula depth : 47 ( 3 avg) % 47.29/47.34 % Maximal term depth : 1 ( 1 avg) % 47.29/47.34 % Number of predicates : 72 ( 72 usr; 0 prp; 1-2 aty) % 47.29/47.34 % Number of functors : 16 ( 16 usr; 16 con; 0-0 aty) % 47.29/47.34 % Number of variables : 131 ( 103 !; 28 ?) % 47.29/47.34 % SPC : FOF_THM_RFO_NEQ % 47.29/47.34 % 47.29/47.34 % Comments : Sean Bechhofer says there are some errors in the encoding of % 47.29/47.34 % datatypes, so this problem may not be perfect. At least it's % 47.29/47.34 % still representative of the type of reasoning required for OWL. % 47.29/47.34 %------------------------------------------------------------------------------ % 47.29/47.34 %----Thing and Nothing % 47.29/47.34 fof(axiom_0,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cowlThing(X) % 47.29/47.34 & ~ cowlNothing(X) ) ). % 47.29/47.34 % 47.29/47.34 %----String and Integer disjoint % 47.29/47.34 fof(axiom_1,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( xsd_string(X) % 47.29/47.34 <=> ~ xsd_integer(X) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC10 % 47.29/47.34 fof(axiom_2,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC10(X) % 47.29/47.34 <=> ( cC8(X) % 47.29/47.34 & cC6(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC100 % 47.29/47.34 fof(axiom_3,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC100(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & ~ cC98(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC104 % 47.29/47.34 fof(axiom_4,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC104(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & ~ cC102(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC106 % 47.29/47.34 fof(axiom_5,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC106(X) % 47.29/47.34 <=> ( ~ cC100(X) % 47.29/47.34 & cC104(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC108 % 47.29/47.34 fof(axiom_6,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC108(X) % 47.29/47.34 <=> ( cC28(X) % 47.29/47.34 & cC106(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC110 % 47.29/47.34 fof(axiom_7,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC110(X) % 47.29/47.34 <=> ( ~ cC12(X) % 47.29/47.34 & ~ cC4(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC112 % 47.29/47.34 fof(axiom_8,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC112(X) % 47.29/47.34 <=> ( ~ cC102(X) % 47.29/47.34 & cC110(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC116 % 47.29/47.34 fof(axiom_9,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC116(X) % 47.29/47.34 <=> ( cC112(X) % 47.29/47.34 & ~ cC114(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC120 % 47.29/47.34 fof(axiom_10,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC120(X) % 47.29/47.34 <=> ( cC116(X) % 47.29/47.34 & ~ cC118(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC122 % 47.29/47.34 fof(axiom_11,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC122(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & ~ cC120(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC124 % 47.29/47.34 fof(axiom_12,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC124(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & cC122(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC126 % 47.29/47.34 fof(axiom_13,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC126(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & cC124(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC128 % 47.29/47.34 fof(axiom_14,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC128(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & cC126(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC130 % 47.29/47.34 fof(axiom_15,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC130(X) % 47.29/47.34 <=> ? [Y] : % 47.29/47.34 ( rR1(X,Y) % 47.29/47.34 & cC128(Y) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC14 % 47.29/47.34 fof(axiom_16,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC14(X) % 47.29/47.34 <=> ( cC10(X) % 47.29/47.34 & cC12(X) ) ) ). % 47.29/47.34 % 47.29/47.34 %----Equality cC18 % 47.29/47.34 fof(axiom_17,axiom, % 47.29/47.34 ! [X] : % 47.29/47.34 ( cC18(X) % 47.29/47.34 <=> ( cC14(X) % 47.29/47.35 & cC16(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC20 % 47.29/47.35 fof(axiom_18,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC20(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC18(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC22 % 47.29/47.35 fof(axiom_19,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC22(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC20(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC24 % 47.29/47.35 fof(axiom_20,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC24(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC22(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC26 % 47.29/47.35 fof(axiom_21,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC26(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC24(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC28 % 47.29/47.35 fof(axiom_22,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC28(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC26(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC30 % 47.29/47.35 fof(axiom_23,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC30(X) % 47.29/47.35 <=> ( cC4(X) % 47.29/47.35 & cC2(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC32 % 47.29/47.35 fof(axiom_24,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC32(X) % 47.29/47.35 <=> ( ~ cC2(X) % 47.29/47.35 & ~ cC4(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC34 % 47.29/47.35 fof(axiom_25,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC34(X) % 47.29/47.35 <=> ( ~ cC32(X) % 47.29/47.35 & ~ cC30(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC36 % 47.29/47.35 fof(axiom_26,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC36(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC34(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC38 % 47.29/47.35 fof(axiom_27,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC38(X) % 47.29/47.35 <=> ( ~ cC36(X) % 47.29/47.35 & cTOP(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC40 % 47.29/47.35 fof(axiom_28,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC40(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC38(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC42 % 47.29/47.35 fof(axiom_29,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC42(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC8(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC44 % 47.29/47.35 fof(axiom_30,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC44(X) % 47.29/47.35 <=> ( ~ cC40(X) % 47.29/47.35 & cC42(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC46 % 47.29/47.35 fof(axiom_31,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC46(X) % 47.29/47.35 <=> ( cC8(X) % 47.29/47.35 & cC4(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC48 % 47.29/47.35 fof(axiom_32,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC48(X) % 47.29/47.35 <=> ( ~ cC8(X) % 47.29/47.35 & ~ cC4(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC50 % 47.29/47.35 fof(axiom_33,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC50(X) % 47.29/47.35 <=> ( ~ cC46(X) % 47.29/47.35 & ~ cC48(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC52 % 47.29/47.35 fof(axiom_34,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC52(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC50(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC54 % 47.29/47.35 fof(axiom_35,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC54(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC52(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC56 % 47.29/47.35 fof(axiom_36,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC56(X) % 47.29/47.35 <=> ( cC44(X) % 47.29/47.35 & ~ cC54(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC58 % 47.29/47.35 fof(axiom_37,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC58(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC56(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC6 % 47.29/47.35 fof(axiom_38,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC6(X) % 47.29/47.35 <=> ( cC4(X) % 47.29/47.35 & cC2(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC60 % 47.29/47.35 fof(axiom_39,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC60(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC12(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC62 % 47.29/47.35 fof(axiom_40,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC62(X) % 47.29/47.35 <=> ( cC60(X) % 47.29/47.35 & ~ cC58(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC64 % 47.29/47.35 fof(axiom_41,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC64(X) % 47.29/47.35 <=> ( cC8(X) % 47.29/47.35 & cC12(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC66 % 47.29/47.35 fof(axiom_42,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC66(X) % 47.29/47.35 <=> ( ~ cC8(X) % 47.29/47.35 & ~ cC12(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC68 % 47.29/47.35 fof(axiom_43,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC68(X) % 47.29/47.35 <=> ( ~ cC64(X) % 47.29/47.35 & ~ cC66(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC70 % 47.29/47.35 fof(axiom_44,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC70(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC68(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC72 % 47.29/47.35 fof(axiom_45,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC72(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC70(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC74 % 47.29/47.35 fof(axiom_46,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC74(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & cC72(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC76 % 47.29/47.35 fof(axiom_47,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC76(X) % 47.29/47.35 <=> ( ~ cC74(X) % 47.29/47.35 & cC62(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC78 % 47.29/47.35 fof(axiom_48,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC78(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC76(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC80 % 47.29/47.35 fof(axiom_49,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC80(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC16(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC82 % 47.29/47.35 fof(axiom_50,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC82(X) % 47.29/47.35 <=> ( ~ cC78(X) % 47.29/47.35 & cC80(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC84 % 47.29/47.35 fof(axiom_51,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC84(X) % 47.29/47.35 <=> ( cC2(X) % 47.29/47.35 & cC12(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC86 % 47.29/47.35 fof(axiom_52,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC86(X) % 47.29/47.35 <=> ( ~ cC12(X) % 47.29/47.35 & ~ cC2(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC88 % 47.29/47.35 fof(axiom_53,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC88(X) % 47.29/47.35 <=> ( ~ cC84(X) % 47.29/47.35 & ~ cC86(X) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC90 % 47.29/47.35 fof(axiom_54,axiom, % 47.29/47.35 ! [X] : % 47.29/47.35 ( cC90(X) % 47.29/47.35 <=> ? [Y] : % 47.29/47.35 ( rR1(X,Y) % 47.29/47.35 & ~ cC88(Y) ) ) ). % 47.29/47.35 % 47.29/47.35 %----Equality cC92 % 47.29/47.35 fof(axiom_55,axiom, % 47.29/47.35 ! [X] : % 47.29/47.36 ( cC92(X) % 47.29/47.36 <=> ? [Y] : % 47.29/47.36 ( rR1(X,Y) % 47.29/47.36 & cC90(Y) ) ) ). % 47.29/47.36 % 47.29/47.36 %----Equality cC94 % 47.29/47.36 fof(axiom_56,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( cC94(X) % 47.29/47.36 <=> ? [Y] : % 47.29/47.36 ( rR1(X,Y) % 47.29/47.36 & cC92(Y) ) ) ). % 47.29/47.36 % 47.29/47.36 %----Equality cC96 % 47.29/47.36 fof(axiom_57,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( cC96(X) % 47.29/47.36 <=> ? [Y] : % 47.29/47.36 ( rR1(X,Y) % 47.29/47.36 & cC94(Y) ) ) ). % 47.29/47.36 % 47.29/47.36 %----Equality cC98 % 47.29/47.36 fof(axiom_58,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( cC98(X) % 47.29/47.36 <=> ( ~ cC96(X) % 47.29/47.36 & cC82(X) ) ) ). % 47.29/47.36 % 47.29/47.36 %----Equality cTEST % 47.29/47.36 fof(axiom_59,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( cTEST(X) % 47.29/47.36 <=> ( cC108(X) % 47.29/47.36 & cC130(X) ) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16439 % 47.29/47.36 fof(axiom_60,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16439,X) % 47.29/47.36 => cC98(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16439 % 47.29/47.36 fof(axiom_61,axiom, % 47.29/47.36 cTEST(iV16439) ). % 47.29/47.36 % 47.29/47.36 %----iV16439 % 47.29/47.36 fof(axiom_62,axiom, % 47.29/47.36 ~ cC100(iV16439) ). % 47.29/47.36 % 47.29/47.36 %----iV16439 % 47.29/47.36 fof(axiom_63,axiom, % 47.29/47.36 cowlThing(iV16439) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_64,axiom, % 47.29/47.36 rR1(iV16439,iV16440) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_65,axiom, % 47.29/47.36 rR1(iV16439,iV16442) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_66,axiom, % 47.29/47.36 rR1(iV16439,iV16441) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_67,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16440,X) % 47.29/47.36 => cC76(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_68,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16440,X) % 47.29/47.36 => ~ cC94(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_69,axiom, % 47.29/47.36 ~ cC102(iV16440) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_70,axiom, % 47.29/47.36 ~ cC78(iV16440) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_71,axiom, % 47.29/47.36 ~ cC96(iV16440) ). % 47.29/47.36 % 47.29/47.36 %----iV16440 % 47.29/47.36 fof(axiom_72,axiom, % 47.29/47.36 cowlThing(iV16440) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_73,axiom, % 47.29/47.36 rR1(iV16440,iV16463) ). % 47.29/47.36 % 47.29/47.36 %----iV16441 % 47.29/47.36 fof(axiom_74,axiom, % 47.29/47.36 cowlThing(iV16441) ). % 47.29/47.36 % 47.29/47.36 %----iV16442 % 47.29/47.36 fof(axiom_75,axiom, % 47.29/47.36 cowlThing(iV16442) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_76,axiom, % 47.29/47.36 ~ cC36(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_77,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16448,X) % 47.29/47.36 => cC68(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_78,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16448,X) % 47.29/47.36 => cC34(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_79,axiom, % 47.29/47.36 cTOP(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_80,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16448,X) % 47.29/47.36 => cC50(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_81,axiom, % 47.29/47.36 ~ cC52(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_82,axiom, % 47.29/47.36 ~ cC70(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_83,axiom, % 47.29/47.36 ~ cC90(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_84,axiom, % 47.29/47.36 cowlThing(iV16448) ). % 47.29/47.36 % 47.29/47.36 %----iV16448 % 47.29/47.36 fof(axiom_85,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16448,X) % 47.29/47.36 => cC88(X) ) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_86,axiom, % 47.29/47.36 rR1(iV16448,iV16449) ). % 47.29/47.36 % 47.29/47.36 %----iV16449 % 47.29/47.36 fof(axiom_87,axiom, % 47.29/47.36 cowlThing(iV16449) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_88,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16453,X) % 47.29/47.36 => ~ cC92(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_89,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16453,X) % 47.29/47.36 => ~ cC72(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_90,axiom, % 47.29/47.36 ~ cC16(iV16453) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_91,axiom, % 47.29/47.36 ~ cC58(iV16453) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_92,axiom, % 47.29/47.36 ~ cC74(iV16453) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_93,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16453,X) % 47.29/47.36 => cC56(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_94,axiom, % 47.29/47.36 cowlThing(iV16453) ). % 47.29/47.36 % 47.29/47.36 %----iV16453 % 47.29/47.36 fof(axiom_95,axiom, % 47.29/47.36 ~ cC94(iV16453) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_96,axiom, % 47.29/47.36 rR1(iV16453,iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_97,axiom, % 47.29/47.36 ~ cC12(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_98,axiom, % 47.29/47.36 ~ cC40(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_99,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16455,X) % 47.29/47.36 => ~ cC90(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_100,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16455,X) % 47.29/47.36 => ~ cC70(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_101,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16455,X) % 47.29/47.36 => ~ cC52(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_102,axiom, % 47.29/47.36 ~ cC72(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_103,axiom, % 47.29/47.36 ~ cC54(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_104,axiom, % 47.29/47.36 ~ cC92(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_105,axiom, % 47.29/47.36 cowlThing(iV16455) ). % 47.29/47.36 % 47.29/47.36 %----iV16455 % 47.29/47.36 fof(axiom_106,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16455,X) % 47.29/47.36 => cC38(X) ) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_107,axiom, % 47.29/47.36 rR1(iV16455,iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_108,axiom, % 47.29/47.36 ~ cC36(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_109,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16457,X) % 47.29/47.36 => cC88(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_110,axiom, % 47.29/47.36 ~ cC52(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_111,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16457,X) % 47.29/47.36 => cC68(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_112,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16457,X) % 47.29/47.36 => cC34(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_113,axiom, % 47.29/47.36 cTOP(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_114,axiom, % 47.29/47.36 ~ cC90(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_115,axiom, % 47.29/47.36 ~ cC70(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_116,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16457,X) % 47.29/47.36 => cC50(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_117,axiom, % 47.29/47.36 cowlThing(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16457 % 47.29/47.36 fof(axiom_118,axiom, % 47.29/47.36 ~ cC8(iV16457) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_119,axiom, % 47.29/47.36 cC4(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_120,axiom, % 47.29/47.36 ~ cC48(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_121,axiom, % 47.29/47.36 ~ cC30(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_122,axiom, % 47.29/47.36 ~ cC6(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_123,axiom, % 47.29/47.36 ~ cC86(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_124,axiom, % 47.29/47.36 ~ cC46(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_125,axiom, % 47.29/47.36 ~ cC14(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_126,axiom, % 47.29/47.36 ~ cC18(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_127,axiom, % 47.29/47.36 ~ cC66(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_128,axiom, % 47.29/47.36 cC12(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_129,axiom, % 47.29/47.36 ~ cC8(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_130,axiom, % 47.29/47.36 ~ cC2(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_131,axiom, % 47.29/47.36 ~ cC10(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_132,axiom, % 47.29/47.36 ~ cC84(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_133,axiom, % 47.29/47.36 ~ cC64(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_134,axiom, % 47.29/47.36 cowlThing(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16459 % 47.29/47.36 fof(axiom_135,axiom, % 47.29/47.36 ~ cC32(iV16459) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_136,axiom, % 47.29/47.36 ~ cC90(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_137,axiom, % 47.29/47.36 ~ cC36(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_138,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16460,X) % 47.29/47.36 => cC68(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_139,axiom, % 47.29/47.36 ~ cC52(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_140,axiom, % 47.29/47.36 cTOP(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_141,axiom, % 47.29/47.36 ~ cC8(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_142,axiom, % 47.29/47.36 ~ cC70(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_143,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16460,X) % 47.29/47.36 => cC88(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_144,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16460,X) % 47.29/47.36 => cC50(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_145,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16460,X) % 47.29/47.36 => cC34(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16460 % 47.29/47.36 fof(axiom_146,axiom, % 47.29/47.36 cowlThing(iV16460) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_147,axiom, % 47.29/47.36 ~ cC40(iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_148,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16461,X) % 47.29/47.36 => ~ cC52(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_149,axiom, % 47.29/47.36 ~ cC92(iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_150,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16461,X) % 47.29/47.36 => ~ cC90(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_151,axiom, % 47.29/47.36 ~ cC12(iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_152,axiom, % 47.29/47.36 ~ cC54(iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_153,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16461,X) % 47.29/47.36 => ~ cC70(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_154,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16461,X) % 47.29/47.36 => cC38(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_155,axiom, % 47.29/47.36 cowlThing(iV16461) ). % 47.29/47.36 % 47.29/47.36 %----iV16461 % 47.29/47.36 fof(axiom_156,axiom, % 47.29/47.36 ~ cC72(iV16461) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_157,axiom, % 47.29/47.36 rR1(iV16461,iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_158,axiom, % 47.29/47.36 ~ cC52(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_159,axiom, % 47.29/47.36 ~ cC8(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_160,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16462,X) % 47.29/47.36 => cC68(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_161,axiom, % 47.29/47.36 ~ cC36(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_162,axiom, % 47.29/47.36 cTOP(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_163,axiom, % 47.29/47.36 ~ cC90(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_164,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16462,X) % 47.29/47.36 => cC34(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_165,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16462,X) % 47.29/47.36 => cC50(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_166,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16462,X) % 47.29/47.36 => cC88(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_167,axiom, % 47.29/47.36 ~ cC70(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16462 % 47.29/47.36 fof(axiom_168,axiom, % 47.29/47.36 cowlThing(iV16462) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_169,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16463,X) % 47.29/47.36 => ~ cC92(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_170,axiom, % 47.29/47.36 ~ cC94(iV16463) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_171,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16463,X) % 47.29/47.36 => cC56(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_172,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16463,X) % 47.29/47.36 => ~ cC72(X) ) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_173,axiom, % 47.29/47.36 ~ cC74(iV16463) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_174,axiom, % 47.29/47.36 ~ cC58(iV16463) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_175,axiom, % 47.29/47.36 ~ cC16(iV16463) ). % 47.29/47.36 % 47.29/47.36 %----iV16463 % 47.29/47.36 fof(axiom_176,axiom, % 47.29/47.36 cowlThing(iV16463) ). % 47.29/47.36 % 47.29/47.36 fof(axiom_177,axiom, % 47.29/47.36 rR1(iV16463,iV16464) ). % 47.29/47.36 % 47.29/47.36 %----iV16464 % 47.29/47.36 fof(axiom_178,axiom, % 47.29/47.36 ~ cC72(iV16464) ). % 47.29/47.36 % 47.29/47.36 %----iV16464 % 47.29/47.36 fof(axiom_179,axiom, % 47.29/47.36 ~ cC40(iV16464) ). % 47.29/47.36 % 47.29/47.36 %----iV16464 % 47.29/47.36 fof(axiom_180,axiom, % 47.29/47.36 ! [X] : % 47.29/47.36 ( rR1(iV16464,X) % 47.29/47.36 => ~ cC70(X) ) ). % 47.29/47.36 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_181,axiom, % 47.29/47.37 ~ cC54(iV16464) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_182,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16464,X) % 47.29/47.37 => cC38(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_183,axiom, % 47.29/47.37 ~ cC12(iV16464) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_184,axiom, % 47.29/47.37 ~ cC92(iV16464) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_185,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16464,X) % 47.29/47.37 => ~ cC90(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_186,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16464,X) % 47.29/47.37 => ~ cC52(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16464 % 47.29/47.37 fof(axiom_187,axiom, % 47.29/47.37 cowlThing(iV16464) ). % 47.29/47.37 % 47.29/47.37 fof(axiom_188,axiom, % 47.29/47.37 rR1(iV16464,iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_189,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16465,X) % 47.29/47.37 => cC68(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_190,axiom, % 47.29/47.37 ~ cC70(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_191,axiom, % 47.29/47.37 ~ cC52(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_192,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16465,X) % 47.29/47.37 => cC88(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_193,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16465,X) % 47.29/47.37 => cC34(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_194,axiom, % 47.29/47.37 ~ cC8(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_195,axiom, % 47.29/47.37 ~ cC36(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_196,axiom, % 47.29/47.37 cTOP(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_197,axiom, % 47.29/47.37 ! [X] : % 47.29/47.37 ( rR1(iV16465,X) % 47.29/47.37 => cC50(X) ) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_198,axiom, % 47.29/47.37 cowlThing(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(axiom_199,axiom, % 47.29/47.37 ~ cC90(iV16465) ). % 47.29/47.37 % 47.29/47.37 %----Thing and Nothing % 47.29/47.37 %----String and Integer disjoint % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16439 % 47.29/47.37 %----iV16440 % 47.29/47.37 %----iV16440 % 47.29/47.37 %----iV16440 % 47.29/47.37 %----iV16440 % 47.29/47.37 %----iV16448 % 47.29/47.37 %----iV16448 % 47.29/47.37 %----iV16453 % 47.29/47.37 %----iV16453 % 47.29/47.37 %----iV16453 % 47.29/47.37 %----iV16453 % 47.29/47.37 %----iV16455 % 47.29/47.37 %----iV16455 % 47.29/47.37 %----iV16455 % 47.29/47.37 %----iV16455 % 47.29/47.37 %----iV16457 % 47.29/47.37 %----iV16457 % 47.29/47.37 %----iV16459 % 47.29/47.37 %----iV16459 % 47.29/47.37 %----iV16459 % 47.29/47.37 %----iV16459 % 47.29/47.37 %----iV16459 % 47.29/47.37 %----iV16460 % 47.29/47.37 %----iV16460 % 47.29/47.37 %----iV16461 % 47.29/47.37 %----iV16461 % 47.29/47.37 %----iV16461 % 47.29/47.37 %----iV16461 % 47.29/47.37 %----iV16462 % 47.29/47.37 %----iV16462 % 47.29/47.37 %----iV16463 % 47.29/47.37 %----iV16463 % 47.29/47.37 %----iV16463 % 47.29/47.37 %----iV16463 % 47.29/47.37 %----iV16464 % 47.29/47.37 %----iV16464 % 47.29/47.37 %----iV16464 % 47.29/47.37 %----iV16464 % 47.29/47.37 %----iV16465 % 47.29/47.37 %----iV16465 % 47.29/47.37 fof(the_axiom,conjecture, % 47.29/47.37 ( ! [X] : % 47.29/47.37 ( cowlThing(X) % 47.29/47.37 & ~ cowlNothing(X) ) % 47.29/47.37 & ! [X] : % 47.29/47.37 ( xsd_string(X) % 47.29/47.37 <=> ~ xsd_integer(X) ) % 47.29/47.37 & cC106(iV16439) % 47.29/47.37 & cC28(iV16439) % 47.29/47.37 & cC130(iV16439) % 47.29/47.37 & cowlThing(iV16439) % 47.29/47.37 & cC108(iV16439) % 47.29/47.37 & cC104(iV16439) % 47.29/47.37 & cC80(iV16440) % 47.29/47.37 & cowlThing(iV16440) % 47.29/47.37 & cC82(iV16440) % 47.29/47.37 & cC98(iV16440) % 47.29/47.37 & cowlThing(iV16448) % 47.29/47.37 & cC38(iV16448) % 47.29/47.37 & cC62(iV16453) % 47.29/47.37 & cowlThing(iV16453) % 47.29/47.37 & cC76(iV16453) % 47.29/47.37 & cC60(iV16453) % 47.29/47.37 & cC44(iV16455) % 47.29/47.37 & cowlThing(iV16455) % 47.29/47.37 & cC56(iV16455) % 47.29/47.37 & cC42(iV16455) % 47.29/47.37 & cowlThing(iV16457) % 47.29/47.37 & cC38(iV16457) % 47.29/47.37 & cC68(iV16459) % 47.29/47.37 & cowlThing(iV16459) % 47.29/47.37 & cC88(iV16459) % 47.29/47.37 & cC50(iV16459) % 47.29/47.37 & cC34(iV16459) % 47.29/47.37 & cowlThing(iV16460) % 47.29/47.37 & cC38(iV16460) % 47.29/47.37 & cC44(iV16461) % 47.29/47.37 & cowlThing(iV16461) % 47.29/47.37 & cC56(iV16461) % 47.29/47.37 & cC42(iV16461) % 47.29/47.37 & cowlThing(iV16462) % 47.29/47.37 & cC38(iV16462) % 47.29/47.37 & cC62(iV16463) % 47.29/47.37 & cowlThing(iV16463) % 47.29/47.37 & cC76(iV16463) % 47.29/47.37 & cC60(iV16463) % 47.29/47.37 & cC44(iV16464) % 47.29/47.37 & cowlThing(iV16464) % 47.29/47.37 & cC56(iV16464) % 47.29/47.37 & cC42(iV16464) % 47.29/47.37 & cowlThing(iV16465) % 47.29/47.37 & cC38(iV16465) ) ). % 47.29/47.37 % 47.29/47.37 %------------------------------------------------------------------------------ % 47.29/47.37 %------------------------------------------- % 47.29/47.37 % Proof found % 47.29/47.37 % SZS status Theorem for theBenchmark % 47.29/47.37 % SZS output start Proof % 47.29/47.37 %ClaNum:303(EqnAxiom:0) % 47.29/47.37 %VarNum:549(SingletonVarNum:246) % 47.29/47.37 %MaxLitNum:35 % 47.29/47.37 %MaxfuncDepth:1 % 47.29/47.37 %SharedTerms:137 % 47.29/47.37 %goalClause: 302 303 % 47.29/47.37 [1]P1(a1) % 47.29/47.37 [2]P13(a1) % 47.29/47.37 [3]P34(a2) % 47.29/47.37 [4]P34(a41) % 47.29/47.37 [5]P34(a37) % 47.29/47.37 [6]P34(a42) % 47.29/47.37 [7]P34(a44) % 47.29/47.37 [8]P35(a3) % 47.29/47.37 [9]P68(a3,a34) % 47.29/47.37 [10]P68(a3,a35) % 47.29/47.37 [11]P68(a3,a36) % 47.29/47.37 [12]P68(a34,a45) % 47.29/47.37 [13]P68(a45,a46) % 47.29/47.37 [14]P68(a2,a38) % 47.29/47.37 [15]P68(a39,a43) % 47.29/47.37 [16]P68(a43,a42) % 47.29/47.37 [17]P68(a40,a41) % 47.29/47.37 [18]P68(a46,a44) % 47.29/47.37 [19]~P2(a1) % 47.29/47.37 [20]~P36(a41) % 47.29/47.37 [21]~P36(a37) % 47.29/47.37 [22]~P36(a1) % 47.29/47.37 [23]~P36(a42) % 47.29/47.37 [24]~P36(a44) % 47.29/47.37 [25]~P37(a1) % 47.29/47.37 [26]~P3(a3) % 47.29/47.37 [27]~P4(a34) % 47.29/47.37 [28]~P1(a43) % 47.29/47.37 [29]~P1(a40) % 47.29/47.37 [30]~P1(a46) % 47.29/47.37 [31]~P14(a1) % 47.29/47.37 [32]~P21(a1) % 47.29/47.37 [33]~P22(a45) % 47.29/47.37 [34]~P22(a39) % 47.29/47.37 [35]~P23(a1) % 47.29/47.37 [36]~P24(a1) % 47.29/47.37 [37]~P30(a1) % 47.29/47.37 [38]~P31(a2) % 47.29/47.37 [39]~P31(a41) % 47.29/47.37 [40]~P31(a37) % 47.29/47.37 [41]~P31(a42) % 47.29/47.37 [42]~P31(a44) % 47.29/47.37 [43]~P38(a43) % 47.29/47.37 [44]~P38(a40) % 47.29/47.37 [45]~P38(a46) % 47.29/47.37 [46]~P39(a1) % 47.29/47.37 [47]~P42(a1) % 47.29/47.37 [48]~P43(a2) % 47.29/47.37 [49]~P43(a41) % 47.29/47.37 [50]~P43(a37) % 47.29/47.37 [51]~P43(a42) % 47.29/47.37 [52]~P43(a44) % 47.29/47.37 [53]~P45(a43) % 47.29/47.37 [54]~P45(a40) % 47.29/47.37 [55]~P45(a46) % 47.29/47.37 [56]~P46(a45) % 47.29/47.37 [57]~P46(a39) % 47.29/47.37 [58]~P48(a1) % 47.29/47.37 [59]~P51(a1) % 47.29/47.37 [60]~P52(a2) % 47.29/47.37 [61]~P52(a41) % 47.29/47.37 [62]~P52(a37) % 47.29/47.37 [63]~P52(a42) % 47.29/47.37 [64]~P52(a44) % 47.29/47.37 [65]~P54(a43) % 47.29/47.37 [66]~P54(a40) % 47.29/47.37 [67]~P54(a46) % 47.29/47.37 [68]~P55(a45) % 47.29/47.37 [69]~P55(a39) % 47.29/47.37 [70]~P56(a34) % 47.29/47.37 [71]~P58(a1) % 47.29/47.37 [72]~P61(a1) % 47.29/47.37 [73]~P62(a2) % 47.29/47.37 [74]~P62(a41) % 47.29/47.37 [75]~P62(a37) % 47.29/47.37 [76]~P62(a42) % 47.29/47.37 [77]~P62(a44) % 47.29/47.37 [78]~P64(a43) % 47.29/47.37 [79]~P64(a40) % 47.29/47.37 [80]~P64(a46) % 47.29/47.37 [81]~P65(a45) % 47.29/47.37 [82]~P65(a39) % 47.29/47.37 [83]~P66(a34) % 47.29/47.37 [84]~P69(x841) % 47.29/47.37 [85]P71(x851)+P70(x851) % 47.29/47.37 [86]~P14(x861)+P2(x861) % 47.29/47.37 [87]~P2(x871)+P36(x871) % 47.29/47.37 [88]~P39(x881)+P36(x881) % 47.29/47.37 [89]~P48(x891)+P36(x891) % 47.29/47.37 [90]~P2(x901)+P37(x901) % 47.29/47.37 [91]~P6(x911)+P5(x911) % 47.29/47.37 [92]~P7(x921)+P6(x921) % 47.29/47.37 [93]~P35(x931)+P7(x931) % 47.29/47.37 [94]~P7(x941)+P25(x941) % 47.29/47.37 [95]~P9(x951)+P8(x951) % 47.29/47.37 [96]~P14(x961)+P1(x961) % 47.29/47.37 [97]~P48(x971)+P1(x971) % 47.29/47.37 [98]~P58(x981)+P1(x981) % 47.29/47.37 [99]~P37(x991)+P13(x991) % 47.29/47.37 [100]~P23(x1001)+P13(x1001) % 47.29/47.37 [101]~P39(x1011)+P13(x1011) % 47.29/47.37 [102]~P10(x1021)+P9(x1021) % 47.29/47.37 [103]~P15(x1031)+P10(x1031) % 47.29/47.37 [104]~P35(x1041)+P16(x1041) % 47.29/47.37 [105]~P21(x1051)+P14(x1051) % 47.29/47.37 [106]~P21(x1061)+P22(x1061) % 47.29/47.37 [107]~P37(x1071)+P24(x1071) % 47.29/47.37 [108]~P23(x1081)+P24(x1081) % 47.29/47.37 [109]~P58(x1091)+P24(x1091) % 47.29/47.37 [110]~P33(x1101)+P34(x1101) % 47.29/47.37 [111]~P41(x1111)+P40(x1111) % 47.29/47.37 [112]~P47(x1121)+P41(x1121) % 47.29/47.37 [113]~P50(x1131)+P49(x1131) % 47.29/47.37 [114]~P57(x1141)+P50(x1141) % 47.29/47.37 [115]~P60(x1151)+P59(x1151) % 47.29/47.37 [116]~P67(x1161)+P60(x1161) % 47.29/47.37 [126]~P71(x1261)+~P70(x1261) % 47.29/47.37 [127]~P42(x1271)+~P36(x1271) % 47.29/47.37 [128]~P51(x1281)+~P36(x1281) % 47.29/47.37 [129]~P6(x1291)+~P3(x1291) % 47.29/47.37 [130]~P66(x1301)+~P67(x1301) % 47.29/47.37 [131]~P9(x1311)+~P4(x1311) % 47.29/47.37 [132]~P1(x1321)+~P8(x1321) % 47.29/47.37 [133]~P13(x1331)+~P8(x1331) % 47.29/47.37 [134]~P51(x1341)+~P1(x1341) % 47.29/47.37 [135]~P61(x1351)+~P1(x1351) % 47.29/47.37 [136]~P30(x1361)+~P13(x1361) % 47.29/47.37 [137]~P42(x1371)+~P13(x1371) % 47.29/47.37 [138]~P11(x1381)+~P10(x1381) % 47.29/47.37 [139]~P12(x1391)+~P15(x1391) % 47.29/47.37 [140]~P32(x1401)+~P23(x1401) % 47.29/47.37 [141]~P30(x1411)+~P24(x1411) % 47.29/47.37 [142]~P61(x1421)+~P24(x1421) % 47.29/47.37 [143]~P32(x1431)+~P30(x1431) % 47.29/47.37 [144]~P33(x1441)+~P31(x1441) % 47.29/47.37 [145]~P41(x1451)+~P38(x1451) % 47.29/47.37 [146]~P44(x1461)+~P39(x1461) % 47.29/47.37 [147]~P44(x1471)+~P42(x1471) % 47.29/47.37 [148]~P47(x1481)+~P45(x1481) % 47.29/47.37 [149]~P50(x1491)+~P46(x1491) % 47.29/47.37 [150]~P53(x1501)+~P48(x1501) % 47.29/47.37 [151]~P53(x1511)+~P51(x1511) % 47.29/47.37 [152]~P57(x1521)+~P55(x1521) % 47.29/47.37 [153]~P60(x1531)+~P56(x1531) % 47.29/47.37 [154]~P63(x1541)+~P58(x1541) % 47.29/47.37 [155]~P63(x1551)+~P61(x1551) % 47.29/47.37 [205]P67(x2051)+~P68(a3,x2051) % 47.29/47.37 [206]P32(x2061)+~P68(a2,x2061) % 47.29/47.37 [207]P32(x2071)+~P68(a41,x2071) % 47.29/47.37 [208]P32(x2081)+~P68(a37,x2081) % 47.29/47.37 [209]P32(x2091)+~P68(a42,x2091) % 47.29/47.37 [210]P32(x2101)+~P68(a44,x2101) % 47.29/47.37 [211]P33(x2111)+~P68(a43,x2111) % 47.29/47.37 [212]P33(x2121)+~P68(a40,x2121) % 47.29/47.37 [213]P33(x2131)+~P68(a46,x2131) % 47.29/47.37 [214]P44(x2141)+~P68(a2,x2141) % 47.29/47.37 [215]P44(x2151)+~P68(a41,x2151) % 47.29/47.37 [216]P44(x2161)+~P68(a37,x2161) % 47.29/47.37 [217]P44(x2171)+~P68(a42,x2171) % 47.29/47.37 [218]P44(x2181)+~P68(a44,x2181) % 47.29/47.37 [219]P47(x2191)+~P68(a45,x2191) % 47.29/47.37 [220]P47(x2201)+~P68(a39,x2201) % 47.29/47.37 [221]P53(x2211)+~P68(a2,x2211) % 47.29/47.37 [222]P53(x2221)+~P68(a41,x2221) % 47.29/47.37 [223]P53(x2231)+~P68(a37,x2231) % 47.29/47.37 [224]P53(x2241)+~P68(a42,x2241) % 47.29/47.37 [225]P53(x2251)+~P68(a44,x2251) % 47.29/47.37 [226]P57(x2261)+~P68(a34,x2261) % 47.29/47.37 [227]P63(x2271)+~P68(a2,x2271) % 47.29/47.37 [228]P63(x2281)+~P68(a41,x2281) % 47.29/47.37 [229]P63(x2291)+~P68(a37,x2291) % 47.29/47.37 [230]P63(x2301)+~P68(a42,x2301) % 47.29/47.37 [231]P63(x2311)+~P68(a44,x2311) % 47.29/47.37 [232]~P43(x2321)+~P68(a43,x2321) % 47.29/47.37 [233]~P43(x2331)+~P68(a40,x2331) % 47.29/47.37 [234]~P43(x2341)+~P68(a46,x2341) % 47.29/47.37 [235]~P52(x2351)+~P68(a43,x2351) % 47.29/47.37 [236]~P52(x2361)+~P68(a40,x2361) % 47.29/47.37 [237]~P52(x2371)+~P68(a46,x2371) % 47.29/47.37 [238]~P54(x2381)+~P68(a45,x2381) % 47.29/47.37 [239]~P54(x2391)+~P68(a39,x2391) % 47.29/47.37 [240]~P62(x2401)+~P68(a43,x2401) % 47.29/47.37 [241]~P62(x2411)+~P68(a40,x2411) % 47.29/47.37 [242]~P62(x2421)+~P68(a46,x2421) % 47.29/47.37 [243]~P64(x2431)+~P68(a45,x2431) % 47.29/47.37 [244]~P64(x2441)+~P68(a39,x2441) % 47.29/47.37 [245]~P65(x2451)+~P68(a34,x2451) % 47.29/47.37 [167]~P18(x1671)+P17(f4(x1671)) % 47.29/47.37 [168]~P19(x1681)+P18(f29(x1681)) % 47.29/47.37 [169]~P20(x1691)+P19(f30(x1691)) % 47.29/47.37 [170]~P16(x1701)+P20(f31(x1701)) % 47.29/47.37 [171]~P27(x1711)+P26(f32(x1711)) % 47.29/47.37 [172]~P28(x1721)+P27(f5(x1721)) % 47.29/47.37 [173]~P29(x1731)+P28(f6(x1731)) % 47.29/47.37 [174]~P25(x1741)+P29(f7(x1741)) % 47.29/47.37 [175]~P45(x1751)+P43(f8(x1751)) % 47.29/47.37 [176]~P54(x1761)+P52(f13(x1761)) % 47.29/47.37 [177]~P55(x1771)+P54(f18(x1771)) % 47.29/47.37 [178]~P64(x1781)+P62(f19(x1781)) % 47.29/47.37 [179]~P65(x1791)+P64(f23(x1791)) % 47.29/47.37 [180]~P66(x1801)+P65(f24(x1801)) % 47.29/47.37 [191]~P3(x1911)+~P67(f14(x1911)) % 47.29/47.37 [192]~P5(x1921)+~P4(f25(x1921)) % 47.29/47.37 [193]~P17(x1931)+~P15(f26(x1931)) % 47.29/47.37 [194]~P26(x1941)+~P21(f33(x1941)) % 47.29/47.37 [195]~P31(x1951)+~P32(f9(x1951)) % 47.29/47.37 [196]~P38(x1961)+~P33(f10(x1961)) % 47.29/47.37 [197]~P40(x1971)+~P36(f11(x1971)) % 47.29/47.37 [198]~P43(x1981)+~P44(f12(x1981)) % 47.29/47.37 [199]~P46(x1991)+~P47(f15(x1991)) % 47.29/47.37 [200]~P49(x2001)+~P1(f16(x2001)) % 47.29/47.37 [201]~P52(x2011)+~P53(f17(x2011)) % 47.29/47.37 [202]~P56(x2021)+~P57(f20(x2021)) % 47.29/47.37 [203]~P59(x2031)+~P22(f21(x2031)) % 47.29/47.37 [204]~P62(x2041)+~P63(f22(x2041)) % 47.29/47.37 [246]~P3(x2461)+P68(x2461,f14(x2461)) % 47.29/47.37 [247]~P5(x2471)+P68(x2471,f25(x2471)) % 47.29/47.37 [248]~P17(x2481)+P68(x2481,f26(x2481)) % 47.29/47.37 [249]~P18(x2491)+P68(x2491,f4(x2491)) % 47.29/47.37 [250]~P19(x2501)+P68(x2501,f29(x2501)) % 47.29/47.37 [251]~P20(x2511)+P68(x2511,f30(x2511)) % 47.29/47.37 [252]~P16(x2521)+P68(x2521,f31(x2521)) % 47.29/47.37 [253]~P26(x2531)+P68(x2531,f33(x2531)) % 47.29/47.37 [254]~P27(x2541)+P68(x2541,f32(x2541)) % 47.29/47.37 [255]~P28(x2551)+P68(x2551,f5(x2551)) % 47.29/47.37 [256]~P29(x2561)+P68(x2561,f6(x2561)) % 47.29/47.37 [257]~P25(x2571)+P68(x2571,f7(x2571)) % 47.29/47.37 [258]~P31(x2581)+P68(x2581,f9(x2581)) % 47.29/47.37 [259]~P38(x2591)+P68(x2591,f10(x2591)) % 47.29/47.37 [260]~P40(x2601)+P68(x2601,f11(x2601)) % 47.29/47.37 [261]~P43(x2611)+P68(x2611,f12(x2611)) % 47.29/47.37 [262]~P45(x2621)+P68(x2621,f8(x2621)) % 47.29/47.37 [263]~P46(x2631)+P68(x2631,f15(x2631)) % 47.29/47.37 [264]~P49(x2641)+P68(x2641,f16(x2641)) % 47.29/47.37 [265]~P52(x2651)+P68(x2651,f17(x2651)) % 47.29/47.37 [266]~P54(x2661)+P68(x2661,f13(x2661)) % 47.29/47.37 [267]~P55(x2671)+P68(x2671,f18(x2671)) % 47.29/47.37 [268]~P56(x2681)+P68(x2681,f20(x2681)) % 47.29/47.37 [269]~P59(x2691)+P68(x2691,f21(x2691)) % 47.29/47.37 [270]~P62(x2701)+P68(x2701,f22(x2701)) % 47.29/47.37 [271]~P64(x2711)+P68(x2711,f19(x2711)) % 47.29/47.37 [272]~P65(x2721)+P68(x2721,f23(x2721)) % 47.29/47.37 [273]~P66(x2731)+P68(x2731,f24(x2731)) % 47.29/47.37 [117]P1(x1171)+P51(x1171)+P36(x1171) % 47.29/47.37 [118]P13(x1181)+P42(x1181)+P36(x1181) % 47.29/47.37 [119]P1(x1191)+P13(x1191)+P8(x1191) % 47.29/47.37 [120]P24(x1201)+P61(x1201)+P1(x1201) % 47.29/47.37 [121]P24(x1211)+P30(x1211)+P13(x1211) % 47.29/47.37 [122]P30(x1221)+P32(x1221)+P23(x1221) % 47.29/47.37 [123]P42(x1231)+P44(x1231)+P39(x1231) % 47.29/47.37 [124]P51(x1241)+P53(x1241)+P48(x1241) % 47.29/47.37 [125]P61(x1251)+P63(x1251)+P58(x1251) % 47.29/47.37 [156]P6(x1561)+~P5(x1561)+P3(x1561) % 47.29/47.37 [157]P66(x1571)+~P60(x1571)+P67(x1571) % 47.29/47.37 [158]P9(x1581)+~P8(x1581)+P4(x1581) % 47.29/47.37 [159]P11(x1591)+~P9(x1591)+P10(x1591) % 47.29/47.37 [160]P12(x1601)+~P10(x1601)+P15(x1601) % 47.29/47.37 [161]P33(x1611)+~P34(x1611)+P31(x1611) % 47.29/47.37 [162]P41(x1621)+~P40(x1621)+P38(x1621) % 47.29/47.37 [163]P47(x1631)+~P41(x1631)+P45(x1631) % 47.29/47.37 [164]P50(x1641)+~P49(x1641)+P46(x1641) % 47.29/47.37 [165]P57(x1651)+~P50(x1651)+P55(x1651) % 47.29/47.37 [166]P60(x1661)+~P59(x1661)+P56(x1661) % 47.29/47.37 [181]~P36(x1811)+~P37(x1811)+P2(x1811) % 47.29/47.37 [182]~P13(x1821)+~P24(x1821)+P37(x1821) % 47.29/47.37 [183]~P6(x1831)+~P25(x1831)+P7(x1831) % 47.29/47.37 [184]~P2(x1841)+~P1(x1841)+P14(x1841) % 47.29/47.37 [185]~P14(x1851)+~P22(x1851)+P21(x1851) % 47.29/47.37 [186]~P13(x1861)+~P24(x1861)+P23(x1861) % 47.29/47.37 [187]~P36(x1871)+~P13(x1871)+P39(x1871) % 47.29/47.37 [188]~P36(x1881)+~P1(x1881)+P48(x1881) % 47.29/47.37 [189]~P1(x1891)+~P24(x1891)+P58(x1891) % 47.29/47.37 [190]~P7(x1901)+~P16(x1901)+P35(x1901) % 47.29/47.37 [274]~P68(x2742,x2741)+P36(x2741)+P40(x2742) % 47.29/47.37 [275]~P68(x2751,x2752)+P3(x2751)+P67(x2752) % 47.29/47.37 [276]~P68(x2761,x2762)+P5(x2761)+P4(x2762) % 47.29/47.37 [277]~P68(x2772,x2771)+P1(x2771)+P49(x2772) % 47.29/47.37 [278]~P68(x2782,x2781)+P15(x2781)+P17(x2782) % 47.29/47.37 [279]~P68(x2792,x2791)+P21(x2791)+P26(x2792) % 47.29/47.37 [280]~P68(x2802,x2801)+P22(x2801)+P59(x2802) % 47.29/47.37 [281]~P68(x2812,x2811)+P32(x2811)+P31(x2812) % 47.29/47.37 [282]~P68(x2822,x2821)+P33(x2821)+P38(x2822) % 47.29/47.37 [283]~P68(x2832,x2831)+P44(x2831)+P43(x2832) % 47.29/47.37 [284]~P68(x2842,x2841)+P47(x2841)+P46(x2842) % 47.29/47.37 [285]~P68(x2852,x2851)+P53(x2851)+P52(x2852) % 47.29/47.37 [286]~P68(x2862,x2861)+P57(x2861)+P56(x2862) % 47.29/47.37 [287]~P68(x2872,x2871)+P63(x2871)+P62(x2872) % 47.29/47.37 [288]~P68(x2881,x2882)+P25(x2881)+~P29(x2882) % 47.29/47.37 [289]~P68(x2891,x2892)+P18(x2891)+~P17(x2892) % 47.29/47.37 [290]~P68(x2901,x2902)+P19(x2901)+~P18(x2902) % 47.29/47.37 [291]~P68(x2911,x2912)+P20(x2911)+~P19(x2912) % 47.29/47.37 [292]~P68(x2921,x2922)+P16(x2921)+~P20(x2922) % 47.29/47.37 [293]~P68(x2931,x2932)+P27(x2931)+~P26(x2932) % 47.29/47.37 [294]~P68(x2941,x2942)+P28(x2941)+~P27(x2942) % 47.29/47.37 [295]~P68(x2951,x2952)+P29(x2951)+~P28(x2952) % 47.29/47.37 [296]~P68(x2961,x2962)+P45(x2961)+~P43(x2962) % 47.29/47.37 [297]~P68(x2971,x2972)+P54(x2971)+~P52(x2972) % 47.29/47.37 [298]~P68(x2981,x2982)+P55(x2981)+~P54(x2982) % 47.29/47.37 [299]~P68(x2991,x2992)+P64(x2991)+~P62(x2992) % 47.29/47.37 [300]~P68(x3001,x3002)+P65(x3001)+~P64(x3002) % 47.29/47.37 [301]~P68(x3011,x3012)+P66(x3011)+~P65(x3012) % 47.29/47.37 [302]~P49(a39)+~P41(a43)+~P41(a40)+~P41(a46)+~P44(a1)+~P47(a43)+~P47(a40)+~P47(a46)+~P49(a45)+~P40(a46)+~P50(a45)+~P50(a39)+~P53(a1)+~P57(a45)+~P57(a39)+~P59(a34)+~P60(a34)+~P63(a1)+~P32(a1)+P70(a28)+~P71(a28)+~P67(a34)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)+P69(a27)+~P33(a2)+~P33(a41)+~P33(a37)+~P33(a42)+~P33(a44)+~P40(a43)+~P40(a40) % 47.29/47.37 [303]~P49(a39)+~P41(a43)+~P41(a40)+~P41(a46)+~P44(a1)+~P47(a43)+~P47(a40)+~P47(a46)+~P49(a45)+~P40(a46)+~P50(a45)+~P50(a39)+~P53(a1)+~P57(a45)+~P57(a39)+~P59(a34)+~P60(a34)+~P63(a1)+~P32(a1)+P71(a28)+~P70(a28)+~P67(a34)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)+P69(a27)+~P33(a2)+~P33(a41)+~P33(a37)+~P33(a42)+~P33(a44)+~P40(a43)+~P40(a40) % 47.29/47.37 %EqnAxiom % 47.29/47.37 % 47.29/47.37 %------------------------------------------- % 47.29/47.39 cnf(304,plain, % 47.29/47.39 (P67(a34)), % 47.29/47.39 inference(scs_inference,[],[9,205])). % 47.29/47.39 cnf(306,plain, % 47.29/47.39 (P32(a38)), % 47.29/47.39 inference(scs_inference,[],[9,14,205,206])). % 47.29/47.39 cnf(308,plain, % 47.29/47.39 (P33(a42)), % 47.29/47.39 inference(scs_inference,[],[9,14,16,205,206,211])). % 47.29/47.39 cnf(310,plain, % 47.29/47.39 (P33(a41)), % 47.29/47.39 inference(scs_inference,[],[9,14,16,17,205,206,211,212])). % 47.29/47.39 cnf(312,plain, % 47.29/47.39 (P33(a44)), % 47.29/47.39 inference(scs_inference,[],[9,14,16,17,18,205,206,211,212,213])). % 47.29/47.39 cnf(314,plain, % 47.29/47.39 (P44(a38)), % 47.29/47.39 inference(scs_inference,[],[9,14,16,17,18,205,206,211,212,213,214])). % 47.29/47.39 cnf(316,plain, % 47.29/47.39 (P47(a46)), % 47.29/47.39 inference(scs_inference,[],[9,13,14,16,17,18,205,206,211,212,213,214,219])). % 47.29/47.39 cnf(318,plain, % 47.29/47.39 (P47(a43)), % 47.29/47.39 inference(scs_inference,[],[9,13,14,15,16,17,18,205,206,211,212,213,214,219,220])). % 47.29/47.39 cnf(320,plain, % 47.29/47.39 (P53(a38)), % 47.29/47.39 inference(scs_inference,[],[9,13,14,15,16,17,18,205,206,211,212,213,214,219,220,221])). % 47.29/47.39 cnf(322,plain, % 47.29/47.39 (P57(a45)), % 47.29/47.39 inference(scs_inference,[],[9,12,13,14,15,16,17,18,205,206,211,212,213,214,219,220,221,226])). % 47.29/47.39 cnf(324,plain, % 47.29/47.39 (P63(a38)), % 47.29/47.39 inference(scs_inference,[],[9,12,13,14,15,16,17,18,205,206,211,212,213,214,219,220,221,226,227])). % 47.29/47.39 cnf(334,plain, % 47.29/47.39 (~P58(a43)), % 47.29/47.39 inference(scs_inference,[],[9,12,13,14,15,16,17,18,20,28,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98])). % 47.29/47.39 cnf(340,plain, % 47.29/47.39 (~P21(a45)), % 47.29/47.39 inference(scs_inference,[],[9,12,13,14,15,16,17,18,20,28,33,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106])). % 47.29/47.39 cnf(342,plain, % 47.29/47.39 (P33(a2)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161])). % 47.29/47.39 cnf(344,plain, % 47.29/47.39 (P40(a40)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274])). % 47.29/47.39 cnf(346,plain, % 47.29/47.39 (P49(a39)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277])). % 47.29/47.39 cnf(348,plain, % 47.29/47.39 (P59(a34)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280])). % 47.29/47.39 cnf(352,plain, % 47.29/47.39 (~P14(a41)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86])). % 47.29/47.39 cnf(354,plain, % 47.29/47.39 (P41(a40)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,44,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162])). % 47.29/47.39 cnf(356,plain, % 47.29/47.39 (P47(a40)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,44,54,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162,163])). % 47.29/47.39 cnf(358,plain, % 47.29/47.39 (P50(a39)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,44,54,57,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162,163,164])). % 47.29/47.39 cnf(360,plain, % 47.29/47.39 (P57(a39)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,44,54,57,69,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162,163,164,165])). % 47.29/47.39 cnf(362,plain, % 47.29/47.39 (P60(a34)), % 47.29/47.39 inference(scs_inference,[],[3,9,12,13,14,15,16,17,18,20,28,33,38,44,54,57,69,70,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162,163,164,165,166])). % 47.29/47.39 cnf(365,plain, % 47.29/47.39 (~P41(a46)+~P44(a1)+~P49(a45)+~P40(a46)+~P50(a45)+~P53(a1)+~P63(a1)+~P32(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)+~P33(a37)+~P40(a43)+~P41(a43)), % 47.29/47.39 inference(scs_inference,[],[84,3,9,12,13,14,15,16,17,18,20,28,33,38,44,54,57,69,70,205,206,211,212,213,214,219,220,221,226,227,88,89,96,97,98,87,105,106,161,274,277,280,279,86,162,163,164,165,166,302])). % 47.29/47.39 cnf(366,plain, % 47.29/47.39 (~P41(a43)+~P41(a46)+~P44(a1)+~P49(a45)+~P40(a46)+~P50(a45)+~P53(a1)+~P63(a1)+~P32(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)+~P33(a37)+~P40(a43)), % 47.29/47.39 inference(scs_inference,[],[346,354,318,356,316,358,322,360,348,362,304,84,342,310,308,312,344,303])). % 47.29/47.39 cnf(367,plain, % 47.29/47.39 (~P21(a41)), % 47.29/47.39 inference(scs_inference,[],[352,105])). % 47.29/47.39 cnf(371,plain, % 47.29/47.39 (P67(a35)), % 47.29/47.39 inference(scs_inference,[],[10,29,352,105,97,205])). % 47.29/47.39 cnf(381,plain, % 47.29/47.39 (~P14(a40)), % 47.29/47.39 inference(scs_inference,[],[10,21,29,34,352,105,97,205,87,86,88,106,96])). % 47.29/47.39 cnf(387,plain, % 47.29/47.39 (P49(a45)), % 47.29/47.39 inference(scs_inference,[],[10,21,29,30,34,13,352,105,97,205,87,86,88,106,96,98,89,277])). % 47.29/47.39 cnf(391,plain, % 47.29/47.39 (P33(a37)), % 47.29/47.39 inference(scs_inference,[],[5,10,21,29,30,34,40,13,12,340,352,105,97,205,87,86,88,106,96,98,89,277,279,161])). % 47.29/47.39 cnf(393,plain, % 47.29/47.39 (P40(a43)), % 47.29/47.39 inference(scs_inference,[],[5,10,21,23,29,30,34,40,13,16,12,340,352,105,97,205,87,86,88,106,96,98,89,277,279,161,274])). % 47.29/47.39 cnf(406,plain, % 47.29/47.39 (~P41(a46)+~P44(a1)+~P40(a46)+~P50(a45)+~P53(a1)+~P63(a1)+~P32(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)+~P41(a43)), % 47.29/47.39 inference(scs_inference,[],[387,391,393,365])). % 47.29/47.39 cnf(413,plain, % 47.29/47.39 (P67(a36)), % 47.29/47.39 inference(scs_inference,[],[11,24,381,30,87,105,97,205])). % 47.29/47.39 cnf(421,plain, % 47.29/47.39 (~P14(a46)), % 47.29/47.39 inference(scs_inference,[],[11,24,381,30,87,105,97,205,89,88,86,96])). % 47.29/47.39 cnf(425,plain, % 47.29/47.39 (P41(a43)), % 47.29/47.39 inference(scs_inference,[],[393,11,24,381,30,43,87,105,97,205,89,88,86,96,98,162])). % 47.29/47.39 cnf(427,plain, % 47.29/47.39 (P50(a45)), % 47.29/47.39 inference(scs_inference,[],[387,393,11,24,381,30,43,56,87,105,97,205,89,88,86,96,98,162,164])). % 47.29/47.39 cnf(431,plain, % 47.29/47.39 (P40(a46)), % 47.29/47.39 inference(scs_inference,[],[387,393,18,17,11,24,381,30,43,56,367,87,105,97,205,89,88,86,96,98,162,164,279,274])). % 47.29/47.39 cnf(440,plain, % 47.29/47.39 (~P41(a46)+~P44(a1)+~P53(a1)+~P63(a1)+~P32(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[425,387,431,427,391,393,366])). % 47.29/47.39 cnf(451,plain, % 47.29/47.39 (P41(a46)), % 47.29/47.39 inference(scs_inference,[],[431,45,421,23,87,105,89,88,86,162])). % 47.29/47.39 cnf(461,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+~P32(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[451,431,427,425,406])). % 47.29/47.39 cnf(472,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+~P32(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P25(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[451,440])). % 47.29/47.39 cnf(766,plain, % 47.29/47.39 (~P6(x7661)+~P4(f25(x7661))), % 47.29/47.39 inference(scs_inference,[],[91,192])). % 47.29/47.39 cnf(1008,plain, % 47.29/47.39 (P25(a3)), % 47.29/47.39 inference(scs_inference,[],[8,93,94])). % 47.29/47.39 cnf(1009,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+~P32(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[1008,461])). % 47.29/47.39 cnf(1010,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+~P32(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[1008,472])). % 47.29/47.39 cnf(2026,plain, % 47.29/47.39 (P32(a1)), % 47.29/47.39 inference(scs_inference,[],[36,37,108,122])). % 47.29/47.39 cnf(2027,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[2026,1009])). % 47.29/47.39 cnf(2028,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+~P63(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[2026,1010])). % 47.29/47.39 cnf(2159,plain, % 47.29/47.39 (P63(a1)), % 47.29/47.39 inference(scs_inference,[],[36,72,109,125])). % 47.29/47.39 cnf(2160,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+P70(a28)+~P71(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[2159,2027])). % 47.29/47.39 cnf(2161,plain, % 47.29/47.39 (~P44(a1)+~P53(a1)+P71(a28)+~P70(a28)+~P5(a3)+~P6(a3)+~P7(a3)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[2159,2028])). % 47.29/47.39 cnf(2442,plain, % 47.29/47.39 (~P36(f11(a40))), % 47.29/47.39 inference(scs_inference,[],[354,111,197])). % 47.29/47.39 cnf(2445,plain, % 47.29/47.39 (~P39(f11(a40))), % 47.29/47.39 inference(scs_inference,[],[2442,87,88])). % 47.29/47.39 cnf(24781,plain, % 47.29/47.39 (~P8(f25(x247811))+~P6(x247811)+P9(f25(x247811))), % 47.29/47.39 inference(scs_inference,[],[766,158])). % 47.29/47.39 cnf(31727,plain, % 47.29/47.39 (P68(a40,f11(a40))), % 47.29/47.39 inference(scs_inference,[],[354,260,111])). % 47.29/47.39 cnf(31734,plain, % 47.29/47.39 (P33(f11(a40))), % 47.29/47.39 inference(scs_inference,[],[31727,233,236,241,212])). % 47.29/47.39 cnf(33851,plain, % 47.29/47.39 (P53(a1)), % 47.29/47.39 inference(scs_inference,[],[371,31734,306,324,314,320,59,2445,58,1,132,116,110,140,144,146,147,150,151,154,123,124])). % 47.29/47.39 cnf(33853,plain, % 47.29/47.39 (P5(a3)), % 47.29/47.39 inference(scs_inference,[],[371,31734,306,324,314,320,59,9,2445,27,58,1,132,116,110,140,144,146,147,150,151,154,123,124,276])). % 47.29/47.39 cnf(33859,plain, % 47.29/47.39 (P6(a3)), % 47.29/47.39 inference(scs_inference,[],[371,31734,306,324,314,320,26,59,9,2445,27,58,334,1,132,116,110,140,144,146,147,150,151,154,123,124,276,115,125,156])). % 47.29/47.39 cnf(33867,plain, % 47.29/47.39 (P7(a3)), % 47.29/47.39 inference(scs_inference,[],[1008,371,31734,306,324,314,320,26,59,9,2445,27,58,334,1,132,116,110,140,144,146,147,150,151,154,123,124,276,115,125,156,281,24781,158,183])). % 47.29/47.39 cnf(33871,plain, % 47.29/47.39 (~P44(a1)+P70(a28)+~P71(a28)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[33851,33853,33859,33867,2160])). % 47.29/47.39 cnf(33872,plain, % 47.29/47.39 (~P44(a1)+P71(a28)+~P70(a28)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[33851,33853,33859,33867,2161])). % 47.29/47.39 cnf(33875,plain, % 47.29/47.39 (P44(a1)), % 47.29/47.39 inference(scs_inference,[],[413,47,46,116,123])). % 47.29/47.39 cnf(33896,plain, % 47.29/47.39 (P70(a28)+~P71(a28)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[33875,33871])). % 47.29/47.39 cnf(33897,plain, % 47.29/47.39 (P71(a28)+~P70(a28)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[33875,33872])). % 47.29/47.39 cnf(54926,plain, % 47.29/47.39 (~P71(a28)+~P16(a3)), % 47.29/47.39 inference(scs_inference,[],[33896,126])). % 47.29/47.40 cnf(55077,plain, % 47.29/47.40 (P70(a28)+~P16(a3)), % 47.29/47.40 inference(scs_inference,[],[54926,85])). % 47.29/47.40 cnf(55228,plain, % 47.29/47.40 (P71(a28)+~P16(a3)), % 47.29/47.40 inference(scs_inference,[],[55077,33897])). % 47.29/47.40 cnf(55379,plain, % 47.29/47.40 (~P70(a28)+~P16(a3)), % 47.29/47.40 inference(scs_inference,[],[55228,126])). % 47.29/47.40 cnf(55530,plain, % 47.29/47.40 (~P16(a3)), % 47.29/47.40 inference(scs_inference,[],[55379,55077])). % 47.29/47.40 cnf(55531,plain, % 47.29/47.40 ($false), % 47.29/47.40 inference(scs_inference,[],[55530,8,104]), % 47.29/47.40 ['proof']). % 47.52/47.43 % SZS output end Proof % 47.52/47.43 % Total time :46.700000s %------------------------------------------------------------------------------