%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS151+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 : n019.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:41 EDT 2024 % Result : Theorem 45.67s 45.63s % Output : CNFRefutation 45.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS151+1 : TPTP v8.2.0. Released v3.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 13:49:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 45.55/45.59 %------------------------------------------- % 45.55/45.59 % File :CSE---1.7 % 45.55/45.59 % Problem :theBenchmark % 45.55/45.59 % Transform :cnf % 45.55/45.59 % Format :tptp:raw % 45.55/45.59 % Command :java -jar mcs_scs.jar %d %s % 45.55/45.59 % 45.55/45.59 % Result :Theorem 44.960000s % 45.55/45.59 % Output :CNFRefutation 44.960000s % 45.55/45.59 %------------------------------------------- % 45.55/45.60 %------------------------------------------------------------------------------ % 45.55/45.60 % File : KRS151+1 : TPTP v8.2.0. Released v3.1.0. % 45.55/45.60 % Domain : Knowledge Representation (Semantic Web) % 45.55/45.60 % Problem : DL Test: k_path ABox test from DL98 systems comparison % 45.55/45.60 % Version : Especial. % 45.55/45.60 % English : % 45.55/45.60 % 45.55/45.60 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 45.55/45.60 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 45.55/45.60 % Source : [Bec03] % 45.55/45.60 % Names : positive_description-logic-Manifest206 [Bec03] % 45.55/45.60 % 45.55/45.60 % Status : Theorem % 45.55/45.60 % Rating : 0.00 v8.1.0, 0.07 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.21 v5.4.0, 0.26 v5.3.0, 0.35 v5.2.0, 0.14 v5.0.0, 0.15 v4.1.0, 0.11 v4.0.1, 0.05 v4.0.0, 0.10 v3.7.0, 0.33 v3.5.0, 0.25 v3.3.0, 0.22 v3.2.0, 0.33 v3.1.0 % 45.55/45.60 % Syntax : Number of formulae : 243 ( 127 unt; 0 def) % 45.55/45.60 % Number of atoms : 490 ( 0 equ) % 45.55/45.60 % Maximal formula atoms : 54 ( 2 avg) % 45.55/45.60 % Number of connectives : 399 ( 152 ~; 0 |; 132 &) % 45.55/45.60 % ( 87 <=>; 28 =>; 0 <=; 0 <~>) % 45.55/45.60 % Maximal formula depth : 52 ( 3 avg) % 45.55/45.60 % Maximal term depth : 1 ( 1 avg) % 45.55/45.60 % Number of predicates : 97 ( 97 usr; 0 prp; 1-2 aty) % 45.55/45.60 % Number of functors : 11 ( 11 usr; 11 con; 0-0 aty) % 45.55/45.60 % Number of variables : 153 ( 117 !; 36 ?) % 45.55/45.60 % SPC : FOF_THM_RFO_NEQ % 45.55/45.60 % 45.55/45.60 % Comments : Sean Bechhofer says there are some errors in the encoding of % 45.55/45.60 % datatypes, so this problem may not be perfect. At least it's % 45.55/45.60 % still representative of the type of reasoning required for OWL. % 45.55/45.60 %------------------------------------------------------------------------------ % 45.55/45.60 %----Thing and Nothing % 45.55/45.60 fof(axiom_0,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cowlThing(X) % 45.55/45.60 & ~ cowlNothing(X) ) ). % 45.55/45.60 % 45.55/45.60 %----String and Integer disjoint % 45.55/45.60 fof(axiom_1,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( xsd_string(X) % 45.55/45.60 <=> ~ xsd_integer(X) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC10 % 45.55/45.60 fof(axiom_2,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC10(X) % 45.55/45.60 <=> ( cC8(X) % 45.55/45.60 & cC4(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC102 % 45.55/45.60 fof(axiom_3,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC102(X) % 45.55/45.60 <=> ? [Y] : % 45.55/45.60 ( rR1(X,Y) % 45.55/45.60 & ~ cC6(Y) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC104 % 45.55/45.60 fof(axiom_4,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC104(X) % 45.55/45.60 <=> ( ~ cC100(X) % 45.55/45.60 & ~ cC102(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC106 % 45.55/45.60 fof(axiom_5,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC106(X) % 45.55/45.60 <=> ? [Y] : % 45.55/45.60 ( rR1(X,Y) % 45.55/45.60 & cC104(Y) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC108 % 45.55/45.60 fof(axiom_6,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC108(X) % 45.55/45.60 <=> ( ~ cC106(X) % 45.55/45.60 & ~ cC98(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC110 % 45.55/45.60 fof(axiom_7,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC110(X) % 45.55/45.60 <=> ( cC108(X) % 45.55/45.60 & cTOP(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC112 % 45.55/45.60 fof(axiom_8,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC112(X) % 45.55/45.60 <=> ( cC90(X) % 45.55/45.60 & cC110(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC114 % 45.55/45.60 fof(axiom_9,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC114(X) % 45.55/45.60 <=> cTOP(X) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC116 % 45.55/45.60 fof(axiom_10,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC116(X) % 45.55/45.60 <=> ( cC114(X) % 45.55/45.60 & cC112(X) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC118 % 45.55/45.60 fof(axiom_11,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC118(X) % 45.55/45.60 <=> ? [Y] : % 45.55/45.60 ( rR1(X,Y) % 45.55/45.60 & ~ cC92(Y) ) ) ). % 45.55/45.60 % 45.55/45.60 %----Equality cC120 % 45.55/45.60 fof(axiom_12,axiom, % 45.55/45.60 ! [X] : % 45.55/45.60 ( cC120(X) % 45.55/45.60 <=> ( ~ cC118(X) % 45.55/45.61 & ~ cC92(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC122 % 45.55/45.61 fof(axiom_13,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC122(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC120(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC124 % 45.55/45.61 fof(axiom_14,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC124(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC92(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC126 % 45.55/45.61 fof(axiom_15,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC126(X) % 45.55/45.61 <=> ( ~ cC124(X) % 45.55/45.61 & ~ cC100(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC128 % 45.55/45.61 fof(axiom_16,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC128(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC126(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC130 % 45.55/45.61 fof(axiom_17,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC130(X) % 45.55/45.61 <=> ( ~ cC122(X) % 45.55/45.61 & ~ cC128(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC132 % 45.55/45.61 fof(axiom_18,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC132(X) % 45.55/45.61 <=> ( cTOP(X) % 45.55/45.61 & cC130(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC134 % 45.55/45.61 fof(axiom_19,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC134(X) % 45.55/45.61 <=> ( cC132(X) % 45.55/45.61 & cC116(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC136 % 45.55/45.61 fof(axiom_20,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC136(X) % 45.55/45.61 <=> cTOP(X) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC138 % 45.55/45.61 fof(axiom_21,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC138(X) % 45.55/45.61 <=> ( cC136(X) % 45.55/45.61 & cC134(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC14 % 45.55/45.61 fof(axiom_22,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC14(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC12(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC140 % 45.55/45.61 fof(axiom_23,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC140(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC100(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC142 % 45.55/45.61 fof(axiom_24,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC142(X) % 45.55/45.61 <=> ( ~ cC140(X) % 45.55/45.61 & ~ cC92(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC144 % 45.55/45.61 fof(axiom_25,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC144(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC142(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC146 % 45.55/45.61 fof(axiom_26,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC146(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC100(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC148 % 45.55/45.61 fof(axiom_27,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC148(X) % 45.55/45.61 <=> ( ~ cC146(X) % 45.55/45.61 & ~ cC100(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC150 % 45.55/45.61 fof(axiom_28,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC150(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC148(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC152 % 45.55/45.61 fof(axiom_29,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC152(X) % 45.55/45.61 <=> ( ~ cC150(X) % 45.55/45.61 & ~ cC144(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC154 % 45.55/45.61 fof(axiom_30,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC154(X) % 45.55/45.61 <=> ( cTOP(X) % 45.55/45.61 & cC152(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC156 % 45.55/45.61 fof(axiom_31,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC156(X) % 45.55/45.61 <=> ( cC154(X) % 45.55/45.61 & cC138(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC158 % 45.55/45.61 fof(axiom_32,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC158(X) % 45.55/45.61 <=> ( cC22(X) % 45.55/45.61 & cC156(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC16 % 45.55/45.61 fof(axiom_33,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC16(X) % 45.55/45.61 <=> ( cC14(X) % 45.55/45.61 & cC10(X) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC160 % 45.55/45.61 fof(axiom_34,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC160(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC6(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC162 % 45.55/45.61 fof(axiom_35,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC162(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC160(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC164 % 45.55/45.61 fof(axiom_36,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC164(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & ~ cC92(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC166 % 45.55/45.61 fof(axiom_37,axiom, % 45.55/45.61 ! [X] : % 45.55/45.61 ( cC166(X) % 45.55/45.61 <=> ? [Y] : % 45.55/45.61 ( rR1(X,Y) % 45.55/45.61 & cC164(Y) ) ) ). % 45.55/45.61 % 45.55/45.61 %----Equality cC168 % 45.55/45.61 fof(axiom_38,axiom, % 45.55/45.61 ! [X] : % 45.60/45.61 ( cC168(X) % 45.60/45.61 <=> ( ~ cC166(X) % 45.60/45.61 & ~ cC162(X) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC170 % 45.60/45.61 fof(axiom_39,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC170(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & ~ cC18(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC172 % 45.60/45.61 fof(axiom_40,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC172(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & cC170(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC174 % 45.60/45.61 fof(axiom_41,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC174(X) % 45.60/45.61 <=> ( cC168(X) % 45.60/45.61 & ~ cC172(X) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC176 % 45.60/45.61 fof(axiom_42,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC176(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & ~ cC100(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC178 % 45.60/45.61 fof(axiom_43,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC178(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & cC176(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC180 % 45.60/45.61 fof(axiom_44,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC180(X) % 45.60/45.61 <=> ( ~ cC178(X) % 45.60/45.61 & cC174(X) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC20 % 45.60/45.61 fof(axiom_45,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC20(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & ~ cC18(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC22 % 45.60/45.61 fof(axiom_46,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC22(X) % 45.60/45.61 <=> ( cC16(X) % 45.60/45.61 & cC20(X) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC24 % 45.60/45.61 fof(axiom_47,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC24(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & ~ cC2(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC26 % 45.60/45.61 fof(axiom_48,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC26(X) % 45.60/45.61 <=> ( ~ cC24(X) % 45.60/45.61 & ~ cC2(X) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC28 % 45.60/45.61 fof(axiom_49,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC28(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & cC26(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC30 % 45.60/45.61 fof(axiom_50,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC30(X) % 45.60/45.61 <=> ? [Y] : % 45.60/45.61 ( rR1(X,Y) % 45.60/45.61 & ~ cC12(Y) ) ) ). % 45.60/45.61 % 45.60/45.61 %----Equality cC32 % 45.60/45.61 fof(axiom_51,axiom, % 45.60/45.61 ! [X] : % 45.60/45.61 ( cC32(X) % 45.60/45.62 <=> ( ~ cC2(X) % 45.60/45.62 & ~ cC30(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC34 % 45.60/45.62 fof(axiom_52,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC34(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC32(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC36 % 45.60/45.62 fof(axiom_53,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC36(X) % 45.60/45.62 <=> ( ~ cC28(X) % 45.60/45.62 & ~ cC34(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC38 % 45.60/45.62 fof(axiom_54,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC38(X) % 45.60/45.62 <=> ( cC36(X) % 45.60/45.62 & cTOP(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC4 % 45.60/45.62 fof(axiom_55,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC4(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC2(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC40 % 45.60/45.62 fof(axiom_56,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC40(X) % 45.60/45.62 <=> cTOP(X) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC42 % 45.60/45.62 fof(axiom_57,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC42(X) % 45.60/45.62 <=> ( cC40(X) % 45.60/45.62 & cC38(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC44 % 45.60/45.62 fof(axiom_58,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC44(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC2(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC46 % 45.60/45.62 fof(axiom_59,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC46(X) % 45.60/45.62 <=> ( ~ cC12(X) % 45.60/45.62 & ~ cC44(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC48 % 45.60/45.62 fof(axiom_60,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC48(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC46(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC50 % 45.60/45.62 fof(axiom_61,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC50(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC12(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC52 % 45.60/45.62 fof(axiom_62,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC52(X) % 45.60/45.62 <=> ( ~ cC12(X) % 45.60/45.62 & ~ cC50(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC54 % 45.60/45.62 fof(axiom_63,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC54(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC52(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC56 % 45.60/45.62 fof(axiom_64,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC56(X) % 45.60/45.62 <=> ( ~ cC48(X) % 45.60/45.62 & ~ cC54(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC58 % 45.60/45.62 fof(axiom_65,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC58(X) % 45.60/45.62 <=> ( cC56(X) % 45.60/45.62 & cTOP(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC60 % 45.60/45.62 fof(axiom_66,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC60(X) % 45.60/45.62 <=> ( cC58(X) % 45.60/45.62 & cC42(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC62 % 45.60/45.62 fof(axiom_67,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC62(X) % 45.60/45.62 <=> cTOP(X) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC64 % 45.60/45.62 fof(axiom_68,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC64(X) % 45.60/45.62 <=> ( cC62(X) % 45.60/45.62 & cC60(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC66 % 45.60/45.62 fof(axiom_69,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC66(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC2(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC68 % 45.60/45.62 fof(axiom_70,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC68(X) % 45.60/45.62 <=> ( ~ cC66(X) % 45.60/45.62 & ~ cC18(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC70 % 45.60/45.62 fof(axiom_71,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC70(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC68(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC72 % 45.60/45.62 fof(axiom_72,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC72(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC12(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC74 % 45.60/45.62 fof(axiom_73,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC74(X) % 45.60/45.62 <=> ( ~ cC18(X) % 45.60/45.62 & ~ cC72(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC76 % 45.60/45.62 fof(axiom_74,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC76(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC74(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC78 % 45.60/45.62 fof(axiom_75,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC78(X) % 45.60/45.62 <=> ( ~ cC70(X) % 45.60/45.62 & ~ cC76(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC8 % 45.60/45.62 fof(axiom_76,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC8(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC6(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC80 % 45.60/45.62 fof(axiom_77,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC80(X) % 45.60/45.62 <=> ( cTOP(X) % 45.60/45.62 & cC78(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC82 % 45.60/45.62 fof(axiom_78,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC82(X) % 45.60/45.62 <=> ( cC80(X) % 45.60/45.62 & cC64(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC84 % 45.60/45.62 fof(axiom_79,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC84(X) % 45.60/45.62 <=> cTOP(X) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC86 % 45.60/45.62 fof(axiom_80,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC86(X) % 45.60/45.62 <=> ( cC82(X) % 45.60/45.62 & cC84(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC88 % 45.60/45.62 fof(axiom_81,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC88(X) % 45.60/45.62 <=> cTOP(X) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC90 % 45.60/45.62 fof(axiom_82,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC90(X) % 45.60/45.62 <=> ( cC88(X) % 45.60/45.62 & cC86(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC94 % 45.60/45.62 fof(axiom_83,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC94(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & ~ cC6(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC96 % 45.60/45.62 fof(axiom_84,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC96(X) % 45.60/45.62 <=> ( ~ cC92(X) % 45.60/45.62 & ~ cC94(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cC98 % 45.60/45.62 fof(axiom_85,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cC98(X) % 45.60/45.62 <=> ? [Y] : % 45.60/45.62 ( rR1(X,Y) % 45.60/45.62 & cC96(Y) ) ) ). % 45.60/45.62 % 45.60/45.62 %----Equality cTEST % 45.60/45.62 fof(axiom_86,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( cTEST(X) % 45.60/45.62 <=> ( cC158(X) % 45.60/45.62 & cC180(X) ) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_87,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC26(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_88,axiom, % 45.60/45.62 cTOP(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_89,axiom, % 45.60/45.62 cTEST(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_90,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC104(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_91,axiom, % 45.60/45.62 ~ cC98(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_92,axiom, % 45.60/45.62 ~ cC122(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_93,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC148(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_94,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC160(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_95,axiom, % 45.60/45.62 ~ cC34(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_96,axiom, % 45.60/45.62 ~ cC28(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_97,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC126(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_98,axiom, % 45.60/45.62 ~ cC70(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_99,axiom, % 45.60/45.62 ~ cC178(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_100,axiom, % 45.60/45.62 ~ cC162(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_101,axiom, % 45.60/45.62 ~ cC166(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_102,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC68(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_103,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC164(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_104,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC46(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_105,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC52(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_106,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC176(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_107,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC142(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_108,axiom, % 45.60/45.62 ~ cC150(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_109,axiom, % 45.60/45.62 ~ cC54(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_110,axiom, % 45.60/45.62 ~ cC106(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_111,axiom, % 45.60/45.62 ~ cC144(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_112,axiom, % 45.60/45.62 ~ cC48(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_113,axiom, % 45.60/45.62 ~ cC76(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_114,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC32(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_115,axiom, % 45.60/45.62 ~ cC128(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_116,axiom, % 45.60/45.62 ~ cC172(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_117,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC120(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_118,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC96(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_119,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC170(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_120,axiom, % 45.60/45.62 cowlThing(iV21026) ). % 45.60/45.62 % 45.60/45.62 %----iV21026 % 45.60/45.62 fof(axiom_121,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21026,X) % 45.60/45.62 => ~ cC74(X) ) ). % 45.60/45.62 % 45.60/45.62 fof(axiom_122,axiom, % 45.60/45.62 rR1(iV21026,iV21030) ). % 45.60/45.62 % 45.60/45.62 fof(axiom_123,axiom, % 45.60/45.62 rR1(iV21026,iV21027) ). % 45.60/45.62 % 45.60/45.62 fof(axiom_124,axiom, % 45.60/45.62 rR1(iV21026,iV21028) ). % 45.60/45.62 % 45.60/45.62 fof(axiom_125,axiom, % 45.60/45.62 rR1(iV21026,iV21029) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_126,axiom, % 45.60/45.62 ~ cC26(iV21027) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_127,axiom, % 45.60/45.62 ~ cC176(iV21027) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_128,axiom, % 45.60/45.62 ! [X] : % 45.60/45.62 ( rR1(iV21027,X) % 45.60/45.62 => cC18(X) ) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_129,axiom, % 45.60/45.62 ~ cC46(iV21027) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_130,axiom, % 45.60/45.62 ~ cC170(iV21027) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.62 fof(axiom_131,axiom, % 45.60/45.62 cC12(iV21027) ). % 45.60/45.62 % 45.60/45.62 %----iV21027 % 45.60/45.63 fof(axiom_132,axiom, % 45.60/45.63 ~ cC120(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_133,axiom, % 45.60/45.63 ~ cC74(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_134,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21027,X) % 45.60/45.63 => cC6(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_135,axiom, % 45.60/45.63 ~ cC52(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_136,axiom, % 45.60/45.63 ~ cC32(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_137,axiom, % 45.60/45.63 ~ cC96(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_138,axiom, % 45.60/45.63 ~ cC68(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_139,axiom, % 45.60/45.63 cC92(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_140,axiom, % 45.60/45.63 ~ cC126(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_141,axiom, % 45.60/45.63 cC100(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_142,axiom, % 45.60/45.63 ~ cC160(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_143,axiom, % 45.60/45.63 ~ cC104(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_144,axiom, % 45.60/45.63 ~ cC148(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_145,axiom, % 45.60/45.63 ~ cC142(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_146,axiom, % 45.60/45.63 cC18(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_147,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21027,X) % 45.60/45.63 => cC92(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_148,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21027,X) % 45.60/45.63 => cC100(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_149,axiom, % 45.60/45.63 ~ cC164(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_150,axiom, % 45.60/45.63 ~ cC2(iV21027) ). % 45.60/45.63 % 45.60/45.63 %----iV21027 % 45.60/45.63 fof(axiom_151,axiom, % 45.60/45.63 cowlThing(iV21027) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_152,axiom, % 45.60/45.63 rR1(iV21027,iV21036) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_153,axiom, % 45.60/45.63 rR1(iV21027,iV21035) ). % 45.60/45.63 % 45.60/45.63 %----iV21028 % 45.60/45.63 fof(axiom_154,axiom, % 45.60/45.63 cowlThing(iV21028) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_155,axiom, % 45.60/45.63 ~ cC148(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_156,axiom, % 45.60/45.63 ~ cC68(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_157,axiom, % 45.60/45.63 ~ cC46(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_158,axiom, % 45.60/45.63 ~ cC104(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_159,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21029,X) % 45.60/45.63 => cC100(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_160,axiom, % 45.60/45.63 ~ cC176(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_161,axiom, % 45.60/45.63 ~ cC142(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_162,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21029,X) % 45.60/45.63 => cC92(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_163,axiom, % 45.60/45.63 ~ cC12(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_164,axiom, % 45.60/45.63 cC2(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_165,axiom, % 45.60/45.63 ~ cC74(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_166,axiom, % 45.60/45.63 ~ cC120(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_167,axiom, % 45.60/45.63 cC92(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_168,axiom, % 45.60/45.63 ~ cC52(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_169,axiom, % 45.60/45.63 ~ cC32(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_170,axiom, % 45.60/45.63 cC100(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_171,axiom, % 45.60/45.63 cC18(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_172,axiom, % 45.60/45.63 ~ cC170(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_173,axiom, % 45.60/45.63 ~ cC26(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_174,axiom, % 45.60/45.63 ~ cC96(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_175,axiom, % 45.60/45.63 ~ cC126(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_176,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21029,X) % 45.60/45.63 => cC6(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_177,axiom, % 45.60/45.63 ~ cC164(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_178,axiom, % 45.60/45.63 ~ cC160(iV21029) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_179,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21029,X) % 45.60/45.63 => cC18(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21029 % 45.60/45.63 fof(axiom_180,axiom, % 45.60/45.63 cowlThing(iV21029) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_181,axiom, % 45.60/45.63 rR1(iV21029,iV21034) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_182,axiom, % 45.60/45.63 rR1(iV21029,iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_183,axiom, % 45.60/45.63 ~ cC32(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_184,axiom, % 45.60/45.63 ~ cC26(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_185,axiom, % 45.60/45.63 ~ cC126(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_186,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21030,X) % 45.60/45.63 => cC18(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_187,axiom, % 45.60/45.63 ~ cC148(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_188,axiom, % 45.60/45.63 ~ cC46(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_189,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21030,X) % 45.60/45.63 => cC6(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_190,axiom, % 45.60/45.63 cC12(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_191,axiom, % 45.60/45.63 ~ cC68(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_192,axiom, % 45.60/45.63 ~ cC74(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_193,axiom, % 45.60/45.63 ~ cC96(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_194,axiom, % 45.60/45.63 ~ cC176(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_195,axiom, % 45.60/45.63 cC2(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_196,axiom, % 45.60/45.63 ~ cC104(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_197,axiom, % 45.60/45.63 cC92(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_198,axiom, % 45.60/45.63 cC100(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_199,axiom, % 45.60/45.63 ~ cC120(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_200,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21030,X) % 45.60/45.63 => cC100(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_201,axiom, % 45.60/45.63 ~ cC170(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_202,axiom, % 45.60/45.63 ~ cC18(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_203,axiom, % 45.60/45.63 ! [X] : % 45.60/45.63 ( rR1(iV21030,X) % 45.60/45.63 => cC92(X) ) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_204,axiom, % 45.60/45.63 ~ cC52(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_205,axiom, % 45.60/45.63 ~ cC160(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_206,axiom, % 45.60/45.63 ~ cC164(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_207,axiom, % 45.60/45.63 cowlThing(iV21030) ). % 45.60/45.63 % 45.60/45.63 %----iV21030 % 45.60/45.63 fof(axiom_208,axiom, % 45.60/45.63 ~ cC142(iV21030) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_209,axiom, % 45.60/45.63 rR1(iV21030,iV21032) ). % 45.60/45.63 % 45.60/45.63 fof(axiom_210,axiom, % 45.60/45.63 rR1(iV21030,iV21031) ). % 45.60/45.63 % 45.60/45.63 %----iV21031 % 45.60/45.63 fof(axiom_211,axiom, % 45.60/45.63 cowlThing(iV21031) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_212,axiom, % 45.60/45.63 cC92(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_213,axiom, % 45.60/45.63 cC100(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_214,axiom, % 45.60/45.63 ~ cC2(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_215,axiom, % 45.60/45.63 cC18(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_216,axiom, % 45.60/45.63 cC6(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21032 % 45.60/45.63 fof(axiom_217,axiom, % 45.60/45.63 cowlThing(iV21032) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_218,axiom, % 45.60/45.63 cC92(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_219,axiom, % 45.60/45.63 cC100(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_220,axiom, % 45.60/45.63 cC18(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_221,axiom, % 45.60/45.63 cC6(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_222,axiom, % 45.60/45.63 ~ cC12(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21033 % 45.60/45.63 fof(axiom_223,axiom, % 45.60/45.63 cowlThing(iV21033) ). % 45.60/45.63 % 45.60/45.63 %----iV21034 % 45.60/45.63 fof(axiom_224,axiom, % 45.60/45.63 cC92(iV21034) ). % 45.60/45.63 % 45.60/45.63 %----iV21034 % 45.60/45.63 fof(axiom_225,axiom, % 45.60/45.63 cC100(iV21034) ). % 45.67/45.63 % 45.67/45.63 %----iV21034 % 45.67/45.63 fof(axiom_226,axiom, % 45.67/45.63 cC18(iV21034) ). % 45.67/45.63 % 45.67/45.63 %----iV21034 % 45.67/45.63 fof(axiom_227,axiom, % 45.67/45.63 cC6(iV21034) ). % 45.67/45.63 % 45.67/45.63 %----iV21034 % 45.67/45.63 fof(axiom_228,axiom, % 45.67/45.63 ~ cC2(iV21034) ). % 45.67/45.63 % 45.67/45.63 %----iV21034 % 45.67/45.63 fof(axiom_229,axiom, % 45.67/45.63 cowlThing(iV21034) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_230,axiom, % 45.67/45.63 cC92(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_231,axiom, % 45.67/45.63 cC100(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_232,axiom, % 45.67/45.63 ~ cC12(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_233,axiom, % 45.67/45.63 cC18(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_234,axiom, % 45.67/45.63 cC6(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21035 % 45.67/45.63 fof(axiom_235,axiom, % 45.67/45.63 cowlThing(iV21035) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_236,axiom, % 45.67/45.63 cC92(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_237,axiom, % 45.67/45.63 cC100(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_238,axiom, % 45.67/45.63 cC18(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_239,axiom, % 45.67/45.63 cC6(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_240,axiom, % 45.67/45.63 ~ cC2(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----iV21036 % 45.67/45.63 fof(axiom_241,axiom, % 45.67/45.63 cowlThing(iV21036) ). % 45.67/45.63 % 45.67/45.63 %----Thing and Nothing % 45.67/45.63 %----String and Integer disjoint % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21026 % 45.67/45.63 %----iV21027 % 45.67/45.63 %----iV21027 % 45.67/45.63 %----iV21027 % 45.67/45.63 %----iV21029 % 45.67/45.63 %----iV21029 % 45.67/45.63 %----iV21029 % 45.67/45.63 %----iV21030 % 45.67/45.63 %----iV21030 % 45.67/45.63 %----iV21030 % 45.67/45.63 fof(the_axiom,conjecture, % 45.67/45.63 ( ! [X] : % 45.67/45.63 ( cowlThing(X) % 45.67/45.63 & ~ cowlNothing(X) ) % 45.67/45.63 & ! [X] : % 45.67/45.63 ( xsd_string(X) % 45.67/45.63 <=> ~ xsd_integer(X) ) % 45.67/45.63 & cowlThing(iV21026) % 45.67/45.63 & cC84(iV21026) % 45.67/45.63 & cC16(iV21026) % 45.67/45.63 & cC36(iV21026) % 45.67/45.63 & cC42(iV21026) % 45.67/45.63 & cC88(iV21026) % 45.67/45.63 & cC86(iV21026) % 45.67/45.63 & cC174(iV21026) % 45.67/45.63 & cC20(iV21026) % 45.67/45.63 & cC156(iV21026) % 45.67/45.63 & cC60(iV21026) % 45.67/45.63 & cC38(iV21026) % 45.67/45.63 & cC158(iV21026) % 45.67/45.63 & cC10(iV21026) % 45.67/45.63 & cC134(iV21026) % 45.67/45.63 & cC22(iV21026) % 45.67/45.63 & cC168(iV21026) % 45.67/45.63 & cC56(iV21026) % 45.67/45.63 & cC78(iV21026) % 45.67/45.63 & cC58(iV21026) % 45.67/45.63 & cC152(iV21026) % 45.67/45.63 & cC40(iV21026) % 45.67/45.63 & cC132(iV21026) % 45.67/45.63 & cC130(iV21026) % 45.67/45.63 & cC62(iV21026) % 45.67/45.63 & cC154(iV21026) % 45.67/45.63 & cC80(iV21026) % 45.67/45.63 & cC8(iV21026) % 45.67/45.63 & cC136(iV21026) % 45.67/45.63 & cC112(iV21026) % 45.67/45.63 & cC180(iV21026) % 45.67/45.63 & cC114(iV21026) % 45.67/45.63 & cC64(iV21026) % 45.67/45.63 & cC110(iV21026) % 45.67/45.63 & cC116(iV21026) % 45.67/45.63 & cC82(iV21026) % 45.67/45.63 & cC138(iV21026) % 45.67/45.63 & cC4(iV21026) % 45.67/45.63 & cC108(iV21026) % 45.67/45.63 & cC14(iV21026) % 45.67/45.63 & cC90(iV21026) % 45.67/45.63 & cowlThing(iV21027) % 45.67/45.63 & cC30(iV21027) % 45.67/45.63 & cC24(iV21027) % 45.67/45.63 & cowlThing(iV21029) % 45.67/45.63 & cC50(iV21029) % 45.67/45.63 & cC44(iV21029) % 45.67/45.63 & cowlThing(iV21030) % 45.67/45.63 & cC66(iV21030) % 45.67/45.63 & cC72(iV21030) ) ). % 45.67/45.63 % 45.67/45.63 %------------------------------------------------------------------------------ % 45.67/45.63 %------------------------------------------- % 45.67/45.63 % Proof found % 45.67/45.63 % SZS status Theorem for theBenchmark % 45.67/45.63 % SZS output start Proof % 45.67/45.63 %ClaNum:398(EqnAxiom:0) % 45.67/45.63 %VarNum:710(SingletonVarNum:316) % 45.67/45.63 %MaxLitNum:49 % 45.67/45.63 %MaxfuncDepth:1 % 45.67/45.63 %SharedTerms:180 % 45.67/45.63 %goalClause: 397 398 % 45.67/45.63 [1]P1(a1) % 45.67/45.63 [2]P1(a2) % 45.67/45.63 [3]P1(a3) % 45.67/45.63 [4]P1(a4) % 45.67/45.63 [5]P1(a5) % 45.67/45.63 [6]P2(a6) % 45.67/45.63 [7]P2(a7) % 45.67/45.63 [8]P2(a47) % 45.67/45.63 [9]P2(a1) % 45.67/45.63 [10]P2(a2) % 45.67/45.63 [11]P2(a3) % 45.67/45.63 [12]P2(a4) % 45.67/45.63 [13]P2(a5) % 45.67/45.63 [14]P70(a8) % 45.67/45.63 [15]P71(a6) % 45.67/45.63 [16]P71(a7) % 45.67/45.63 [17]P71(a47) % 45.67/45.63 [18]P71(a1) % 45.67/45.63 [19]P71(a2) % 45.67/45.63 [20]P71(a3) % 45.67/45.63 [21]P71(a4) % 45.67/45.63 [22]P71(a5) % 45.67/45.63 [23]P4(a6) % 45.67/45.63 [24]P4(a7) % 45.67/45.63 [25]P14(a7) % 45.67/45.63 [26]P14(a47) % 45.67/45.63 [27]P14(a1) % 45.67/45.63 [28]P14(a2) % 45.67/45.63 [29]P14(a3) % 45.67/45.63 [30]P14(a4) % 45.67/45.63 [31]P14(a5) % 45.67/45.63 [32]P47(a6) % 45.67/45.63 [33]P47(a47) % 45.67/45.63 [34]P89(a8) % 45.67/45.63 [35]P93(a8,a6) % 45.67/45.63 [36]P93(a8,a7) % 45.67/45.63 [37]P93(a8,a48) % 45.67/45.63 [38]P93(a8,a47) % 45.67/45.63 [39]P93(a6,a5) % 45.67/45.63 [40]P93(a6,a49) % 45.67/45.63 [41]P93(a7,a1) % 45.67/45.63 [42]P93(a7,a2) % 45.67/45.63 [43]P93(a47,a3) % 45.67/45.63 [44]P93(a47,a4) % 45.67/45.63 [45]~P5(a6) % 45.67/45.63 [46]~P5(a7) % 45.67/45.63 [47]~P5(a47) % 45.67/45.63 [48]~P7(a8) % 45.67/45.63 [49]~P90(a8) % 45.67/45.63 [50]~P15(a6) % 45.67/45.63 [51]~P15(a7) % 45.67/45.63 [52]~P15(a47) % 45.67/45.63 [53]~P16(a8) % 45.67/45.63 [54]~P17(a6) % 45.67/45.63 [55]~P17(a7) % 45.67/45.63 [56]~P17(a47) % 45.67/45.63 [57]~P19(a8) % 45.67/45.63 [58]~P4(a47) % 45.67/45.63 [59]~P4(a2) % 45.67/45.63 [60]~P4(a4) % 45.67/45.63 [61]~P20(a6) % 45.67/45.63 [62]~P20(a7) % 45.67/45.63 [63]~P20(a47) % 45.67/45.63 [64]~P28(a8) % 45.67/45.63 [65]~P29(a6) % 45.67/45.63 [66]~P29(a7) % 45.67/45.63 [67]~P29(a47) % 45.67/45.63 [68]~P31(a8) % 45.67/45.63 [69]~P32(a6) % 45.67/45.63 [70]~P32(a7) % 45.67/45.63 [71]~P32(a47) % 45.67/45.63 [72]~P38(a8) % 45.67/45.63 [73]~P39(a6) % 45.67/45.63 [74]~P39(a7) % 45.67/45.63 [75]~P39(a47) % 45.67/45.63 [76]~P40(a8) % 45.67/45.63 [77]~P41(a6) % 45.67/45.63 [78]~P41(a7) % 45.67/45.63 [79]~P41(a47) % 45.67/45.63 [80]~P14(a6) % 45.67/45.63 [81]~P43(a8) % 45.67/45.63 [82]~P44(a6) % 45.67/45.63 [83]~P44(a7) % 45.67/45.63 [84]~P44(a47) % 45.67/45.63 [85]~P46(a8) % 45.67/45.63 [86]~P47(a7) % 45.67/45.63 [87]~P47(a1) % 45.67/45.63 [88]~P47(a3) % 45.67/45.63 [89]~P47(a5) % 45.67/45.63 [90]~P49(a6) % 45.67/45.63 [91]~P49(a7) % 45.67/45.63 [92]~P49(a47) % 45.67/45.63 [93]~P53(a8) % 45.67/45.63 [94]~P54(a6) % 45.67/45.63 [95]~P54(a7) % 45.67/45.63 [96]~P54(a47) % 45.67/45.63 [97]~P56(a8) % 45.67/45.63 [98]~P57(a6) % 45.67/45.63 [99]~P57(a7) % 45.67/45.63 [100]~P57(a47) % 45.67/45.63 [101]~P64(a8) % 45.67/45.63 [102]~P65(a6) % 45.67/45.63 [103]~P65(a7) % 45.67/45.63 [104]~P65(a47) % 45.67/45.63 [105]~P67(a8) % 45.67/45.63 [106]~P72(a6) % 45.67/45.63 [107]~P72(a7) % 45.67/45.63 [108]~P72(a47) % 45.67/45.63 [109]~P77(a8) % 45.67/45.63 [110]~P78(a6) % 45.67/45.63 [111]~P78(a7) % 45.67/45.63 [112]~P78(a47) % 45.67/45.63 [113]~P80(a8) % 45.67/45.63 [114]~P91(a6) % 45.67/45.63 [115]~P91(a7) % 45.67/45.63 [116]~P91(a47) % 45.67/45.63 [117]~P94(x1171) % 45.67/45.63 [118]P96(x1181)+P95(x1181) % 45.67/45.63 [119]~P33(x1191)+P3(x1191) % 45.67/45.63 [120]~P3(x1201)+P81(x1201) % 45.67/45.63 [121]~P3(x1211)+P58(x1211) % 45.67/45.63 [122]~P9(x1221)+P8(x1221) % 45.67/45.63 [123]~P10(x1231)+P9(x1231) % 45.67/45.63 [124]~P9(x1241)+P70(x1241) % 45.67/45.63 [125]~P11(x1251)+P70(x1251) % 45.67/45.63 [126]~P21(x1261)+P70(x1261) % 45.67/45.63 [127]~P23(x1271)+P70(x1271) % 45.67/45.63 [128]~P34(x1281)+P70(x1281) % 45.67/45.63 [129]~P59(x1291)+P70(x1291) % 45.67/45.63 [130]~P61(x1301)+P70(x1301) % 45.67/45.63 [131]~P68(x1311)+P70(x1311) % 45.67/45.63 [132]~P73(x1321)+P70(x1321) % 45.67/45.63 [133]~P83(x1331)+P70(x1331) % 45.67/45.63 [134]~P84(x1341)+P70(x1341) % 45.67/45.63 [135]~P86(x1351)+P70(x1351) % 45.67/45.63 [136]~P12(x1361)+P10(x1361) % 45.67/45.63 [137]~P10(x1371)+P88(x1371) % 45.67/45.63 [138]~P70(x1381)+P11(x1381) % 45.67/45.63 [139]~P12(x1391)+P11(x1391) % 45.67/45.63 [140]~P24(x1401)+P12(x1401) % 45.67/45.63 [141]~P21(x1411)+P22(x1411) % 45.67/45.63 [142]~P24(x1421)+P21(x1421) % 45.67/45.63 [143]~P25(x1431)+P24(x1431) % 45.67/45.63 [144]~P70(x1441)+P23(x1441) % 45.67/45.63 [145]~P25(x1451)+P23(x1451) % 45.67/45.63 [146]~P36(x1461)+P25(x1461) % 45.67/45.63 [147]~P33(x1471)+P26(x1471) % 45.67/45.63 [148]~P34(x1481)+P35(x1481) % 45.67/45.63 [149]~P36(x1491)+P34(x1491) % 45.67/45.63 [150]~P37(x1501)+P36(x1501) % 45.67/45.63 [151]~P89(x1511)+P37(x1511) % 45.67/45.63 [152]~P37(x1521)+P50(x1521) % 45.67/45.63 [153]~P50(x1531)+P33(x1531) % 45.67/45.63 [154]~P45(x1541)+P42(x1541) % 45.67/45.63 [155]~P48(x1551)+P45(x1551) % 45.67/45.63 [156]~P89(x1561)+P48(x1561) % 45.67/45.63 [157]~P50(x1571)+P51(x1571) % 45.67/45.63 [158]~P59(x1581)+P60(x1581) % 45.67/45.63 [159]~P62(x1591)+P59(x1591) % 45.67/45.63 [160]~P70(x1601)+P61(x1601) % 45.67/45.63 [161]~P62(x1611)+P61(x1611) % 45.67/45.63 [162]~P74(x1621)+P62(x1621) % 45.67/45.63 [163]~P68(x1631)+P69(x1631) % 45.67/45.63 [164]~P74(x1641)+P68(x1641) % 45.67/45.63 [165]~P75(x1651)+P74(x1651) % 45.67/45.63 [166]~P70(x1661)+P73(x1661) % 45.67/45.63 [167]~P75(x1671)+P73(x1671) % 45.67/45.63 [168]~P85(x1681)+P75(x1681) % 45.67/45.63 [169]~P83(x1691)+P82(x1691) % 45.67/45.63 [170]~P85(x1701)+P83(x1701) % 45.67/45.63 [171]~P87(x1711)+P85(x1711) % 45.67/45.63 [172]~P70(x1721)+P84(x1721) % 45.67/45.63 [173]~P87(x1731)+P84(x1731) % 45.67/45.63 [174]~P88(x1741)+P87(x1741) % 45.67/45.63 [175]~P70(x1751)+P86(x1751) % 45.67/45.63 [176]~P88(x1761)+P86(x1761) % 45.67/45.63 [196]~P96(x1961)+~P95(x1961) % 45.67/45.63 [197]~P5(x1971)+~P6(x1971) % 45.67/45.63 [198]~P2(x1981)+~P5(x1981) % 45.67/45.63 [199]~P17(x1991)+~P2(x1991) % 45.67/45.63 [200]~P29(x2001)+~P2(x2001) % 45.67/45.63 [201]~P8(x2011)+~P7(x2011) % 45.67/45.63 [202]~P90(x2021)+~P8(x2021) % 45.67/45.63 [203]~P15(x2031)+~P13(x2031) % 45.67/45.63 [204]~P15(x2041)+~P71(x2041) % 45.67/45.63 [205]~P20(x2051)+~P71(x2051) % 45.67/45.63 [206]~P91(x2061)+~P71(x2061) % 45.67/45.63 [207]~P22(x2071)+~P16(x2071) % 45.67/45.63 [208]~P17(x2081)+~P18(x2081) % 45.67/45.63 [209]~P22(x2091)+~P19(x2091) % 45.67/45.63 [210]~P57(x2101)+~P4(x2101) % 45.67/45.63 [211]~P65(x2111)+~P4(x2111) % 45.67/45.63 [212]~P20(x2121)+~P27(x2121) % 45.67/45.63 [213]~P35(x2131)+~P28(x2131) % 45.67/45.63 [214]~P29(x2141)+~P30(x2141) % 45.67/45.63 [215]~P35(x2151)+~P31(x2151) % 45.67/45.63 [216]~P42(x2161)+~P38(x2161) % 45.67/45.63 [217]~P42(x2171)+~P40(x2171) % 45.67/45.63 [218]~P72(x2181)+~P14(x2181) % 45.67/45.63 [219]~P78(x2191)+~P14(x2191) % 45.67/45.63 [220]~P45(x2201)+~P43(x2201) % 45.67/45.63 [221]~P48(x2211)+~P46(x2211) % 45.67/45.63 [222]~P49(x2221)+~P52(x2221) % 45.67/45.63 [223]~P49(x2231)+~P47(x2231) % 45.67/45.63 [224]~P54(x2241)+~P47(x2241) % 45.67/45.63 [225]~P60(x2251)+~P53(x2251) % 45.67/45.63 [226]~P54(x2261)+~P55(x2261) % 45.67/45.63 [227]~P60(x2271)+~P56(x2271) % 45.67/45.63 [228]~P57(x2281)+~P63(x2281) % 45.67/45.63 [229]~P69(x2291)+~P64(x2291) % 45.67/45.63 [230]~P65(x2301)+~P66(x2301) % 45.67/45.63 [231]~P69(x2311)+~P67(x2311) % 45.67/45.63 [232]~P72(x2321)+~P76(x2321) % 45.67/45.63 [233]~P82(x2331)+~P77(x2331) % 45.67/45.63 [234]~P78(x2341)+~P79(x2341) % 45.67/45.63 [235]~P82(x2351)+~P80(x2351) % 45.67/45.63 [236]~P91(x2361)+~P92(x2361) % 45.67/45.63 [297]P1(x2971)+~P93(a6,x2971) % 45.67/45.63 [298]P1(x2981)+~P93(a7,x2981) % 45.67/45.63 [299]P1(x2991)+~P93(a47,x2991) % 45.67/45.63 [300]P2(x3001)+~P93(a6,x3001) % 45.67/45.63 [301]P2(x3011)+~P93(a7,x3011) % 45.67/45.63 [302]P2(x3021)+~P93(a47,x3021) % 45.67/45.63 [303]P71(x3031)+~P93(a6,x3031) % 45.67/45.63 [304]P71(x3041)+~P93(a7,x3041) % 45.67/45.63 [305]P71(x3051)+~P93(a47,x3051) % 45.67/45.63 [306]P14(x3061)+~P93(a6,x3061) % 45.67/45.63 [307]P14(x3071)+~P93(a7,x3071) % 45.67/45.63 [308]P14(x3081)+~P93(a47,x3081) % 45.67/45.63 [309]~P5(x3091)+~P93(a8,x3091) % 45.67/45.63 [310]~P15(x3101)+~P93(a8,x3101) % 45.67/45.63 [311]~P17(x3111)+~P93(a8,x3111) % 45.67/45.63 [312]~P20(x3121)+~P93(a8,x3121) % 45.67/45.63 [313]~P29(x3131)+~P93(a8,x3131) % 45.67/45.63 [314]~P32(x3141)+~P93(a8,x3141) % 45.67/45.63 [315]~P39(x3151)+~P93(a8,x3151) % 45.67/45.63 [316]~P41(x3161)+~P93(a8,x3161) % 45.67/45.63 [317]~P44(x3171)+~P93(a8,x3171) % 45.67/45.63 [318]~P49(x3181)+~P93(a8,x3181) % 45.67/45.63 [319]~P54(x3191)+~P93(a8,x3191) % 45.67/45.63 [320]~P57(x3201)+~P93(a8,x3201) % 45.67/45.63 [321]~P65(x3211)+~P93(a8,x3211) % 45.67/45.63 [322]~P72(x3221)+~P93(a8,x3221) % 45.67/45.63 [323]~P78(x3231)+~P93(a8,x3231) % 45.67/45.63 [324]~P91(x3241)+~P93(a8,x3241) % 45.67/45.63 [239]~P7(x2391)+P5(f9(x2391)) % 45.67/45.63 [240]~P16(x2401)+P15(f31(x2401)) % 45.67/45.63 [241]~P19(x2411)+P17(f42(x2411)) % 45.67/45.63 [242]~P28(x2421)+P20(f44(x2421)) % 45.67/45.63 [243]~P31(x2431)+P29(f10(x2431)) % 45.67/45.63 [244]~P38(x2441)+P32(f12(x2441)) % 45.67/45.63 [245]~P40(x2451)+P39(f14(x2451)) % 45.67/45.63 [246]~P43(x2461)+P41(f16(x2461)) % 45.67/45.63 [247]~P46(x2471)+P44(f18(x2471)) % 45.67/45.63 [248]~P53(x2481)+P49(f20(x2481)) % 45.67/45.63 [249]~P56(x2491)+P54(f24(x2491)) % 45.67/45.63 [250]~P64(x2501)+P57(f26(x2501)) % 45.67/45.63 [251]~P67(x2511)+P65(f29(x2511)) % 45.67/45.63 [252]~P77(x2521)+P72(f32(x2521)) % 45.67/45.63 [253]~P80(x2531)+P78(f34(x2531)) % 45.67/45.63 [254]~P90(x2541)+P91(f36(x2541)) % 45.67/45.63 [277]~P81(x2771)+~P1(f37(x2771)) % 45.67/45.63 [278]~P58(x2781)+~P47(f27(x2781)) % 45.67/45.63 [279]~P6(x2791)+~P1(f21(x2791)) % 45.67/45.63 [280]~P13(x2801)+~P71(f39(x2801)) % 45.67/45.63 [281]~P18(x2811)+~P71(f43(x2811)) % 45.67/45.63 [282]~P26(x2821)+~P4(f45(x2821)) % 45.67/45.63 [283]~P27(x2831)+~P2(f46(x2831)) % 45.67/45.63 [284]~P30(x2841)+~P2(f11(x2841)) % 45.67/45.63 [285]~P32(x2851)+~P1(f13(x2851)) % 45.67/45.63 [286]~P39(x2861)+~P71(f15(x2861)) % 45.67/45.63 [287]~P41(x2871)+~P14(f17(x2871)) % 45.67/45.63 [288]~P44(x2881)+~P2(f19(x2881)) % 45.67/45.63 [289]~P51(x2891)+~P14(f22(x2891)) % 45.67/45.63 [290]~P52(x2901)+~P47(f23(x2901)) % 45.67/45.63 [291]~P55(x2911)+~P4(f25(x2911)) % 45.67/45.63 [292]~P63(x2921)+~P47(f28(x2921)) % 45.67/45.63 [293]~P66(x2931)+~P4(f30(x2931)) % 45.67/45.63 [294]~P76(x2941)+~P47(f33(x2941)) % 45.67/45.63 [295]~P79(x2951)+~P4(f35(x2951)) % 45.67/45.63 [296]~P92(x2961)+~P1(f38(x2961)) % 45.67/45.63 [325]~P6(x3251)+P93(x3251,f21(x3251)) % 45.67/45.63 [326]~P7(x3261)+P93(x3261,f9(x3261)) % 45.67/45.63 [327]~P13(x3271)+P93(x3271,f39(x3271)) % 45.67/45.63 [328]~P16(x3281)+P93(x3281,f31(x3281)) % 45.67/45.63 [329]~P18(x3291)+P93(x3291,f43(x3291)) % 45.67/45.63 [330]~P19(x3301)+P93(x3301,f42(x3301)) % 45.67/45.63 [331]~P26(x3311)+P93(x3311,f45(x3311)) % 45.67/45.63 [332]~P27(x3321)+P93(x3321,f46(x3321)) % 45.67/45.63 [333]~P28(x3331)+P93(x3331,f44(x3331)) % 45.67/45.63 [334]~P30(x3341)+P93(x3341,f11(x3341)) % 45.67/45.63 [335]~P31(x3351)+P93(x3351,f10(x3351)) % 45.67/45.63 [336]~P32(x3361)+P93(x3361,f13(x3361)) % 45.67/45.63 [337]~P38(x3371)+P93(x3371,f12(x3371)) % 45.67/45.63 [338]~P39(x3381)+P93(x3381,f15(x3381)) % 45.67/45.63 [339]~P40(x3391)+P93(x3391,f14(x3391)) % 45.67/45.63 [340]~P41(x3401)+P93(x3401,f17(x3401)) % 45.67/45.63 [341]~P43(x3411)+P93(x3411,f16(x3411)) % 45.67/45.63 [342]~P44(x3421)+P93(x3421,f19(x3421)) % 45.67/45.63 [343]~P46(x3431)+P93(x3431,f18(x3431)) % 45.67/45.63 [344]~P51(x3441)+P93(x3441,f22(x3441)) % 45.67/45.63 [345]~P52(x3451)+P93(x3451,f23(x3451)) % 45.67/45.63 [346]~P53(x3461)+P93(x3461,f20(x3461)) % 45.67/45.63 [347]~P55(x3471)+P93(x3471,f25(x3471)) % 45.67/45.63 [348]~P56(x3481)+P93(x3481,f24(x3481)) % 45.67/45.63 [349]~P58(x3491)+P93(x3491,f27(x3491)) % 45.67/45.63 [350]~P63(x3501)+P93(x3501,f28(x3501)) % 45.67/45.63 [351]~P64(x3511)+P93(x3511,f26(x3511)) % 45.67/45.63 [352]~P66(x3521)+P93(x3521,f30(x3521)) % 45.67/45.63 [353]~P67(x3531)+P93(x3531,f29(x3531)) % 45.67/45.63 [354]~P76(x3541)+P93(x3541,f33(x3541)) % 45.67/45.63 [355]~P77(x3551)+P93(x3551,f32(x3551)) % 45.67/45.63 [356]~P79(x3561)+P93(x3561,f35(x3561)) % 45.67/45.63 [357]~P80(x3571)+P93(x3571,f34(x3571)) % 45.67/45.63 [358]~P81(x3581)+P93(x3581,f37(x3581)) % 45.67/45.63 [359]~P92(x3591)+P93(x3591,f38(x3591)) % 45.67/45.63 [360]~P90(x3601)+P93(x3601,f36(x3601)) % 45.67/45.63 [177]P5(x1771)+P2(x1771)+P6(x1771) % 45.67/45.63 [178]P18(x1781)+P17(x1781)+P2(x1781) % 45.67/45.63 [179]P30(x1791)+P29(x1791)+P2(x1791) % 45.67/45.63 [180]P8(x1801)+P90(x1801)+P7(x1801) % 45.67/45.63 [181]P71(x1811)+P15(x1811)+P13(x1811) % 45.67/45.63 [182]P27(x1821)+P20(x1821)+P71(x1821) % 45.67/45.63 [183]P92(x1831)+P91(x1831)+P71(x1831) % 45.67/45.63 [184]P19(x1841)+P22(x1841)+P16(x1841) % 45.67/45.63 [185]P63(x1851)+P57(x1851)+P4(x1851) % 45.67/45.63 [186]P66(x1861)+P65(x1861)+P4(x1861) % 45.67/45.63 [187]P31(x1871)+P35(x1871)+P28(x1871) % 45.67/45.63 [188]P40(x1881)+P42(x1881)+P38(x1881) % 45.67/45.63 [189]P76(x1891)+P72(x1891)+P14(x1891) % 45.67/45.63 [190]P79(x1901)+P78(x1901)+P14(x1901) % 45.67/45.63 [191]P47(x1911)+P49(x1911)+P52(x1911) % 45.67/45.63 [192]P55(x1921)+P54(x1921)+P47(x1921) % 45.67/45.63 [193]P56(x1931)+P60(x1931)+P53(x1931) % 45.67/45.63 [194]P67(x1941)+P69(x1941)+P64(x1941) % 45.67/45.63 [195]P80(x1951)+P82(x1951)+P77(x1951) % 45.67/45.63 [237]P45(x2371)+~P42(x2371)+P43(x2371) % 45.67/45.63 [238]P48(x2381)+~P45(x2381)+P46(x2381) % 45.67/45.63 [255]~P81(x2551)+~P58(x2551)+P3(x2551) % 45.67/45.63 [256]~P8(x2561)+~P70(x2561)+P9(x2561) % 45.67/45.63 [257]~P9(x2571)+~P88(x2571)+P10(x2571) % 45.67/45.63 [258]~P87(x2581)+~P86(x2581)+P88(x2581) % 45.67/45.63 [259]~P10(x2591)+~P11(x2591)+P12(x2591) % 45.67/45.63 [260]~P70(x2601)+~P22(x2601)+P21(x2601) % 45.67/45.63 [261]~P12(x2611)+~P21(x2611)+P24(x2611) % 45.67/45.63 [262]~P24(x2621)+~P23(x2621)+P25(x2621) % 45.67/45.63 [263]~P70(x2631)+~P35(x2631)+P34(x2631) % 45.67/45.63 [264]~P25(x2641)+~P34(x2641)+P36(x2641) % 45.67/45.63 [265]~P36(x2651)+~P50(x2651)+P37(x2651) % 45.67/45.63 [266]~P33(x2661)+~P51(x2661)+P50(x2661) % 45.67/45.63 [267]~P3(x2671)+~P26(x2671)+P33(x2671) % 45.67/45.63 [268]~P70(x2681)+~P60(x2681)+P59(x2681) % 45.67/45.63 [269]~P59(x2691)+~P61(x2691)+P62(x2691) % 45.67/45.63 [270]~P70(x2701)+~P69(x2701)+P68(x2701) % 45.67/45.63 [271]~P62(x2711)+~P68(x2711)+P74(x2711) % 45.67/45.63 [272]~P74(x2721)+~P73(x2721)+P75(x2721) % 45.67/45.63 [273]~P70(x2731)+~P82(x2731)+P83(x2731) % 45.67/45.63 [274]~P75(x2741)+~P83(x2741)+P85(x2741) % 45.67/45.63 [275]~P85(x2751)+~P84(x2751)+P87(x2751) % 45.67/45.63 [276]~P37(x2761)+~P48(x2761)+P89(x2761) % 45.67/45.63 [361]~P93(x3611,x3612)+P81(x3611)+P1(x3612) % 45.67/45.63 [362]~P93(x3621,x3622)+P58(x3621)+P47(x3622) % 45.67/45.63 [363]~P93(x3631,x3632)+P6(x3631)+P1(x3632) % 45.67/45.63 [364]~P93(x3642,x3641)+P1(x3641)+P32(x3642) % 45.67/45.63 [365]~P93(x3652,x3651)+P1(x3651)+P92(x3652) % 45.67/45.63 [366]~P93(x3662,x3661)+P2(x3661)+P27(x3662) % 45.67/45.63 [367]~P93(x3672,x3671)+P2(x3671)+P30(x3672) % 45.67/45.63 [368]~P93(x3682,x3681)+P2(x3681)+P44(x3682) % 45.67/45.63 [369]~P93(x3691,x3692)+P13(x3691)+P71(x3692) % 45.67/45.63 [370]~P93(x3702,x3701)+P71(x3701)+P18(x3702) % 45.67/45.63 [371]~P93(x3712,x3711)+P71(x3711)+P39(x3712) % 45.67/45.63 [372]~P93(x3721,x3722)+P26(x3721)+P4(x3722) % 45.67/45.63 [373]~P93(x3732,x3731)+P4(x3731)+P55(x3732) % 45.67/45.63 [374]~P93(x3742,x3741)+P4(x3741)+P66(x3742) % 45.67/45.63 [375]~P93(x3752,x3751)+P4(x3751)+P79(x3752) % 45.67/45.63 [376]~P93(x3761,x3762)+P41(x3761)+P14(x3762) % 45.67/45.63 [377]~P93(x3772,x3771)+P14(x3771)+P51(x3772) % 45.67/45.63 [378]~P93(x3781,x3782)+P52(x3781)+P47(x3782) % 45.67/45.63 [379]~P93(x3792,x3791)+P47(x3791)+P63(x3792) % 45.67/45.63 [380]~P93(x3802,x3801)+P47(x3801)+P76(x3802) % 45.67/45.63 [381]~P93(x3811,x3812)+P7(x3811)+~P5(x3812) % 45.67/45.63 [382]~P93(x3821,x3822)+P90(x3821)+~P91(x3822) % 45.67/45.63 [383]~P93(x3831,x3832)+P16(x3831)+~P15(x3832) % 45.67/45.63 [384]~P93(x3841,x3842)+P19(x3841)+~P17(x3842) % 45.67/45.63 [385]~P93(x3851,x3852)+P28(x3851)+~P20(x3852) % 45.67/45.63 [386]~P93(x3861,x3862)+P31(x3861)+~P29(x3862) % 45.67/45.63 [387]~P93(x3871,x3872)+P38(x3871)+~P32(x3872) % 45.67/45.63 [388]~P93(x3881,x3882)+P40(x3881)+~P39(x3882) % 45.67/45.63 [389]~P93(x3891,x3892)+P43(x3891)+~P41(x3892) % 45.67/45.63 [390]~P93(x3901,x3902)+P46(x3901)+~P44(x3902) % 45.67/45.63 [391]~P93(x3911,x3912)+P53(x3911)+~P49(x3912) % 45.67/45.63 [392]~P93(x3921,x3922)+P56(x3921)+~P54(x3922) % 45.67/45.63 [393]~P93(x3931,x3932)+P64(x3931)+~P57(x3932) % 45.67/45.63 [394]~P93(x3941,x3942)+P67(x3941)+~P65(x3942) % 45.67/45.63 [395]~P93(x3951,x3952)+P77(x3951)+~P72(x3952) % 45.67/45.63 [396]~P93(x3961,x3962)+P80(x3961)+~P78(x3962) % 45.67/45.63 [397]P94(a40)+P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P8(a8)+~P9(a8)+~P10(a8)+~P88(a8)+~P11(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P51(a8)+~P52(a7)+~P55(a7)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P63(a47)+~P66(a47)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P76(a6)+~P79(a6)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8) % 45.67/45.63 [398]P94(a40)+P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P8(a8)+~P9(a8)+~P10(a8)+~P88(a8)+~P11(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P51(a8)+~P52(a7)+~P55(a7)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P63(a47)+~P66(a47)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P76(a6)+~P79(a6)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8) % 45.67/45.63 %EqnAxiom % 45.67/45.63 % 45.67/45.63 %------------------------------------------- % 45.67/45.64 cnf(439,plain, % 45.67/45.64 (~P32(a48)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314])). % 45.67/45.64 cnf(443,plain, % 45.67/45.64 (~P41(a48)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316])). % 45.67/45.64 cnf(457,plain, % 45.67/45.64 (P8(a8)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180])). % 45.67/45.64 cnf(459,plain, % 45.67/45.64 (P63(a47)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,100,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185])). % 45.67/45.64 cnf(461,plain, % 45.67/45.64 (P66(a47)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,100,104,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186])). % 45.67/45.64 cnf(463,plain, % 45.67/45.64 (P76(a6)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,80,100,104,106,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189])). % 45.67/45.64 cnf(465,plain, % 45.67/45.64 (P79(a6)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,80,100,104,106,110,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189,190])). % 45.67/45.64 cnf(467,plain, % 45.67/45.64 (P52(a7)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,80,86,91,100,104,106,110,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189,190,191])). % 45.67/45.64 cnf(469,plain, % 45.67/45.64 (P55(a7)), % 45.67/45.64 inference(scs_inference,[],[37,39,40,41,43,48,49,58,80,86,91,95,100,104,106,110,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189,190,191,192])). % 45.67/45.64 cnf(471,plain, % 45.67/45.64 (P9(a8)), % 45.67/45.64 inference(scs_inference,[],[14,37,39,40,41,43,48,49,58,80,86,91,95,100,104,106,110,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189,190,191,192,256])). % 45.67/45.64 cnf(479,plain, % 45.67/45.64 (P51(a8)), % 45.67/45.64 inference(scs_inference,[],[14,35,37,38,39,40,41,43,48,49,58,80,86,91,95,100,104,106,110,9,18,27,218,219,318,319,320,321,322,323,206,297,298,299,300,303,306,309,310,311,312,313,314,315,316,317,324,199,200,204,205,180,185,186,189,190,191,192,256,373,374,375,377])). % 45.67/45.64 cnf(500,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P11(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[117,457,471,479,467,469,459,461,463,465,397])). % 45.67/45.64 cnf(501,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P11(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[117,457,471,479,467,469,459,461,463,465,398])). % 45.67/45.64 cnf(835,plain, % 45.67/45.64 (P81(x8351)+~P33(x8351)), % 45.67/45.64 inference(scs_inference,[],[119,120])). % 45.67/45.64 cnf(1318,plain, % 45.67/45.64 (P11(a8)), % 45.67/45.64 inference(scs_inference,[],[471,124,138])). % 45.67/45.64 cnf(1319,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1318,500])). % 45.67/45.64 cnf(1320,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P23(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1318,501])). % 45.67/45.64 cnf(1427,plain, % 45.67/45.64 (P23(a8)), % 45.67/45.64 inference(scs_inference,[],[1318,125,144])). % 45.67/45.64 cnf(1428,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1427,1319])). % 45.67/45.64 cnf(1429,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P73(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1427,1320])). % 45.67/45.64 cnf(1657,plain, % 45.67/45.64 (P73(a8)), % 45.67/45.64 inference(scs_inference,[],[1427,127,166])). % 45.67/45.64 cnf(1658,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1657,1428])). % 45.67/45.64 cnf(1659,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P61(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[1657,1429])). % 45.67/45.64 cnf(1766,plain, % 45.67/45.64 (P84(x17661)+~P34(x17661)), % 45.67/45.64 inference(scs_inference,[],[128,172])). % 45.67/45.64 cnf(1887,plain, % 45.67/45.64 (P86(x18871)+~P59(x18871)), % 45.67/45.64 inference(scs_inference,[],[129,175])). % 45.67/45.64 cnf(2250,plain, % 45.67/45.64 (P61(a8)), % 45.67/45.64 inference(scs_inference,[],[1657,132,160])). % 45.67/45.64 cnf(2251,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[2250,1658])). % 45.67/45.64 cnf(2252,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P50(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[2250,1659])). % 45.67/45.64 cnf(2261,plain, % 45.67/45.64 (P62(a8)+~P59(a8)), % 45.67/45.64 inference(scs_inference,[],[2250,42,43,40,80,443,297,298,299,376,269])). % 45.67/45.64 cnf(2722,plain, % 45.67/45.64 (P88(x27221)+~P12(x27221)), % 45.67/45.64 inference(scs_inference,[],[136,137])). % 45.67/45.64 cnf(2843,plain, % 45.67/45.64 (P70(x28431)+~P12(x28431)), % 45.67/45.64 inference(scs_inference,[],[139,125])). % 45.67/45.64 cnf(2964,plain, % 45.67/45.64 (~P24(x29641)+P88(x29641)), % 45.67/45.64 inference(scs_inference,[],[140,2722])). % 45.67/45.64 cnf(3085,plain, % 45.67/45.64 (~P16(x30851)+~P21(x30851)), % 45.67/45.64 inference(scs_inference,[],[141,207])). % 45.67/45.64 cnf(3811,plain, % 45.67/45.64 (~P28(x38111)+~P34(x38111)), % 45.67/45.64 inference(scs_inference,[],[148,213])). % 45.67/45.64 cnf(4174,plain, % 45.67/45.64 (P50(a8)), % 45.67/45.64 inference(scs_inference,[],[34,151,152])). % 45.67/45.64 cnf(4175,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,2251])). % 45.67/45.64 cnf(4176,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P3(a8)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,2252])). % 45.67/45.64 cnf(4185,plain, % 45.67/45.64 (P37(a8)+~P36(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,42,43,40,80,443,298,299,297,376,265])). % 45.67/45.64 cnf(4283,plain, % 45.67/45.64 (P3(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,153,119])). % 45.67/45.64 cnf(4284,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4283,4175])). % 45.67/45.64 cnf(4285,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P45(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4283,4176])). % 45.67/45.64 cnf(4390,plain, % 45.67/45.64 (~P38(x43901)+~P45(x43901)), % 45.67/45.64 inference(scs_inference,[],[154,216])). % 45.67/45.64 cnf(4632,plain, % 45.67/45.64 (P45(a8)), % 45.67/45.64 inference(scs_inference,[],[34,156,155])). % 45.67/45.64 cnf(4633,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4632,4284])). % 45.67/45.64 cnf(4634,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P48(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4632,4285])). % 45.67/45.64 cnf(4641,plain, % 45.67/45.64 (P48(a8)), % 45.67/45.64 inference(scs_inference,[],[4632,42,43,40,85,299,298,297,238])). % 45.67/45.64 cnf(4653,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4641,4633])). % 45.67/45.64 cnf(4654,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P81(a8)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[4641,4634])). % 45.67/45.64 cnf(4727,plain, % 45.67/45.64 (~P14(f22(a8))), % 45.67/45.64 inference(scs_inference,[],[4174,157,289])). % 45.67/45.64 cnf(4851,plain, % 45.67/45.64 (~P53(x48511)+~P59(x48511)), % 45.67/45.64 inference(scs_inference,[],[158,225])). % 45.67/45.64 cnf(4972,plain, % 45.67/45.64 (~P62(x49721)+P86(x49721)), % 45.67/45.64 inference(scs_inference,[],[159,1887])). % 45.67/45.64 cnf(5214,plain, % 45.67/45.64 (P86(x52141)+~P74(x52141)), % 45.67/45.64 inference(scs_inference,[],[162,4972])). % 45.67/45.64 cnf(5335,plain, % 45.67/45.64 (~P64(x53351)+~P68(x53351)), % 45.67/45.64 inference(scs_inference,[],[163,229])). % 45.67/45.64 cnf(5940,plain, % 45.67/45.64 (~P77(x59401)+~P83(x59401)), % 45.67/45.64 inference(scs_inference,[],[169,233])). % 45.67/45.64 cnf(7390,plain, % 45.67/45.64 (P22(a8)+~P22(a8)), % 45.67/45.64 inference(scs_inference,[],[53,209,184])). % 45.67/45.64 cnf(10654,plain, % 45.67/45.64 (P81(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,835,153])). % 45.67/45.64 cnf(10655,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[10654,4653])). % 45.67/45.64 cnf(10656,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P42(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[10654,4654])). % 45.67/45.64 cnf(11364,plain, % 45.67/45.64 (P70(x113641)+~P24(x113641)), % 45.67/45.64 inference(scs_inference,[],[2843,140])). % 45.67/45.64 cnf(11485,plain, % 45.67/45.64 (P87(x114851)+~P24(x114851)), % 45.67/45.64 inference(scs_inference,[],[2964,174])). % 45.67/45.64 cnf(11606,plain, % 45.67/45.64 (~P16(x116061)+~P24(x116061)), % 45.67/45.64 inference(scs_inference,[],[3085,142])). % 45.67/45.64 cnf(11968,plain, % 45.67/45.64 (~P28(x119681)+~P36(x119681)), % 45.67/45.64 inference(scs_inference,[],[3811,149])). % 45.67/45.64 cnf(12452,plain, % 45.67/45.64 (P42(a8)), % 45.67/45.64 inference(scs_inference,[],[4632,76,4390,188])). % 45.67/45.64 cnf(12453,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[12452,10655])). % 45.67/45.64 cnf(12454,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P35(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[12452,10656])). % 45.67/45.64 cnf(12679,plain, % 45.67/45.64 (~P53(x126791)+~P62(x126791)), % 45.67/45.64 inference(scs_inference,[],[4851,159])). % 45.67/45.64 cnf(12921,plain, % 45.67/45.64 (P86(x129211)+~P75(x129211)), % 45.67/45.64 inference(scs_inference,[],[5214,165])). % 45.67/45.64 cnf(13042,plain, % 45.67/45.64 (~P64(x130421)+~P74(x130421)), % 45.67/45.64 inference(scs_inference,[],[5335,164])). % 45.67/45.64 cnf(13404,plain, % 45.67/45.64 (~P77(x134041)+~P85(x134041)), % 45.67/45.64 inference(scs_inference,[],[5940,170])). % 45.67/45.64 cnf(14728,plain, % 45.67/45.64 (~P24(x147281)+P23(x147281)), % 45.67/45.64 inference(scs_inference,[],[11364,144])). % 45.67/45.64 cnf(14849,plain, % 45.67/45.64 (P87(x148491)+~P25(x148491)), % 45.67/45.64 inference(scs_inference,[],[11485,143])). % 45.67/45.64 cnf(14970,plain, % 45.67/45.64 (~P16(x149701)+~P25(x149701)), % 45.67/45.64 inference(scs_inference,[],[11606,143])). % 45.67/45.64 cnf(15212,plain, % 45.67/45.64 (~P28(x152121)+~P37(x152121)), % 45.67/45.64 inference(scs_inference,[],[11968,150])). % 45.67/45.64 cnf(15574,plain, % 45.67/45.64 (~P53(x155741)+~P74(x155741)), % 45.67/45.64 inference(scs_inference,[],[12679,162])). % 45.67/45.64 cnf(15816,plain, % 45.67/45.64 (P86(x158161)+~P85(x158161)), % 45.67/45.64 inference(scs_inference,[],[12921,168])). % 45.67/45.64 cnf(15937,plain, % 45.67/45.64 (~P64(x159371)+~P75(x159371)), % 45.67/45.64 inference(scs_inference,[],[13042,165])). % 45.67/45.64 cnf(16179,plain, % 45.67/45.64 (~P77(x161791)+~P87(x161791)), % 45.67/45.64 inference(scs_inference,[],[13404,171])). % 45.67/45.64 cnf(16663,plain, % 45.67/45.64 (P25(x166631)+~P24(x166631)), % 45.67/45.64 inference(scs_inference,[],[14728,262])). % 45.67/45.64 cnf(16784,plain, % 45.67/45.64 (P87(x167841)+~P36(x167841)), % 45.67/45.64 inference(scs_inference,[],[14849,146])). % 45.67/45.64 cnf(16905,plain, % 45.67/45.64 (~P16(x169051)+~P36(x169051)), % 45.67/45.64 inference(scs_inference,[],[14970,146])). % 45.67/45.64 cnf(17147,plain, % 45.67/45.64 (~P37(a8)+P35(a8)), % 45.67/45.64 inference(scs_inference,[],[68,15212,187])). % 45.67/45.64 cnf(17268,plain, % 45.67/45.64 (~P53(x172681)+~P75(x172681)), % 45.67/45.64 inference(scs_inference,[],[15574,165])). % 45.67/45.64 cnf(17509,plain, % 45.67/45.64 (P86(x175091)+~P87(x175091)), % 45.67/45.64 inference(scs_inference,[],[15816,171])). % 45.67/45.64 cnf(17630,plain, % 45.67/45.64 (~P64(x176301)+~P85(x176301)), % 45.67/45.64 inference(scs_inference,[],[15937,168])). % 45.67/45.64 cnf(17872,plain, % 45.67/45.64 (~P77(x178721)+~P88(x178721)), % 45.67/45.64 inference(scs_inference,[],[16179,174])). % 45.67/45.64 cnf(18477,plain, % 45.67/45.64 (P87(x184771)+~P37(x184771)), % 45.67/45.64 inference(scs_inference,[],[16784,150])). % 45.67/45.64 cnf(18598,plain, % 45.67/45.64 (~P16(x185981)+~P37(x185981)), % 45.67/45.64 inference(scs_inference,[],[16905,150])). % 45.67/45.64 cnf(18840,plain, % 45.67/45.64 (P35(a8)), % 45.67/45.64 inference(scs_inference,[],[34,17147,151])). % 45.67/45.64 cnf(18841,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[18840,12453])). % 45.67/45.64 cnf(18842,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P34(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P84(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[18840,12454])). % 45.67/45.64 cnf(18849,plain, % 45.67/45.64 (P34(a8)), % 45.67/45.64 inference(scs_inference,[],[18840,42,43,40,14,299,298,297,263])). % 45.67/45.64 cnf(18853,plain, % 45.67/45.64 (P84(a8)), % 45.67/45.64 inference(scs_inference,[],[18840,4727,42,43,40,14,443,299,298,297,263,376,1766])). % 45.67/45.64 cnf(18855,plain, % 45.67/45.64 (P36(a8)+~P25(a8)), % 45.67/45.64 inference(scs_inference,[],[18840,4727,42,43,40,14,443,299,298,297,263,376,1766,264])). % 45.67/45.64 cnf(18857,plain, % 45.67/45.64 (P37(a8)+~P25(a8)), % 45.67/45.64 inference(scs_inference,[],[4174,18840,4727,42,43,40,14,443,299,298,297,263,376,1766,264,265])). % 45.67/45.64 cnf(18870,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[18849,18853,18841])). % 45.67/45.64 cnf(18871,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P87(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[18849,18853,18842])). % 45.67/45.64 cnf(18944,plain, % 45.67/45.64 (~P53(x189441)+~P85(x189441)), % 45.67/45.64 inference(scs_inference,[],[17268,168])). % 45.67/45.64 cnf(19186,plain, % 45.67/45.64 (~P64(x191861)+~P87(x191861)), % 45.67/45.64 inference(scs_inference,[],[17630,171])). % 45.67/45.64 cnf(19307,plain, % 45.67/45.64 (~P12(x193071)+~P77(x193071)), % 45.67/45.64 inference(scs_inference,[],[17872,2722])). % 45.67/45.64 cnf(19911,plain, % 45.67/45.64 (P87(a8)), % 45.67/45.64 inference(scs_inference,[],[34,18477,151])). % 45.67/45.64 cnf(19912,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,18870])). % 45.67/45.64 cnf(19913,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P10(a8)+~P88(a8)+~P12(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)+~P86(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,18871])). % 45.67/45.64 cnf(19914,plain, % 45.67/45.64 (P86(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,17509])). % 45.67/45.64 cnf(19922,plain, % 45.67/45.64 (P88(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,44,41,39,17509,299,297,298,258])). % 45.67/45.64 cnf(19926,plain, % 45.67/45.64 (P10(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,471,4727,44,41,39,443,17509,299,297,298,258,376,257])). % 45.67/45.64 cnf(19928,plain, % 45.67/45.64 (P12(a8)), % 45.67/45.64 inference(scs_inference,[],[1318,19911,471,4727,44,41,39,443,17509,299,297,298,258,376,257,259])). % 45.67/45.64 cnf(19938,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[19926,19922,19928,19914,19912])). % 45.67/45.64 cnf(19939,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P82(a8)+~P83(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[19926,19922,19928,19914,19913])). % 45.67/45.64 cnf(20012,plain, % 45.67/45.64 (~P37(a8)+P22(a8)), % 45.67/45.64 inference(scs_inference,[],[57,18598,184])). % 45.67/45.64 cnf(20133,plain, % 45.67/45.64 (~P24(a8)+P36(a8)), % 45.67/45.64 inference(scs_inference,[],[18855,16663])). % 45.67/45.64 cnf(20254,plain, % 45.67/45.64 (~P25(a8)+P22(a8)), % 45.67/45.64 inference(scs_inference,[],[18857,20012])). % 45.67/45.64 cnf(20375,plain, % 45.67/45.64 (~P85(a8)+P60(a8)), % 45.67/45.64 inference(scs_inference,[],[97,18944,193])). % 45.67/45.64 cnf(20617,plain, % 45.67/45.64 (~P24(x206171)+~P64(x206171)), % 45.67/45.64 inference(scs_inference,[],[19186,11485])). % 45.67/45.64 cnf(20738,plain, % 45.67/45.64 (P82(a8)), % 45.67/45.64 inference(scs_inference,[],[19928,113,19307,195])). % 45.67/45.64 cnf(20739,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P83(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[20738,19938])). % 45.67/45.64 cnf(20740,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P83(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[20738,19939])). % 45.67/45.64 cnf(20747,plain, % 45.67/45.64 (P83(a8)), % 45.67/45.64 inference(scs_inference,[],[20738,42,43,40,14,299,297,298,273])). % 45.67/45.64 cnf(20753,plain, % 45.67/45.64 (~P75(a8)+P60(a8)), % 45.67/45.64 inference(scs_inference,[],[20738,4727,42,43,40,14,443,299,297,298,273,376,274,20375])). % 45.67/45.64 cnf(20754,plain, % 45.67/45.64 (P59(a8)+~P75(a8)), % 45.67/45.64 inference(scs_inference,[],[20738,4727,42,43,40,14,443,299,297,298,273,376,274,20375,268])). % 45.67/45.64 cnf(20765,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[20747,20739])). % 45.67/45.64 cnf(20766,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P36(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[20747,20740])). % 45.67/45.64 cnf(21200,plain, % 45.67/45.64 (~P21(a8)+P36(a8)), % 45.67/45.64 inference(scs_inference,[],[19928,20133,261])). % 45.67/45.64 cnf(21321,plain, % 45.67/45.64 (~P36(a8)+P22(a8)), % 45.67/45.64 inference(scs_inference,[],[20254,146])). % 45.67/45.64 cnf(21563,plain, % 45.67/45.64 (P69(a8)+~P24(a8)), % 45.67/45.64 inference(scs_inference,[],[105,20617,194])). % 45.67/45.64 cnf(21926,plain, % 45.67/45.64 (~P75(a8)+P62(a8)), % 45.67/45.64 inference(scs_inference,[],[20754,2261])). % 45.67/45.64 cnf(22167,plain, % 45.67/45.64 (~P22(a8)+P36(a8)), % 45.67/45.64 inference(scs_inference,[],[14,21200,260])). % 45.67/45.64 cnf(22530,plain, % 45.67/45.64 (P68(a8)+~P24(a8)), % 45.67/45.64 inference(scs_inference,[],[14,21563,270])). % 45.67/45.64 cnf(22892,plain, % 45.67/45.64 (~P85(a8)+P62(a8)), % 45.67/45.64 inference(scs_inference,[],[21926,168])). % 45.67/45.64 cnf(23013,plain, % 45.67/45.64 (P36(a8)), % 45.67/45.64 inference(scs_inference,[],[53,57,22167,184])). % 45.67/45.64 cnf(23014,plain, % 45.67/45.64 (P37(a8)), % 45.67/45.64 inference(scs_inference,[],[23013,4185])). % 45.67/45.64 cnf(23015,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23013,20765])). % 45.67/45.64 cnf(23016,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P22(a8)+~P21(a8)+~P24(a8)+~P25(a8)+~P26(a8)+~P37(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23013,20766])). % 45.67/45.64 cnf(23017,plain, % 45.67/45.64 (P22(a8)), % 45.67/45.64 inference(scs_inference,[],[23013,21321])). % 45.67/45.64 cnf(23026,plain, % 45.67/45.64 (P22(a8)), % 45.67/45.64 inference(scs_inference,[],[23017,7390])). % 45.67/45.64 cnf(23034,plain, % 45.67/45.64 (P21(a8)), % 45.67/45.64 inference(scs_inference,[],[23017,42,43,40,14,299,298,297,260])). % 45.67/45.64 cnf(23036,plain, % 45.67/45.64 (P24(a8)), % 45.67/45.64 inference(scs_inference,[],[19928,23017,42,43,40,14,299,298,297,260,261])). % 45.67/45.64 cnf(23040,plain, % 45.67/45.64 (P25(a8)), % 45.67/45.64 inference(scs_inference,[],[19928,23017,4727,42,43,40,14,443,299,298,297,260,261,376,16663])). % 45.67/45.64 cnf(23044,plain, % 45.67/45.64 (P69(a8)), % 45.67/45.64 inference(scs_inference,[],[23036,21563])). % 45.67/45.64 cnf(23046,plain, % 45.67/45.64 (P68(a8)), % 45.67/45.64 inference(scs_inference,[],[23036,22530])). % 45.67/45.64 cnf(23047,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23026,23034,23036,23040,23014,23015])). % 45.67/45.64 cnf(23048,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P69(a8)+~P68(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23026,23034,23036,23040,23014,23016])). % 45.67/45.64 cnf(23066,plain, % 45.67/45.64 (P74(a8)+~P62(a8)), % 45.67/45.64 inference(scs_inference,[],[23046,4727,42,43,40,443,297,299,298,376,271])). % 45.67/45.64 cnf(23068,plain, % 45.67/45.64 (P75(a8)+~P62(a8)), % 45.67/45.64 inference(scs_inference,[],[1657,23046,4727,42,43,40,443,297,299,298,376,271,272])). % 45.67/45.64 cnf(23070,plain, % 45.67/45.64 (P85(a8)+~P62(a8)), % 45.67/45.64 inference(scs_inference,[],[20747,1657,23046,4727,42,43,40,443,297,299,298,376,271,272,274])). % 45.67/45.64 cnf(23072,plain, % 45.67/45.64 (~P62(a8)+P60(a8)), % 45.67/45.64 inference(scs_inference,[],[20747,1657,23046,4727,42,43,40,443,297,299,298,376,271,272,274,20753])). % 45.67/45.64 cnf(23076,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23044,23046,23047])). % 45.67/45.64 cnf(23077,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P62(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23044,23046,23048])). % 45.67/45.64 cnf(23406,plain, % 45.67/45.64 (P62(a8)), % 45.67/45.64 inference(scs_inference,[],[19911,22892,171])). % 45.67/45.64 cnf(23407,plain, % 45.67/45.64 (P74(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23066])). % 45.67/45.64 cnf(23408,plain, % 45.67/45.64 (P75(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23068])). % 45.67/45.64 cnf(23409,plain, % 45.67/45.64 (P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23070])). % 45.67/45.64 cnf(23410,plain, % 45.67/45.64 (P60(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23072])). % 45.67/45.64 cnf(23411,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23076])). % 45.67/45.64 cnf(23412,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P26(a8)+~P33(a8)+~P60(a8)+~P59(a8)+~P74(a8)+~P75(a8)+~P85(a8)), % 45.67/45.64 inference(scs_inference,[],[23406,23077])). % 45.67/45.64 cnf(23427,plain, % 45.67/45.64 (P59(a8)), % 45.67/45.64 inference(scs_inference,[],[23408,20754])). % 45.67/45.64 cnf(23440,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)+~P26(a8)+~P33(a8)), % 45.67/45.64 inference(scs_inference,[],[23410,23427,23407,23408,23409,23411])). % 45.67/45.64 cnf(23441,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)+~P26(a8)+~P33(a8)), % 45.67/45.64 inference(scs_inference,[],[23410,23427,23407,23408,23409,23412])). % 45.67/45.64 cnf(24369,plain, % 45.67/45.64 (~P1(f37(a8))), % 45.67/45.64 inference(scs_inference,[],[4283,277,120])). % 45.67/45.64 cnf(28482,plain, % 45.67/45.64 (P26(a8)), % 45.67/45.64 inference(scs_inference,[],[36,38,58,43,41,40,88,86,11,198,297,299,298,362,378,372])). % 45.67/45.64 cnf(28490,plain, % 45.67/45.64 (P33(a8)), % 45.67/45.64 inference(scs_inference,[],[4283,4727,36,38,24369,58,43,41,40,88,86,443,439,11,198,297,299,298,362,378,372,364,376,222,267])). % 45.67/45.64 cnf(28497,plain, % 45.67/45.64 (P95(a41)+~P96(a41)+~P58(a8)), % 45.67/45.64 inference(scs_inference,[],[28482,28490,23440])). % 45.67/45.64 cnf(28498,plain, % 45.67/45.64 (P96(a41)+~P95(a41)+~P58(a8)), % 45.67/45.64 inference(scs_inference,[],[28482,28490,23441])). % 45.67/45.64 cnf(28507,plain, % 45.67/45.64 (P58(a8)), % 45.67/45.64 inference(scs_inference,[],[36,44,41,40,86,13,198,297,298,299,362])). % 45.67/45.64 cnf(28520,plain, % 45.67/45.64 (P95(a41)+~P96(a41)), % 45.67/45.64 inference(scs_inference,[],[28507,28497])). % 45.67/45.64 cnf(28521,plain, % 45.67/45.64 (P96(a41)+~P95(a41)), % 45.67/45.64 inference(scs_inference,[],[28507,28498])). % 45.67/45.64 cnf(30919,plain, % 45.67/45.64 (~P96(a41)), % 45.67/45.64 inference(scs_inference,[],[28520,196])). % 45.67/45.64 cnf(30920,plain, % 45.67/45.64 (~P95(a41)), % 45.67/45.64 inference(scs_inference,[],[30919,28521])). % 45.67/45.64 cnf(30931,plain, % 45.67/45.64 ($false), % 45.67/45.64 inference(scs_inference,[],[30919,30920,118]), % 45.67/45.64 ['proof']). % 45.67/45.70 % SZS output end Proof % 45.67/45.70 % Total time :44.960000s %------------------------------------------------------------------------------