%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS155+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 : n028.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 59.06s 59.04s % Output : CNFRefutation 59.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.11 % Problem : KRS155+1 : TPTP v8.2.0. Released v3.1.0. % 0.02/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n028.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:53:08 EDT 2024 % 0.11/0.32 % CPUTime : % 0.53/0.56 start to proof:theBenchmark % 58.95/59.00 %------------------------------------------- % 58.95/59.00 % File :CSE---1.7 % 58.95/59.00 % Problem :theBenchmark % 58.95/59.00 % Transform :cnf % 58.95/59.00 % Format :tptp:raw % 58.95/59.00 % Command :java -jar mcs_scs.jar %d %s % 58.95/59.01 % 58.95/59.01 % Result :Theorem 58.380000s % 58.95/59.01 % Output :CNFRefutation 58.380000s % 58.95/59.01 %------------------------------------------- % 58.98/59.01 %------------------------------------------------------------------------------ % 58.98/59.01 % File : KRS155+1 : TPTP v8.2.0. Released v3.1.0. % 58.98/59.01 % Domain : Knowledge Representation (Semantic Web) % 58.98/59.01 % Problem : DL Test: k_d4 ABox test from DL98 systems comparison % 58.98/59.02 % Version : Especial. % 58.98/59.02 % English : % 58.98/59.02 % 58.98/59.02 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 58.98/59.02 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 58.98/59.02 % Source : [Bec03] % 58.98/59.02 % Names : positive_description-logic-Manifest662 [Bec03] % 58.98/59.02 % 58.98/59.02 % Status : Theorem % 58.98/59.02 % Rating : 0.00 v8.2.0, 0.07 v8.1.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.12 v6.0.0, 0.25 v5.4.0, 0.22 v5.3.0, 0.35 v5.2.0, 0.21 v5.0.0, 0.25 v4.1.0, 0.22 v4.0.1, 0.16 v4.0.0, 0.15 v3.7.0, 0.67 v3.5.0, 0.25 v3.3.0, 0.00 v3.2.0, 0.11 v3.1.0 % 58.98/59.02 % Syntax : Number of formulae : 135 ( 34 unt; 0 def) % 58.98/59.02 % Number of atoms : 300 ( 0 equ) % 58.98/59.02 % Maximal formula atoms : 19 ( 2 avg) % 58.98/59.02 % Number of connectives : 193 ( 28 ~; 0 |; 65 &) % 58.98/59.02 % ( 97 <=>; 3 =>; 0 <=; 0 <~>) % 58.98/59.02 % Maximal formula depth : 17 ( 4 avg) % 58.98/59.02 % Maximal term depth : 1 ( 1 avg) % 58.98/59.02 % Number of predicates : 102 ( 102 usr; 0 prp; 1-2 aty) % 58.98/59.02 % Number of functors : 10 ( 10 usr; 10 con; 0-0 aty) % 58.98/59.02 % Number of variables : 181 ( 102 !; 79 ?) % 58.98/59.02 % SPC : FOF_THM_RFO_NEQ % 58.98/59.02 % 58.98/59.02 % Comments : Sean Bechhofer says there are some errors in the encoding of % 58.98/59.02 % datatypes, so this problem may not be perfect. At least it's % 58.98/59.02 % still representative of the type of reasoning required for OWL. % 58.98/59.02 %------------------------------------------------------------------------------ % 58.98/59.02 %----Thing and Nothing % 58.98/59.02 fof(axiom_0,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cowlThing(X) % 58.98/59.02 & ~ cowlNothing(X) ) ). % 58.98/59.02 % 58.98/59.02 %----String and Integer disjoint % 58.98/59.02 fof(axiom_1,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( xsd_string(X) % 58.98/59.02 <=> ~ xsd_integer(X) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC10 % 58.98/59.02 fof(axiom_2,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC10(X) % 58.98/59.02 <=> ( cC4(X) % 58.98/59.02 & cC8(X) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC12 % 58.98/59.02 fof(axiom_3,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC12(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC10(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC14 % 58.98/59.02 fof(axiom_4,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC14(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px1(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC14 % 58.98/59.02 fof(axiom_5,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC14(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cTOP(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC14xcomp % 58.98/59.02 fof(axiom_6,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC14xcomp(X) % 58.98/59.02 <=> ? [Y0] : ra_Px1(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC16 % 58.98/59.02 fof(axiom_7,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC16(X) % 58.98/59.02 <=> ? [Y0] : ra_Px2(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC16 % 58.98/59.02 fof(axiom_8,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC16(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC14xcomp(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC16xcomp % 58.98/59.02 fof(axiom_9,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC16xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px2(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC18 % 58.98/59.02 fof(axiom_10,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC18(X) % 58.98/59.02 <=> ( cC16xcomp(X) % 58.98/59.02 & cC12(X) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC2 % 58.98/59.02 fof(axiom_11,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC2(X) % 58.98/59.02 <=> ? [Y0] : ra_Px3(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC2xcomp % 58.98/59.02 fof(axiom_12,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC2xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px3(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC20 % 58.98/59.02 fof(axiom_13,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC20(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC2xcomp(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC20 % 58.98/59.02 fof(axiom_14,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC20(X) % 58.98/59.02 <=> ? [Y0] : ra_Px5(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC20xcomp % 58.98/59.02 fof(axiom_15,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC20xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px5(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC22 % 58.98/59.02 fof(axiom_16,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC22(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC2xcomp(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC24 % 58.98/59.02 fof(axiom_17,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC24(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC22(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC26 % 58.98/59.02 fof(axiom_18,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC26(X) % 58.98/59.02 <=> ( cC24(X) % 58.98/59.02 & cC20xcomp(X) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC26 % 58.98/59.02 fof(axiom_19,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC26(X) % 58.98/59.02 <=> ? [Y0] : ra_Px30(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC26xcomp % 58.98/59.02 fof(axiom_20,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC26xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px30(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC28 % 58.98/59.02 fof(axiom_21,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC28(X) % 58.98/59.02 <=> ? [Y0] : ra_Px6(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC28 % 58.98/59.02 fof(axiom_22,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC28(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC26(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC28xcomp % 58.98/59.02 fof(axiom_23,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC28xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px6(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC30 % 58.98/59.02 fof(axiom_24,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC30(X) % 58.98/59.02 <=> ( cC18(X) % 58.98/59.02 & cC28xcomp(X) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC32 % 58.98/59.02 fof(axiom_25,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC32(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC2(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC32 % 58.98/59.02 fof(axiom_26,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC32(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px7(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC32xcomp % 58.98/59.02 fof(axiom_27,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC32xcomp(X) % 58.98/59.02 <=> ? [Y0] : ra_Px7(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC34 % 58.98/59.02 fof(axiom_28,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC34(X) % 58.98/59.02 <=> ? [Y0] : ra_Px9(X,Y0) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC34 % 58.98/59.02 fof(axiom_29,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC34(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC32xcomp(Y) ) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC34xcomp % 58.98/59.02 fof(axiom_30,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC34xcomp(X) % 58.98/59.02 <=> ~ ? [Y] : ra_Px9(X,Y) ) ). % 58.98/59.02 % 58.98/59.02 %----Equality cC36 % 58.98/59.02 fof(axiom_31,axiom, % 58.98/59.02 ! [X] : % 58.98/59.02 ( cC36(X) % 58.98/59.02 <=> ? [Y] : % 58.98/59.02 ( rR1(X,Y) % 58.98/59.02 & cC2(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC36 % 58.98/59.03 fof(axiom_32,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC36(X) % 58.98/59.03 <=> ? [Y0] : ra_Px8(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC36xcomp % 58.98/59.03 fof(axiom_33,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC36xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px8(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC38 % 58.98/59.03 fof(axiom_34,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC38(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC36xcomp(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC4 % 58.98/59.03 fof(axiom_35,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC4(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2xcomp(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC40 % 58.98/59.03 fof(axiom_36,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC40(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC38(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC42 % 58.98/59.03 fof(axiom_37,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC42(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px31(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC42 % 58.98/59.03 fof(axiom_38,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC42(X) % 58.98/59.03 <=> ( cC40(X) % 58.98/59.03 & cC34xcomp(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC42xcomp % 58.98/59.03 fof(axiom_39,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC42xcomp(X) % 58.98/59.03 <=> ? [Y0] : ra_Px31(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC44 % 58.98/59.03 fof(axiom_40,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC44(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px10(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC44 % 58.98/59.03 fof(axiom_41,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC44(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC42(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC44xcomp % 58.98/59.03 fof(axiom_42,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC44xcomp(X) % 58.98/59.03 <=> ? [Y0] : ra_Px10(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC46 % 58.98/59.03 fof(axiom_43,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC46(X) % 58.98/59.03 <=> ( cC44xcomp(X) % 58.98/59.03 & cC30(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC48 % 58.98/59.03 fof(axiom_44,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC48(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2xcomp(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC48 % 58.98/59.03 fof(axiom_45,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC48(X) % 58.98/59.03 <=> ? [Y0] : ra_Px12(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC48xcomp % 58.98/59.03 fof(axiom_46,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC48xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px12(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC50 % 58.98/59.03 fof(axiom_47,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC50(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px13(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC50 % 58.98/59.03 fof(axiom_48,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC50(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC50xcomp % 58.98/59.03 fof(axiom_49,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC50xcomp(X) % 58.98/59.03 <=> ? [Y0] : ra_Px13(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC52 % 58.98/59.03 fof(axiom_50,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC52(X) % 58.98/59.03 <=> ? [Y0] : ra_Px32(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC52 % 58.98/59.03 fof(axiom_51,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC52(X) % 58.98/59.03 <=> ( cC50xcomp(X) % 58.98/59.03 & cC48xcomp(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC52xcomp % 58.98/59.03 fof(axiom_52,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC52xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px32(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC54 % 58.98/59.03 fof(axiom_53,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC54(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC52(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC54 % 58.98/59.03 fof(axiom_54,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC54(X) % 58.98/59.03 <=> ? [Y0] : ra_Px14(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC54xcomp % 58.98/59.03 fof(axiom_55,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC54xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px14(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC56 % 58.98/59.03 fof(axiom_56,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC56(X) % 58.98/59.03 <=> ( cC54xcomp(X) % 58.98/59.03 & cC46(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC58 % 58.98/59.03 fof(axiom_57,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC58(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC6 % 58.98/59.03 fof(axiom_58,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC6(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px28(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC6 % 58.98/59.03 fof(axiom_59,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC6(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2xcomp(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC6xcomp % 58.98/59.03 fof(axiom_60,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC6xcomp(X) % 58.98/59.03 <=> ? [Y0] : ra_Px28(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC60 % 58.98/59.03 fof(axiom_61,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC60(X) % 58.98/59.03 <=> ( cC2xcomp(X) % 58.98/59.03 & cC58(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC62 % 58.98/59.03 fof(axiom_62,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC62(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC60(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC62 % 58.98/59.03 fof(axiom_63,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC62(X) % 58.98/59.03 <=> ? [Y0] : ra_Px17(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC62xcomp % 58.98/59.03 fof(axiom_64,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC62xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px17(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC64 % 58.98/59.03 fof(axiom_65,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC64(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC2(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC66 % 58.98/59.03 fof(axiom_66,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC66(X) % 58.98/59.03 <=> ( cC2xcomp(X) % 58.98/59.03 & cC64(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC68 % 58.98/59.03 fof(axiom_67,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC68(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC66(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC70 % 58.98/59.03 fof(axiom_68,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC70(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC68(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC72 % 58.98/59.03 fof(axiom_69,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC72(X) % 58.98/59.03 <=> ( cC62xcomp(X) % 58.98/59.03 & cC70(X) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC72 % 58.98/59.03 fof(axiom_70,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC72(X) % 58.98/59.03 <=> ? [Y0] : ra_Px33(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC72xcomp % 58.98/59.03 fof(axiom_71,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC72xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px33(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC74 % 58.98/59.03 fof(axiom_72,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC74(X) % 58.98/59.03 <=> ? [Y] : % 58.98/59.03 ( rR1(X,Y) % 58.98/59.03 & cC72(Y) ) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC74 % 58.98/59.03 fof(axiom_73,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC74(X) % 58.98/59.03 <=> ? [Y0] : ra_Px18(X,Y0) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC74xcomp % 58.98/59.03 fof(axiom_74,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC74xcomp(X) % 58.98/59.03 <=> ~ ? [Y] : ra_Px18(X,Y) ) ). % 58.98/59.03 % 58.98/59.03 %----Equality cC76 % 58.98/59.03 fof(axiom_75,axiom, % 58.98/59.03 ! [X] : % 58.98/59.03 ( cC76(X) % 58.98/59.03 <=> ( cC74xcomp(X) % 58.98/59.03 & cC56(X) ) ) ). % 59.06/59.03 % 59.06/59.03 %----Equality cC78 % 59.06/59.03 fof(axiom_76,axiom, % 59.06/59.03 ! [X] : % 59.06/59.03 ( cC78(X) % 59.06/59.03 <=> ? [Y] : % 59.06/59.03 ( rR1(X,Y) % 59.06/59.03 & cC2xcomp(Y) ) ) ). % 59.06/59.03 % 59.06/59.03 %----Equality cC78 % 59.06/59.03 fof(axiom_77,axiom, % 59.06/59.03 ! [X] : % 59.06/59.03 ( cC78(X) % 59.06/59.03 <=> ? [Y0] : ra_Px20(X,Y0) ) ). % 59.06/59.03 % 59.06/59.03 %----Equality cC78xcomp % 59.06/59.03 fof(axiom_78,axiom, % 59.06/59.03 ! [X] : % 59.06/59.03 ( cC78xcomp(X) % 59.06/59.03 <=> ~ ? [Y] : ra_Px20(X,Y) ) ). % 59.06/59.03 % 59.06/59.03 %----Equality cC8 % 59.06/59.03 fof(axiom_79,axiom, % 59.06/59.03 ! [X] : % 59.06/59.03 ( cC8(X) % 59.06/59.03 <=> ? [Y] : % 59.06/59.03 ( rR1(X,Y) % 59.06/59.03 & cC6xcomp(Y) ) ) ). % 59.06/59.03 % 59.06/59.03 %----Equality cC80 % 59.06/59.03 fof(axiom_80,axiom, % 59.06/59.03 ! [X] : % 59.06/59.03 ( cC80(X) % 59.06/59.03 <=> ( cC78xcomp(X) % 59.06/59.03 & cC2xcomp(X) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC82 % 59.06/59.04 fof(axiom_81,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC82(X) % 59.06/59.04 <=> ~ ? [Y] : ra_Px25(X,Y) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC82 % 59.06/59.04 fof(axiom_82,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC82(X) % 59.06/59.04 <=> ? [Y] : % 59.06/59.04 ( rR1(X,Y) % 59.06/59.04 & cC80(Y) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC82xcomp % 59.06/59.04 fof(axiom_83,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC82xcomp(X) % 59.06/59.04 <=> ? [Y0] : ra_Px25(X,Y0) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC84 % 59.06/59.04 fof(axiom_84,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC84(X) % 59.06/59.04 <=> ? [Y] : % 59.06/59.04 ( rR1(X,Y) % 59.06/59.04 & cC2xcomp(Y) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC84 % 59.06/59.04 fof(axiom_85,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC84(X) % 59.06/59.04 <=> ? [Y0] : ra_Px23(X,Y0) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC84xcomp % 59.06/59.04 fof(axiom_86,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC84xcomp(X) % 59.06/59.04 <=> ~ ? [Y] : ra_Px23(X,Y) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC86 % 59.06/59.04 fof(axiom_87,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC86(X) % 59.06/59.04 <=> ( cC84xcomp(X) % 59.06/59.04 & cC2xcomp(X) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC88 % 59.06/59.04 fof(axiom_88,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC88(X) % 59.06/59.04 <=> ? [Y] : % 59.06/59.04 ( rR1(X,Y) % 59.06/59.04 & cC86(Y) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC90 % 59.06/59.04 fof(axiom_89,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC90(X) % 59.06/59.04 <=> ? [Y] : % 59.06/59.04 ( rR1(X,Y) % 59.06/59.04 & cC88(Y) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC92 % 59.06/59.04 fof(axiom_90,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC92(X) % 59.06/59.04 <=> ( cC82xcomp(X) % 59.06/59.04 & cC90(X) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC92 % 59.06/59.04 fof(axiom_91,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC92(X) % 59.06/59.04 <=> ~ ? [Y] : ra_Px34(X,Y) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC92xcomp % 59.06/59.04 fof(axiom_92,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC92xcomp(X) % 59.06/59.04 <=> ? [Y0] : ra_Px34(X,Y0) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC94 % 59.06/59.04 fof(axiom_93,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC94(X) % 59.06/59.04 <=> ? [Y0] : ra_Px29(X,Y0) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC94 % 59.06/59.04 fof(axiom_94,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC94(X) % 59.06/59.04 <=> ? [Y] : % 59.06/59.04 ( rR1(X,Y) % 59.06/59.04 & cC92(Y) ) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cC94xcomp % 59.06/59.04 fof(axiom_95,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cC94xcomp(X) % 59.06/59.04 <=> ~ ? [Y] : ra_Px29(X,Y) ) ). % 59.06/59.04 % 59.06/59.04 %----Equality cTEST % 59.06/59.04 fof(axiom_96,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( cTEST(X) % 59.06/59.04 <=> ( cC76(X) % 59.06/59.04 & cC94xcomp(X) ) ) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_97,axiom, % 59.06/59.04 cC52xcomp(iV8467) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_98,axiom, % 59.06/59.04 cC72xcomp(iV8467) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_99,axiom, % 59.06/59.04 cC92xcomp(iV8467) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_100,axiom, % 59.06/59.04 cC42xcomp(iV8467) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_101,axiom, % 59.06/59.04 cC26xcomp(iV8467) ). % 59.06/59.04 % 59.06/59.04 %----iV8467 % 59.06/59.04 fof(axiom_102,axiom, % 59.06/59.04 cowlThing(iV8467) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_103,axiom, % 59.06/59.04 rR1(iV8467,iV8471) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_104,axiom, % 59.06/59.04 rR1(iV8467,iV8470) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_105,axiom, % 59.06/59.04 rR1(iV8467,iV8469) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_106,axiom, % 59.06/59.04 rR1(iV8467,iV8474) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_107,axiom, % 59.06/59.04 rR1(iV8467,iV8468) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_108,axiom, % 59.06/59.04 rR1(iV8467,iV8473) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_109,axiom, % 59.06/59.04 rR1(iV8467,iV8475) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_110,axiom, % 59.06/59.04 rR1(iV8467,iV8472) ). % 59.06/59.04 % 59.06/59.04 %----iV8468 % 59.06/59.04 fof(axiom_111,axiom, % 59.06/59.04 cC2xcomp(iV8468) ). % 59.06/59.04 % 59.06/59.04 %----iV8468 % 59.06/59.04 fof(axiom_112,axiom, % 59.06/59.04 cowlThing(iV8468) ). % 59.06/59.04 % 59.06/59.04 %----iV8469 % 59.06/59.04 fof(axiom_113,axiom, % 59.06/59.04 cC6xcomp(iV8469) ). % 59.06/59.04 % 59.06/59.04 %----iV8469 % 59.06/59.04 fof(axiom_114,axiom, % 59.06/59.04 cowlThing(iV8469) ). % 59.06/59.04 % 59.06/59.04 %----iV8469 % 59.06/59.04 fof(axiom_115,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( rR1(iV8469,X) % 59.06/59.04 => cC2(X) ) ). % 59.06/59.04 % 59.06/59.04 %----iV8470 % 59.06/59.04 fof(axiom_116,axiom, % 59.06/59.04 cTOP(iV8470) ). % 59.06/59.04 % 59.06/59.04 %----iV8470 % 59.06/59.04 fof(axiom_117,axiom, % 59.06/59.04 cowlThing(iV8470) ). % 59.06/59.04 % 59.06/59.04 %----iV8471 % 59.06/59.04 fof(axiom_118,axiom, % 59.06/59.04 cC78xcomp(iV8471) ). % 59.06/59.04 % 59.06/59.04 %----iV8471 % 59.06/59.04 fof(axiom_119,axiom, % 59.06/59.04 cC2xcomp(iV8471) ). % 59.06/59.04 % 59.06/59.04 %----iV8471 % 59.06/59.04 fof(axiom_120,axiom, % 59.06/59.04 cowlThing(iV8471) ). % 59.06/59.04 % 59.06/59.04 %----iV8471 % 59.06/59.04 fof(axiom_121,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( rR1(iV8471,X) % 59.06/59.04 => cC2(X) ) ). % 59.06/59.04 % 59.06/59.04 %----iV8472 % 59.06/59.04 fof(axiom_122,axiom, % 59.06/59.04 cC2xcomp(iV8472) ). % 59.06/59.04 % 59.06/59.04 %----iV8472 % 59.06/59.04 fof(axiom_123,axiom, % 59.06/59.04 cowlThing(iV8472) ). % 59.06/59.04 % 59.06/59.04 fof(axiom_124,axiom, % 59.06/59.04 rR1(iV8472,iV8476) ). % 59.06/59.04 % 59.06/59.04 %----iV8473 % 59.06/59.04 fof(axiom_125,axiom, % 59.06/59.04 cC2xcomp(iV8473) ). % 59.06/59.04 % 59.06/59.04 %----iV8473 % 59.06/59.04 fof(axiom_126,axiom, % 59.06/59.04 cowlThing(iV8473) ). % 59.06/59.04 % 59.06/59.04 %----iV8474 % 59.06/59.04 fof(axiom_127,axiom, % 59.06/59.04 cC32xcomp(iV8474) ). % 59.06/59.04 % 59.06/59.04 %----iV8474 % 59.06/59.04 fof(axiom_128,axiom, % 59.06/59.04 cowlThing(iV8474) ). % 59.06/59.04 % 59.06/59.04 %----iV8474 % 59.06/59.04 fof(axiom_129,axiom, % 59.06/59.04 ! [X] : % 59.06/59.04 ( rR1(iV8474,X) % 59.06/59.04 => cC2xcomp(X) ) ). % 59.06/59.04 % 59.06/59.04 %----iV8475 % 59.06/59.04 fof(axiom_130,axiom, % 59.06/59.04 cC2xcomp(iV8475) ). % 59.06/59.04 % 59.06/59.04 %----iV8475 % 59.06/59.04 fof(axiom_131,axiom, % 59.06/59.04 cowlThing(iV8475) ). % 59.06/59.04 % 59.06/59.04 %----iV8476 % 59.06/59.04 fof(axiom_132,axiom, % 59.06/59.04 cC2(iV8476) ). % 59.06/59.04 % 59.06/59.04 %----iV8476 % 59.06/59.04 fof(axiom_133,axiom, % 59.06/59.04 cowlThing(iV8476) ). % 59.06/59.04 % 59.06/59.04 %----Thing and Nothing % 59.06/59.04 %----String and Integer disjoint % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8467 % 59.06/59.04 %----iV8471 % 59.06/59.04 %----iV8471 % 59.06/59.04 %----iV8472 % 59.06/59.04 %----iV8472 % 59.06/59.04 %----iV8472 % 59.06/59.04 fof(the_axiom,conjecture, % 59.06/59.04 ( ! [X] : % 59.06/59.04 ( cowlThing(X) % 59.06/59.04 & ~ cowlNothing(X) ) % 59.06/59.04 & ! [X] : % 59.06/59.04 ( xsd_string(X) % 59.06/59.04 <=> ~ xsd_integer(X) ) % 59.06/59.04 & cC20(iV8467) % 59.06/59.04 & cC4(iV8467) % 59.06/59.04 & cC8(iV8467) % 59.06/59.04 & cC82(iV8467) % 59.06/59.04 & cC62(iV8467) % 59.06/59.04 & cC14(iV8467) % 59.06/59.04 & cC34(iV8467) % 59.06/59.04 & cC10(iV8467) % 59.06/59.04 & cowlThing(iV8467) % 59.06/59.04 & cC48(iV8467) % 59.06/59.04 & cowlThing(iV8471) % 59.06/59.04 & cC80(iV8471) % 59.06/59.04 & cC58(iV8472) % 59.06/59.04 & cC60(iV8472) % 59.06/59.04 & cowlThing(iV8472) ) ). % 59.06/59.04 % 59.06/59.04 %------------------------------------------------------------------------------ % 59.06/59.04 %------------------------------------------- % 59.06/59.04 % Proof found % 59.06/59.04 % SZS status Theorem for theBenchmark % 59.06/59.04 % SZS output start Proof % 59.06/59.04 %ClaNum:269(EqnAxiom:0) % 59.06/59.04 %VarNum:690(SingletonVarNum:322) % 59.06/59.04 %MaxLitNum:15 % 59.06/59.04 %MaxfuncDepth:1 % 59.06/59.04 %SharedTerms:53 % 59.06/59.04 %goalClause: 268 269 % 59.06/59.04 [1]P1(a1) % 59.06/59.04 [2]P2(a86) % 59.06/59.04 [3]P10(a87) % 59.06/59.04 [4]P10(a2) % 59.06/59.04 [5]P10(a88) % 59.06/59.04 [6]P10(a90) % 59.06/59.04 [7]P10(a89) % 59.06/59.04 [8]P11(a3) % 59.06/59.04 [9]P19(a91) % 59.06/59.04 [10]P22(a3) % 59.06/59.04 [11]P31(a3) % 59.06/59.04 [12]P40(a85) % 59.06/59.04 [13]P52(a3) % 59.06/59.04 [14]P55(a87) % 59.06/59.04 [15]P60(a3) % 59.06/59.04 [16]P74(a3,a87) % 59.06/59.04 [17]P74(a3,a1) % 59.06/59.04 [18]P74(a3,a85) % 59.06/59.04 [19]P74(a3,a91) % 59.06/59.04 [20]P74(a3,a2) % 59.06/59.04 [21]P74(a3,a88) % 59.06/59.04 [22]P74(a3,a90) % 59.06/59.04 [23]P74(a3,a89) % 59.06/59.04 [24]P74(a89,a86) % 59.06/59.04 [25]~P75(x251) % 59.06/59.04 [26]P77(x261)+P76(x261) % 59.06/59.04 [27]~P3(x271)+P23(x271) % 59.06/59.04 [28]~P3(x281)+P61(x281) % 59.06/59.04 [29]~P5(x291)+P4(x291) % 59.06/59.04 [30]~P5(x301)+P6(x301) % 59.06/59.04 [31]~P20(x311)+P5(x311) % 59.06/59.04 [32]~P41(x321)+P10(x321) % 59.06/59.04 [33]~P47(x331)+P10(x331) % 59.06/59.04 [34]~P62(x341)+P10(x341) % 59.06/59.04 [35]~P63(x351)+P10(x351) % 59.06/59.04 [36]~P14(x361)+P12(x361) % 59.06/59.04 [37]~P14(x371)+P15(x371) % 59.06/59.04 [38]~P20(x381)+P17(x381) % 59.06/59.04 [39]~P32(x391)+P20(x391) % 59.06/59.04 [40]~P29(x401)+P24(x401) % 59.06/59.04 [41]~P29(x411)+P30(x411) % 59.06/59.04 [42]~P32(x421)+P33(x421) % 59.06/59.04 [43]~P42(x431)+P32(x431) % 59.06/59.04 [44]~P37(x441)+P35(x441) % 59.06/59.04 [45]~P37(x451)+P38(x451) % 59.06/59.04 [46]~P42(x461)+P43(x461) % 59.06/59.04 [47]~P56(x471)+P42(x471) % 59.06/59.04 [48]~P41(x481)+P45(x481) % 59.06/59.04 [49]~P53(x491)+P48(x491) % 59.06/59.04 [50]~P47(x501)+P50(x501) % 59.06/59.04 [51]~P53(x511)+P54(x511) % 59.06/59.04 [52]~P56(x521)+P57(x521) % 59.06/59.04 [53]~P71(x531)+P56(x531) % 59.06/59.04 [54]~P62(x541)+P55(x541) % 59.06/59.04 [55]~P68(x551)+P64(x551) % 59.06/59.04 [56]~P63(x561)+P66(x561) % 59.06/59.04 [57]~P68(x571)+P69(x571) % 59.06/59.04 [58]~P71(x581)+P72(x581) % 59.06/59.04 [59]~P77(x591)+~P76(x591) % 59.06/59.04 [107]P2(x1071)+~P74(a87,x1071) % 59.06/59.04 [108]P2(x1081)+~P74(a85,x1081) % 59.06/59.04 [109]P10(x1091)+~P74(a91,x1091) % 59.06/59.04 [60]~P4(x601)+P3(f4(x601)) % 59.06/59.04 [61]~P7(x611)+P1(f15(x611)) % 59.06/59.04 [62]~P9(x621)+P8(f37(x621)) % 59.06/59.04 [63]~P21(x631)+P2(f16(x631)) % 59.06/59.04 [64]~P26(x641)+P2(f17(x641)) % 59.06/59.04 [65]~P39(x651)+P2(f38(x651)) % 59.06/59.04 [66]~P45(x661)+P2(f40(x661)) % 59.06/59.04 [67]~P50(x671)+P2(f47(x671)) % 59.06/59.04 [68]~P13(x681)+P10(f5(x681)) % 59.06/59.04 [69]~P16(x691)+P10(f6(x691)) % 59.06/59.04 [70]~P23(x701)+P10(f23(x701)) % 59.06/59.04 [71]~P36(x711)+P10(f28(x711)) % 59.06/59.04 [72]~P46(x721)+P10(f48(x721)) % 59.06/59.04 [73]~P59(x731)+P10(f55(x731)) % 59.06/59.04 [74]~P67(x741)+P10(f70(x741)) % 59.06/59.04 [75]~P15(x751)+P16(f9(x751)) % 59.06/59.04 [76]~P18(x761)+P14(f10(x761)) % 59.06/59.04 [77]~P25(x771)+P19(f18(x771)) % 59.06/59.04 [78]~P28(x781)+P27(f24(x781)) % 59.06/59.04 [79]~P30(x791)+P28(f29(x791)) % 59.06/59.04 [80]~P34(x801)+P29(f30(x801)) % 59.06/59.04 [81]~P44(x811)+P37(f41(x811)) % 59.06/59.04 [82]~P61(x821)+P40(f64(x821)) % 59.06/59.04 [83]~P49(x831)+P41(f51(x831)) % 59.06/59.04 [84]~P51(x841)+P47(f56(x841)) % 59.06/59.04 [85]~P54(x851)+P51(f57(x851)) % 59.06/59.04 [86]~P58(x861)+P53(f58(x861)) % 59.06/59.04 [87]~P65(x871)+P62(f67(x871)) % 59.06/59.04 [88]~P70(x881)+P63(f71(x881)) % 59.06/59.04 [89]~P69(x891)+P70(f74(x891)) % 59.06/59.04 [90]~P73(x901)+P68(f75(x901)) % 59.06/59.04 [110]P7(x1101)+P78(x1101,f27(x1101)) % 59.06/59.04 [111]P6(x1111)+P79(x1111,f79(x1111)) % 59.06/59.04 [112]P10(x1121)+P86(x1121,f81(x1121)) % 59.06/59.04 [113]P12(x1131)+P92(x1131,f7(x1131)) % 59.06/59.04 [114]P11(x1141)+P93(x1141,f11(x1141)) % 59.06/59.04 [115]P17(x1151)+P98(x1151,f14(x1151)) % 59.06/59.04 [116]P21(x1161)+P99(x1161,f19(x1161)) % 59.06/59.04 [117]P24(x1171)+P100(x1171,f22(x1171)) % 59.06/59.04 [118]P27(x1181)+P101(x1181,f25(x1181)) % 59.06/59.04 [119]P29(x1191)+P94(x1191,f31(x1191)) % 59.06/59.04 [120]P34(x1201)+P80(x1201,f32(x1201)) % 59.06/59.04 [121]P35(x1211)+P81(x1211,f35(x1211)) % 59.06/59.04 [122]P39(x1221)+P82(x1221,f39(x1221)) % 59.06/59.04 [123]P31(x1231)+P95(x1231,f42(x1231)) % 59.06/59.04 [124]P43(x1241)+P83(x1241,f45(x1241)) % 59.06/59.04 [125]P46(x1251)+P87(x1251,f49(x1251)) % 59.06/59.04 [126]P48(x1261)+P84(x1261,f53(x1261)) % 59.06/59.04 [127]P52(x1271)+P96(x1271,f59(x1271)) % 59.06/59.04 [128]P57(x1281)+P85(x1281,f62(x1281)) % 59.06/59.04 [129]P55(x1291)+P88(x1291,f65(x1291)) % 59.06/59.04 [130]P65(x1301)+P89(x1301,f68(x1301)) % 59.06/59.04 [131]P66(x1311)+P90(x1311,f72(x1311)) % 59.06/59.04 [132]P68(x1321)+P97(x1321,f76(x1321)) % 59.06/59.04 [133]P72(x1331)+P91(x1331,f80(x1331)) % 59.06/59.04 [158]~P4(x1581)+P74(x1581,f4(x1581)) % 59.06/59.04 [159]~P7(x1591)+P74(x1591,f15(x1591)) % 59.06/59.04 [160]~P9(x1601)+P74(x1601,f37(x1601)) % 59.06/59.04 [161]~P13(x1611)+P74(x1611,f5(x1611)) % 59.06/59.04 [162]~P16(x1621)+P74(x1621,f6(x1621)) % 59.06/59.04 [163]~P15(x1631)+P74(x1631,f9(x1631)) % 59.06/59.04 [164]~P18(x1641)+P74(x1641,f10(x1641)) % 59.06/59.04 [165]~P21(x1651)+P74(x1651,f16(x1651)) % 59.06/59.04 [166]~P25(x1661)+P74(x1661,f18(x1661)) % 59.06/59.04 [167]~P26(x1671)+P74(x1671,f17(x1671)) % 59.06/59.04 [168]~P28(x1681)+P74(x1681,f24(x1681)) % 59.06/59.04 [169]~P23(x1691)+P74(x1691,f23(x1691)) % 59.06/59.04 [170]~P30(x1701)+P74(x1701,f29(x1701)) % 59.06/59.04 [171]~P34(x1711)+P74(x1711,f30(x1711)) % 59.06/59.04 [172]~P36(x1721)+P74(x1721,f28(x1721)) % 59.06/59.04 [173]~P39(x1731)+P74(x1731,f38(x1731)) % 59.06/59.04 [174]~P44(x1741)+P74(x1741,f41(x1741)) % 59.06/59.04 [175]~P45(x1751)+P74(x1751,f40(x1751)) % 59.06/59.04 [176]~P46(x1761)+P74(x1761,f48(x1761)) % 59.06/59.04 [177]~P49(x1771)+P74(x1771,f51(x1771)) % 59.06/59.04 [178]~P50(x1781)+P74(x1781,f47(x1781)) % 59.06/59.04 [179]~P51(x1791)+P74(x1791,f56(x1791)) % 59.06/59.04 [180]~P54(x1801)+P74(x1801,f57(x1801)) % 59.06/59.04 [181]~P58(x1811)+P74(x1811,f58(x1811)) % 59.06/59.04 [182]~P59(x1821)+P74(x1821,f55(x1821)) % 59.06/59.04 [183]~P61(x1831)+P74(x1831,f64(x1831)) % 59.06/59.04 [184]~P65(x1841)+P74(x1841,f67(x1841)) % 59.06/59.04 [185]~P67(x1851)+P74(x1851,f70(x1851)) % 59.06/59.04 [186]~P70(x1861)+P74(x1861,f71(x1861)) % 59.06/59.04 [187]~P69(x1871)+P74(x1871,f74(x1871)) % 59.06/59.04 [188]~P73(x1881)+P74(x1881,f75(x1881)) % 59.06/59.04 [189]~P8(x1891)+P78(x1891,f50(x1891)) % 59.06/59.04 [190]~P9(x1901)+P79(x1901,f61(x1901)) % 59.06/59.04 [191]~P2(x1911)+P86(x1911,f82(x1911)) % 59.06/59.04 [192]~P13(x1921)+P92(x1921,f8(x1921)) % 59.06/59.04 [193]~P14(x1931)+P93(x1931,f12(x1931)) % 59.06/59.04 [194]~P18(x1941)+P98(x1941,f13(x1941)) % 59.06/59.04 [195]~P19(x1951)+P99(x1951,f20(x1951)) % 59.06/59.04 [196]~P25(x1961)+P100(x1961,f21(x1961)) % 59.06/59.04 [197]~P26(x1971)+P101(x1971,f26(x1971)) % 59.06/59.04 [198]~P22(x1981)+P94(x1981,f33(x1981)) % 59.06/59.04 [199]~P33(x1991)+P80(x1991,f34(x1991)) % 59.06/59.04 [200]~P36(x2001)+P81(x2001,f36(x2001)) % 59.06/59.04 [201]~P38(x2011)+P82(x2011,f43(x2011)) % 59.06/59.04 [202]~P37(x2021)+P95(x2021,f44(x2021)) % 59.06/59.04 [203]~P44(x2031)+P83(x2031,f46(x2031)) % 59.06/59.04 [204]~P40(x2041)+P87(x2041,f52(x2041)) % 59.06/59.04 [205]~P49(x2051)+P84(x2051,f54(x2051)) % 59.06/59.04 [206]~P53(x2061)+P96(x2061,f60(x2061)) % 59.06/59.04 [207]~P58(x2071)+P85(x2071,f63(x2071)) % 59.06/59.04 [208]~P59(x2081)+P88(x2081,f66(x2081)) % 59.06/59.04 [209]~P64(x2091)+P89(x2091,f69(x2091)) % 59.06/59.04 [210]~P67(x2101)+P90(x2101,f73(x2101)) % 59.06/59.04 [211]~P60(x2111)+P97(x2111,f77(x2111)) % 59.06/59.04 [212]~P73(x2121)+P91(x2121,f78(x2121)) % 59.06/59.04 [134]P8(x1341)+~P78(x1341,x1342) % 59.06/59.04 [135]P9(x1351)+~P79(x1351,x1352) % 59.06/59.04 [136]P2(x1361)+~P86(x1361,x1362) % 59.06/59.04 [137]P13(x1371)+~P92(x1371,x1372) % 59.06/59.04 [138]P14(x1381)+~P93(x1381,x1382) % 59.06/59.04 [139]P18(x1391)+~P98(x1391,x1392) % 59.06/59.04 [140]P19(x1401)+~P99(x1401,x1402) % 59.06/59.04 [141]P25(x1411)+~P100(x1411,x1412) % 59.06/59.04 [142]P26(x1421)+~P101(x1421,x1422) % 59.06/59.04 [143]P22(x1431)+~P94(x1431,x1432) % 59.06/59.04 [144]P33(x1441)+~P80(x1441,x1442) % 59.06/59.04 [145]P36(x1451)+~P81(x1451,x1452) % 59.06/59.04 [146]P38(x1461)+~P82(x1461,x1462) % 59.06/59.04 [147]P37(x1471)+~P95(x1471,x1472) % 59.06/59.04 [148]P44(x1481)+~P83(x1481,x1482) % 59.06/59.04 [149]P40(x1491)+~P87(x1491,x1492) % 59.06/59.04 [150]P49(x1501)+~P84(x1501,x1502) % 59.06/59.04 [151]P53(x1511)+~P96(x1511,x1512) % 59.06/59.04 [152]P58(x1521)+~P85(x1521,x1522) % 59.06/59.04 [153]P59(x1531)+~P88(x1531,x1532) % 59.06/59.04 [154]P64(x1541)+~P89(x1541,x1542) % 59.06/59.04 [155]P67(x1551)+~P90(x1551,x1552) % 59.06/59.04 [156]P60(x1561)+~P97(x1561,x1562) % 59.06/59.04 [157]P73(x1571)+~P91(x1571,x1572) % 59.06/59.04 [213]~P7(x2131)+~P78(x2131,x2132) % 59.06/59.04 [214]~P6(x2141)+~P79(x2141,x2142) % 59.06/59.04 [215]~P10(x2151)+~P86(x2151,x2152) % 59.06/59.04 [216]~P12(x2161)+~P92(x2161,x2162) % 59.06/59.04 [217]~P11(x2171)+~P93(x2171,x2172) % 59.06/59.04 [218]~P17(x2181)+~P98(x2181,x2182) % 59.06/59.04 [219]~P21(x2191)+~P99(x2191,x2192) % 59.06/59.04 [220]~P24(x2201)+~P100(x2201,x2202) % 59.06/59.04 [221]~P27(x2211)+~P101(x2211,x2212) % 59.06/59.04 [222]~P29(x2221)+~P94(x2221,x2222) % 59.06/59.04 [223]~P34(x2231)+~P80(x2231,x2232) % 59.06/59.04 [224]~P35(x2241)+~P81(x2241,x2242) % 59.06/59.04 [225]~P39(x2251)+~P82(x2251,x2252) % 59.06/59.04 [226]~P31(x2261)+~P95(x2261,x2262) % 59.06/59.04 [227]~P43(x2271)+~P83(x2271,x2272) % 59.06/59.04 [228]~P46(x2281)+~P87(x2281,x2282) % 59.06/59.04 [229]~P48(x2291)+~P84(x2291,x2292) % 59.06/59.04 [230]~P52(x2301)+~P96(x2301,x2302) % 59.06/59.04 [231]~P57(x2311)+~P85(x2311,x2312) % 59.06/59.04 [232]~P55(x2321)+~P88(x2321,x2322) % 59.06/59.04 [233]~P65(x2331)+~P89(x2331,x2332) % 59.06/59.04 [234]~P66(x2341)+~P90(x2341,x2342) % 59.06/59.04 [235]~P68(x2351)+~P97(x2351,x2352) % 59.06/59.04 [236]~P72(x2361)+~P91(x2361,x2362) % 59.06/59.04 [91]~P23(x911)+~P61(x911)+P3(x911) % 59.06/59.04 [92]~P4(x921)+~P6(x921)+P5(x921) % 59.06/59.04 [93]~P12(x931)+~P15(x931)+P14(x931) % 59.06/59.04 [94]~P5(x941)+~P17(x941)+P20(x941) % 59.06/59.04 [95]~P24(x951)+~P30(x951)+P29(x951) % 59.06/59.04 [96]~P20(x961)+~P33(x961)+P32(x961) % 59.06/59.04 [97]~P35(x971)+~P38(x971)+P37(x971) % 59.06/59.04 [98]~P32(x981)+~P43(x981)+P42(x981) % 59.06/59.04 [99]~P10(x991)+~P45(x991)+P41(x991) % 59.06/59.04 [100]~P10(x1001)+~P50(x1001)+P47(x1001) % 59.06/59.04 [101]~P48(x1011)+~P54(x1011)+P53(x1011) % 59.06/59.04 [102]~P42(x1021)+~P57(x1021)+P56(x1021) % 59.06/59.04 [103]~P10(x1031)+~P55(x1031)+P62(x1031) % 59.06/59.04 [104]~P10(x1041)+~P66(x1041)+P63(x1041) % 59.06/59.04 [105]~P64(x1051)+~P69(x1051)+P68(x1051) % 59.06/59.04 [106]~P56(x1061)+~P72(x1061)+P71(x1061) % 59.06/59.04 [237]~P74(x2371,x2372)+P23(x2371)+~P10(x2372) % 59.06/59.04 [238]~P74(x2381,x2382)+P61(x2381)+~P40(x2382) % 59.06/59.04 [239]~P74(x2391,x2392)+P4(x2391)+~P3(x2392) % 59.06/59.04 [240]~P74(x2401,x2402)+P7(x2401)+~P1(x2402) % 59.06/59.04 [241]~P74(x2411,x2412)+P9(x2411)+~P8(x2412) % 59.06/59.04 [242]~P74(x2421,x2422)+P13(x2421)+~P10(x2422) % 59.06/59.04 [243]~P74(x2431,x2432)+P16(x2431)+~P10(x2432) % 59.06/59.04 [244]~P74(x2441,x2442)+P15(x2441)+~P16(x2442) % 59.06/59.04 [245]~P74(x2451,x2452)+P18(x2451)+~P14(x2452) % 59.06/59.04 [246]~P74(x2461,x2462)+P21(x2461)+~P2(x2462) % 59.06/59.04 [247]~P74(x2471,x2472)+P25(x2471)+~P19(x2472) % 59.06/59.04 [248]~P74(x2481,x2482)+P26(x2481)+~P2(x2482) % 59.06/59.04 [249]~P74(x2491,x2492)+P28(x2491)+~P27(x2492) % 59.06/59.04 [250]~P74(x2501,x2502)+P30(x2501)+~P28(x2502) % 59.06/59.04 [251]~P74(x2511,x2512)+P34(x2511)+~P29(x2512) % 59.06/59.04 [252]~P74(x2521,x2522)+P36(x2521)+~P10(x2522) % 59.06/59.04 [253]~P74(x2531,x2532)+P39(x2531)+~P2(x2532) % 59.06/59.04 [254]~P74(x2541,x2542)+P44(x2541)+~P37(x2542) % 59.06/59.04 [255]~P74(x2551,x2552)+P45(x2551)+~P2(x2552) % 59.06/59.04 [256]~P74(x2561,x2562)+P46(x2561)+~P10(x2562) % 59.06/59.04 [257]~P74(x2571,x2572)+P49(x2571)+~P41(x2572) % 59.06/59.04 [258]~P74(x2581,x2582)+P50(x2581)+~P2(x2582) % 59.06/59.04 [259]~P74(x2591,x2592)+P51(x2591)+~P47(x2592) % 59.06/59.04 [260]~P74(x2601,x2602)+P54(x2601)+~P51(x2602) % 59.06/59.04 [261]~P74(x2611,x2612)+P58(x2611)+~P53(x2612) % 59.06/59.04 [262]~P74(x2621,x2622)+P59(x2621)+~P10(x2622) % 59.06/59.04 [263]~P74(x2631,x2632)+P65(x2631)+~P62(x2632) % 59.06/59.04 [264]~P74(x2641,x2642)+P67(x2641)+~P10(x2642) % 59.06/59.04 [265]~P74(x2651,x2652)+P70(x2651)+~P63(x2652) % 59.06/59.04 [266]~P74(x2661,x2662)+P69(x2661)+~P70(x2662) % 59.06/59.04 [267]~P74(x2671,x2672)+P73(x2671)+~P68(x2672) % 59.06/59.04 [268]P75(a83)+P76(a84)+~P77(a84)+~P3(a3)+~P23(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P62(a87)+~P65(a3) % 59.06/59.04 [269]P75(a83)+P77(a84)+~P76(a84)+~P3(a3)+~P23(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P62(a87)+~P65(a3) % 59.06/59.04 %EqnAxiom % 59.06/59.04 % 59.06/59.04 %------------------------------------------- % 59.06/59.05 cnf(274,plain, % 59.06/59.05 (~P59(a87)), % 59.06/59.05 inference(scs_inference,[],[3,14,215,232,208])). % 59.06/59.05 cnf(282,plain, % 59.06/59.05 (P62(a87)), % 59.06/59.05 inference(scs_inference,[],[3,14,8,11,13,215,232,208,217,226,230,103])). % 59.06/59.05 cnf(295,plain, % 59.06/59.05 (~P77(a84)+~P3(a3)+~P23(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P65(a3)+P76(a84)), % 59.06/59.05 inference(scs_inference,[],[25,3,14,8,11,13,215,232,208,217,226,230,103,262,191,193,202,206,268])). % 59.06/59.05 cnf(296,plain, % 59.06/59.05 (P77(a84)+~P76(a84)+~P3(a3)+~P23(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P65(a3)), % 59.06/59.05 inference(scs_inference,[],[25,282,269])). % 59.06/59.05 cnf(403,plain, % 59.06/59.05 (~P3(x4031)+P40(f64(x4031))), % 59.06/59.05 inference(scs_inference,[],[28,82])). % 59.06/59.05 cnf(589,plain, % 59.06/59.05 (P23(a3)), % 59.06/59.05 inference(scs_inference,[],[282,16,34,237])). % 59.06/59.05 cnf(590,plain, % 59.06/59.05 (~P77(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P65(a3)+P76(a84)), % 59.06/59.05 inference(scs_inference,[],[589,295])). % 59.06/59.05 cnf(591,plain, % 59.06/59.05 (P77(a84)+~P76(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+~P65(a3)), % 59.06/59.05 inference(scs_inference,[],[589,296])). % 59.06/59.05 cnf(1268,plain, % 59.06/59.05 (~P63(x12681)+~P90(x12681,x12682)), % 59.06/59.05 inference(scs_inference,[],[56,234])). % 59.06/59.05 cnf(1484,plain, % 59.06/59.05 (~P101(x14841,x14842)+P2(f17(x14841))), % 59.06/59.05 inference(scs_inference,[],[64,142])). % 59.06/59.05 cnf(1546,plain, % 59.06/59.05 (P10(f5(a3))), % 59.06/59.05 inference(scs_inference,[],[6,22,68,242])). % 59.06/59.05 cnf(1581,plain, % 59.06/59.05 (P10(f6(a3))), % 59.06/59.05 inference(scs_inference,[],[6,22,69,243])). % 59.06/59.05 cnf(1616,plain, % 59.06/59.05 (P10(f28(a3))), % 59.06/59.05 inference(scs_inference,[],[6,22,71,252])). % 59.06/59.05 cnf(1651,plain, % 59.06/59.05 (P10(f48(a3))), % 59.06/59.05 inference(scs_inference,[],[6,22,72,256])). % 59.06/59.05 cnf(1686,plain, % 59.06/59.05 (P10(f55(a3))), % 59.06/59.05 inference(scs_inference,[],[6,22,73,262])). % 59.06/59.05 cnf(2004,plain, % 59.06/59.05 (P62(f67(a3))), % 59.06/59.05 inference(scs_inference,[],[282,16,87,263])). % 59.06/59.05 cnf(2159,plain, % 59.06/59.05 (~P86(x21591,x21592)+~P74(a91,x21591)), % 59.06/59.05 inference(scs_inference,[],[109,215])). % 59.06/59.05 cnf(2252,plain, % 59.06/59.05 (~P92(x22521,x22522)+P74(x22521,f5(x22521))), % 59.06/59.05 inference(scs_inference,[],[137,161])). % 59.06/59.05 cnf(2748,plain, % 59.06/59.05 (~P99(x27481,x27482)+P99(x27481,f19(x27481))), % 59.06/59.05 inference(scs_inference,[],[219,116])). % 59.06/59.05 cnf(2779,plain, % 59.06/59.05 (~P101(x27791,x27792)+P101(x27791,f25(x27791))), % 59.06/59.05 inference(scs_inference,[],[221,118])). % 59.06/59.05 cnf(2903,plain, % 59.06/59.05 (~P87(x29031,x29032)+P87(x29031,f49(x29031))), % 59.06/59.05 inference(scs_inference,[],[228,125])). % 59.06/59.05 cnf(2934,plain, % 59.06/59.05 (~P89(a3,x29341)), % 59.06/59.05 inference(scs_inference,[],[282,16,233,263])). % 59.06/59.05 cnf(2935,plain, % 59.06/59.05 (P65(a3)), % 59.06/59.05 inference(scs_inference,[],[2934,130])). % 59.06/59.05 cnf(2946,plain, % 59.06/59.05 (~P77(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+P76(a84)), % 59.06/59.05 inference(scs_inference,[],[2935,590])). % 59.06/59.05 cnf(2947,plain, % 59.06/59.05 (P77(a84)+~P76(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P13(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)), % 59.06/59.05 inference(scs_inference,[],[2935,591])). % 59.06/59.05 cnf(3034,plain, % 59.06/59.05 (~P3(x30341)+P87(f64(x30341),f52(f64(x30341)))), % 59.06/59.05 inference(scs_inference,[],[403,204])). % 59.06/59.05 cnf(4273,plain, % 59.06/59.05 (~P92(x42731,x42732)+P92(x42731,f7(x42731))), % 59.06/59.05 inference(scs_inference,[],[113,216])). % 59.06/59.05 cnf(4955,plain, % 59.06/59.05 (~P90(x49551,x49552)+P90(x49551,f72(x49551))), % 59.06/59.05 inference(scs_inference,[],[131,234])). % 59.06/59.05 cnf(5234,plain, % 59.06/59.05 (P74(a3,f23(a3))), % 59.06/59.05 inference(scs_inference,[],[7,23,169,237])). % 59.06/59.05 cnf(5637,plain, % 59.06/59.05 (P74(a3,f67(a3))), % 59.06/59.05 inference(scs_inference,[],[2934,184,130])). % 59.06/59.05 cnf(5916,plain, % 59.06/59.05 (~P90(x59161,x59162)+P90(x59161,f73(x59161))), % 59.06/59.05 inference(scs_inference,[],[210,155])). % 59.06/59.05 cnf(7233,plain, % 59.06/59.05 (P13(a3)), % 59.06/59.05 inference(scs_inference,[],[23,7,242])). % 59.06/59.05 cnf(7237,plain, % 59.06/59.05 (P23(x72371)+~P74(x72371,f5(a3))), % 59.06/59.05 inference(scs_inference,[],[23,7,1546,274,242,262,237])). % 59.06/59.05 cnf(7239,plain, % 59.06/59.05 (P26(a89)), % 59.06/59.05 inference(scs_inference,[],[2,24,23,7,1546,274,242,262,237,248])). % 59.06/59.05 cnf(7241,plain, % 59.06/59.05 (~P77(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+P76(a84)), % 59.06/59.05 inference(scs_inference,[],[7233,2946])). % 59.06/59.05 cnf(7242,plain, % 59.06/59.05 (P77(a84)+~P76(a84)+~P3(a3)+~P61(a3)+~P7(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)), % 59.06/59.05 inference(scs_inference,[],[7233,2947])). % 59.06/59.05 cnf(7245,plain, % 59.06/59.05 (P13(x72451)+~P74(x72451,f6(a3))), % 59.06/59.05 inference(scs_inference,[],[1581,274,262,242])). % 59.06/59.05 cnf(7267,plain, % 59.06/59.05 (P13(x72671)+~P74(x72671,f48(a3))), % 59.06/59.05 inference(scs_inference,[],[4,1651,274,262,242])). % 59.06/59.05 cnf(7658,plain, % 59.06/59.05 (~P74(x76581,f5(a3))+P10(f23(x76581))), % 59.06/59.05 inference(scs_inference,[],[7237,70])). % 59.06/59.05 cnf(7689,plain, % 59.06/59.05 (~P74(x76891,f6(a3))+P10(f5(x76891))), % 59.06/59.05 inference(scs_inference,[],[7245,68])). % 59.06/59.05 cnf(7813,plain, % 59.06/59.05 (~P74(x78131,f48(a3))+P10(f5(x78131))), % 59.06/59.05 inference(scs_inference,[],[7267,68])). % 59.06/59.05 cnf(9083,plain, % 59.06/59.05 (P101(a89,f25(a89))), % 59.06/59.05 inference(scs_inference,[],[7239,2779,197])). % 59.06/59.05 cnf(9329,plain, % 59.06/59.05 (P87(a85,f49(a85))), % 59.06/59.05 inference(scs_inference,[],[12,2903,204])). % 59.06/59.05 cnf(9515,plain, % 59.06/59.05 (P92(a3,f7(a3))), % 59.06/59.05 inference(scs_inference,[],[7233,4273,192])). % 59.06/59.05 cnf(9516,plain, % 59.06/59.05 (P74(a3,f5(a3))), % 59.06/59.05 inference(scs_inference,[],[9515,2252])). % 59.06/59.05 cnf(9518,plain, % 59.06/59.05 (P10(f23(a3))), % 59.06/59.05 inference(scs_inference,[],[9515,2252,7658])). % 59.06/59.05 cnf(9522,plain, % 59.06/59.05 (~P2(f23(a3))), % 59.06/59.05 inference(scs_inference,[],[9515,2252,7658,215,191])). % 59.06/59.05 cnf(9740,plain, % 59.06/59.05 (P90(x97401,f72(x97401))+~P67(x97401)), % 59.06/59.05 inference(scs_inference,[],[4955,210])). % 59.06/59.05 cnf(9771,plain, % 59.06/59.05 (P90(a3,f72(a3))), % 59.06/59.05 inference(scs_inference,[],[1546,9516,9740,264])). % 59.06/59.05 cnf(11206,plain, % 59.06/59.05 (P67(a3)), % 59.06/59.05 inference(scs_inference,[],[9771,5916,155])). % 59.06/59.05 cnf(11609,plain, % 59.06/59.05 (~P86(f5(x116091),x116092)+~P74(x116091,f6(a3))), % 59.06/59.05 inference(scs_inference,[],[7689,215])). % 59.06/59.05 cnf(11671,plain, % 59.06/59.05 (~P86(f5(x116711),x116712)+~P74(x116711,f48(a3))), % 59.06/59.05 inference(scs_inference,[],[7813,215])). % 59.06/59.05 cnf(12599,plain, % 59.06/59.05 (~P3(x125991)+~P46(f64(x125991))), % 59.06/59.05 inference(scs_inference,[],[3034,228])). % 59.06/59.05 cnf(14225,plain, % 59.06/59.05 (P16(a3)), % 59.06/59.05 inference(scs_inference,[],[1686,1546,5637,9516,9515,9329,274,9083,216,262,228,221,238,243])). % 59.06/59.05 cnf(14227,plain, % 59.06/59.05 (P46(a3)), % 59.06/59.05 inference(scs_inference,[],[1686,1546,5637,9516,9515,9329,274,9083,216,262,228,221,238,243,256])). % 59.06/59.05 cnf(14232,plain, % 59.06/59.05 (P61(a3)), % 59.06/59.05 inference(scs_inference,[],[18,12,238])). % 59.06/59.05 cnf(14234,plain, % 59.06/59.05 (P3(a3)), % 59.06/59.05 inference(scs_inference,[],[589,18,12,238,91])). % 59.06/59.05 cnf(14249,plain, % 59.06/59.05 (~P77(a84)+~P7(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)+P76(a84)), % 59.06/59.05 inference(scs_inference,[],[14234,14232,7241])). % 59.06/59.05 cnf(14250,plain, % 59.06/59.05 (P77(a84)+~P76(a84)+~P7(a3)+~P25(a3)+~P36(a3)+~P45(a89)+~P41(a89)+~P49(a3)), % 59.06/59.05 inference(scs_inference,[],[14234,14232,7242])). % 59.06/59.05 cnf(15426,plain, % 59.06/59.05 (P26(x154261)+~P74(x154261,f17(a89))), % 59.06/59.05 inference(scs_inference,[],[1616,274,9083,262,1484,248])). % 59.06/59.05 cnf(15434,plain, % 59.06/59.05 (~P74(x154341,f17(a89))+P2(f17(x154341))), % 59.06/59.05 inference(scs_inference,[],[15426,64])). % 59.06/59.05 cnf(15465,plain, % 59.06/59.05 (~P74(x154651,f17(a89))+P86(f17(x154651),f82(f17(x154651)))), % 59.06/59.05 inference(scs_inference,[],[15434,191])). % 59.06/59.05 cnf(15682,plain, % 59.06/59.05 (~P2(f5(x156821))+~P74(x156821,f6(a3))), % 59.06/59.05 inference(scs_inference,[],[11609,191])). % 59.06/59.05 cnf(15713,plain, % 59.06/59.05 (~P74(x157131,f6(a3))+~P74(a87,f5(x157131))), % 59.06/59.05 inference(scs_inference,[],[15682,107])). % 59.06/59.05 cnf(15744,plain, % 59.06/59.05 (~P2(f5(x157441))+~P74(x157441,f48(a3))), % 59.06/59.05 inference(scs_inference,[],[11671,191])). % 59.06/59.05 cnf(15775,plain, % 59.06/59.05 (~P74(x157751,f48(a3))+~P74(a85,f5(x157751))), % 59.06/59.05 inference(scs_inference,[],[15744,108])). % 59.06/59.05 cnf(17817,plain, % 59.06/59.05 (~P74(x178171,f17(a89))+~P74(a91,f17(x178171))), % 59.06/59.05 inference(scs_inference,[],[15465,2159])). % 59.06/59.05 cnf(25044,plain, % 59.06/59.05 (P7(a3)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,12,7239,17,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240])). % 59.06/59.05 cnf(25046,plain, % 59.06/59.05 (P25(a3)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,12,7239,19,17,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240,247])). % 59.06/59.05 cnf(25048,plain, % 59.06/59.05 (P36(a3)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,5234,12,7239,19,17,9518,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240,247,252])). % 59.06/59.05 cnf(25054,plain, % 59.06/59.05 (P45(a89)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,5234,12,7239,19,17,24,9518,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240,247,252,253,258,255])). % 59.06/59.05 cnf(25056,plain, % 59.06/59.05 (P41(a89)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,5234,12,7239,19,17,24,9518,7,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240,247,252,253,258,255,99])). % 59.06/59.05 cnf(25058,plain, % 59.06/59.05 (P49(a3)), % 59.06/59.05 inference(scs_inference,[],[1,2004,9522,9,10,14227,14234,9771,11206,7233,14225,2,5234,12,7239,19,17,23,24,9518,7,54,234,1268,107,108,12599,162,167,176,185,192,195,197,198,204,210,2748,15713,15775,17817,34,228,191,240,247,252,253,258,255,99,257])). % 59.06/59.05 cnf(25153,plain, % 59.06/59.05 (P76(a84)+~P77(a84)), % 59.06/59.05 inference(scs_inference,[],[25046,25048,25054,25056,25058,25044,14249])). % 59.06/59.05 cnf(25154,plain, % 59.06/59.05 (~P76(a84)+P77(a84)), % 59.06/59.05 inference(scs_inference,[],[25044,25046,25048,25054,25056,25058,14250])). % 59.06/59.05 cnf(25607,plain, % 59.06/59.05 (~P77(a84)), % 59.06/59.05 inference(scs_inference,[],[25153,59])). % 59.06/59.05 cnf(25608,plain, % 59.06/59.05 (~P76(a84)), % 59.06/59.05 inference(scs_inference,[],[25607,25154])). % 59.06/59.05 cnf(25609,plain, % 59.06/59.05 (P76(a84)), % 59.06/59.05 inference(scs_inference,[],[25607,26])). % 59.06/59.05 cnf(25639,plain, % 59.06/59.05 ($false), % 59.06/59.05 inference(scs_inference,[],[25608,25609]), % 59.06/59.05 ['proof']). % 59.06/59.10 % SZS output end Proof % 59.06/59.10 % Total time :58.380000s %------------------------------------------------------------------------------