%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS103+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n009.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:30 EDT 2024 % Result : Unsatisfiable 1.48s 1.58s % Output : CNFRefutation 1.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS103+1 : TPTP v8.2.0. Released v3.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jun 19 14:05:53 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 1.48/1.56 %------------------------------------------- % 1.48/1.56 % File :CSE---1.7 % 1.48/1.56 % Problem :theBenchmark % 1.48/1.56 % Transform :cnf % 1.48/1.56 % Format :tptp:raw % 1.48/1.56 % Command :java -jar mcs_scs.jar %d %s % 1.48/1.56 % 1.48/1.56 % Result :Theorem 0.940000s % 1.48/1.56 % Output :CNFRefutation 0.940000s % 1.48/1.56 %------------------------------------------- % 1.48/1.57 %------------------------------------------------------------------------------ % 1.48/1.57 % File : KRS103+1 : TPTP v8.2.0. Released v3.1.0. % 1.48/1.57 % Domain : Knowledge Representation (Semantic Web) % 1.48/1.57 % Problem : A different encoding of description-logic-502 % 1.48/1.57 % Version : Especial. % 1.48/1.57 % English : % 1.48/1.57 % 1.48/1.57 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 1.48/1.57 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 1.48/1.57 % Source : [Bec03] % 1.48/1.57 % Names : inconsistent_description-logic-Manifest504 [Bec03] % 1.48/1.57 % 1.48/1.57 % Status : Unsatisfiable % 1.48/1.57 % Rating : 0.00 v3.1.0 % 1.48/1.57 % Syntax : Number of formulae : 57 ( 1 unt; 0 def) % 1.48/1.57 % Number of atoms : 203 ( 0 equ) % 1.48/1.57 % Maximal formula atoms : 4 ( 3 avg) % 1.48/1.57 % Number of connectives : 157 ( 11 ~; 90 |; 10 &) % 1.48/1.57 % ( 1 <=>; 45 =>; 0 <=; 0 <~>) % 1.48/1.57 % Maximal formula depth : 5 ( 5 avg) % 1.48/1.57 % Maximal term depth : 1 ( 1 avg) % 1.48/1.57 % Number of predicates : 23 ( 23 usr; 0 prp; 1-1 aty) % 1.48/1.57 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 1.48/1.57 % Number of variables : 56 ( 56 !; 0 ?) % 1.48/1.57 % SPC : FOF_UNS_EPR_NEQ % 1.48/1.57 % 1.48/1.57 % Comments : Sean Bechhofer says there are some errors in the encoding of % 1.48/1.57 % datatypes, so this problem may not be perfect. At least it's % 1.48/1.57 % still representative of the type of reasoning required for OWL. % 1.48/1.57 %------------------------------------------------------------------------------ % 1.48/1.57 %----Thing and Nothing % 1.48/1.57 fof(axiom_0,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cowlThing(X) % 1.48/1.57 & ~ cowlNothing(X) ) ). % 1.48/1.57 % 1.48/1.57 %----String and Integer disjoint % 1.48/1.57 fof(axiom_1,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( xsd_string(X) % 1.48/1.57 <=> ~ xsd_integer(X) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_2,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus1(X) % 1.48/1.57 | cplus9(X) % 1.48/1.57 | cminus6(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_3,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus3(X) % 1.48/1.57 | cminus5(X) % 1.48/1.57 | cminus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_4,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus3(X) % 1.48/1.57 | cplus7(X) % 1.48/1.57 | cplus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_5,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus4(X) % 1.48/1.57 | cplus6(X) % 1.48/1.57 | cplus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_6,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus3(X) % 1.48/1.57 | cminus7(X) % 1.48/1.57 | cplus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_7,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus4(X) % 1.48/1.57 | cplus5(X) % 1.48/1.57 | cplus9(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_8,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus7(X) % 1.48/1.57 | cplus9(X) % 1.48/1.57 | cminus6(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_9,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus9(X) % 1.48/1.57 | cminus4(X) % 1.48/1.57 | cminus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_10,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus3(X) % 1.48/1.57 | cminus4(X) % 1.48/1.57 | cplus6(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_11,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus4(X) % 1.48/1.57 | cplus6(X) % 1.48/1.57 | cminus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_12,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus1(X) % 1.48/1.57 | cminus4(X) % 1.48/1.57 | cplus6(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_13,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus2(X) % 1.48/1.57 | cplus5(X) % 1.48/1.57 | cplus9(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_14,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus4(X) % 1.48/1.57 | cplus2(X) % 1.48/1.57 | cplus1(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_15,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cminus3(X) % 1.48/1.57 | cplus5(X) % 1.48/1.57 | cminus8(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_16,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus6(X) % 1.48/1.57 | cminus8(X) % 1.48/1.57 | cminus7(X) ) ) ). % 1.48/1.57 % 1.48/1.57 %----Super cTest % 1.48/1.57 fof(axiom_17,axiom, % 1.48/1.57 ! [X] : % 1.48/1.57 ( cTest(X) % 1.48/1.57 => ( cplus3(X) % 1.48/1.58 | cplus4(X) % 1.48/1.58 | cplus1(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_18,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus2(X) % 1.48/1.58 | cplus6(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_19,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus2(X) % 1.48/1.58 | cplus1(X) % 1.48/1.58 | cminus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_20,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus3(X) % 1.48/1.58 | cplus2(X) % 1.48/1.58 | cplus8(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_21,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus2(X) % 1.48/1.58 | cplus4(X) % 1.48/1.58 | cminus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_22,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus2(X) % 1.48/1.58 | cplus6(X) % 1.48/1.58 | cminus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_23,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus5(X) % 1.48/1.58 | cminus7(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_24,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cminus2(X) % 1.48/1.58 | cminus5(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_25,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus3(X) % 1.48/1.58 | cplus4(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_26,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus2(X) % 1.48/1.58 | cminus5(X) % 1.48/1.58 | cminus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_27,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus4(X) % 1.48/1.58 | cminus5(X) % 1.48/1.58 | cplus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_28,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cplus3(X) % 1.48/1.58 | cplus4(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_29,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cminus3(X) % 1.48/1.58 | cminus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_30,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cplus1(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_31,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cminus8(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_32,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus3(X) % 1.48/1.58 | cminus8(X) % 1.48/1.58 | cplus9(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_33,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cminus2(X) % 1.48/1.58 | cplus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_34,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cplus9(X) % 1.48/1.58 | cplus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_35,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cminus2(X) % 1.48/1.58 | cplus3(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_36,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus1(X) % 1.48/1.58 | cplus4(X) % 1.48/1.58 | cplus2(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_37,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus2(X) % 1.48/1.58 | cminus3(X) % 1.48/1.58 | cplus1(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_38,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus3(X) % 1.48/1.58 | cplus4(X) % 1.48/1.58 | cplus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_39,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus2(X) % 1.48/1.58 | cplus3(X) % 1.48/1.58 | cminus8(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_40,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cplus3(X) % 1.48/1.58 | cminus5(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_41,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cplus4(X) % 1.48/1.58 | cplus1(X) % 1.48/1.58 | cplus7(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_42,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cminus3(X) % 1.48/1.58 | cplus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_43,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus9(X) % 1.48/1.58 | cplus1(X) % 1.48/1.58 | cminus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_44,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cplus1(X) % 1.48/1.58 | cminus6(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_45,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus4(X) % 1.48/1.58 | cplus2(X) % 1.48/1.58 | cplus8(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----Super cTest % 1.48/1.58 fof(axiom_46,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ( cTest(X) % 1.48/1.58 => ( cminus5(X) % 1.48/1.58 | cplus7(X) % 1.48/1.58 | cplus8(X) ) ) ). % 1.48/1.58 % 1.48/1.58 %----i2003_11_14_17_20_46476 % 1.48/1.58 fof(axiom_47,axiom, % 1.48/1.58 cTest(i2003_11_14_17_20_46476) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_48,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cminus8(X) % 1.48/1.58 & cplus8(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_49,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cminus9(X) % 1.48/1.58 & cplus9(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_50,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cplus4(X) % 1.48/1.58 & cminus4(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_51,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cminus7(X) % 1.48/1.58 & cplus7(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_52,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cplus3(X) % 1.48/1.58 & cminus3(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_53,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cplus5(X) % 1.48/1.58 & cminus5(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_54,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cminus2(X) % 1.48/1.58 & cplus2(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_55,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cminus1(X) % 1.48/1.58 & cplus1(X) ) ). % 1.48/1.58 % 1.48/1.58 fof(axiom_56,axiom, % 1.48/1.58 ! [X] : % 1.48/1.58 ~ ( cplus6(X) % 1.48/1.58 & cminus6(X) ) ). % 1.48/1.58 % 1.48/1.58 %------------------------------------------------------------------------------ % 1.48/1.58 %------------------------------------------- % 1.48/1.58 % Proof found % 1.48/1.58 % SZS status Theorem for theBenchmark % 1.48/1.59 % SZS output start Proof % 1.48/1.59 %ClaNum:58(EqnAxiom:0) % 1.48/1.59 %VarNum:203(SingletonVarNum:57) % 1.48/1.59 %MaxLitNum:4 % 1.48/1.59 %MaxfuncDepth:0 % 1.48/1.59 %SharedTerms:2 % 1.48/1.59 [1]P1(a1) % 1.48/1.59 [2]~P2(x21) % 1.48/1.59 [3]P13(x31)+P12(x31) % 1.48/1.59 [4]~P13(x41)+~P12(x41) % 1.48/1.59 [5]~P3(x51)+~P14(x51) % 1.48/1.59 [6]~P4(x61)+~P15(x61) % 1.48/1.59 [7]~P16(x71)+~P5(x71) % 1.48/1.59 [8]~P17(x81)+~P6(x81) % 1.48/1.59 [9]~P19(x91)+~P8(x91) % 1.48/1.59 [10]~P21(x101)+~P10(x101) % 1.48/1.59 [11]~P11(x111)+~P22(x111) % 1.48/1.59 [12]~P20(x121)+~P9(x121) % 1.48/1.59 [13]~P7(x131)+~P18(x131) % 1.48/1.59 [14]P15(x141)+P5(x141)+~P1(x141)+P14(x141) % 1.48/1.59 [15]P15(x151)+P9(x151)+~P1(x151)+P14(x151) % 1.48/1.59 [16]P5(x161)+P9(x161)+~P1(x161)+P14(x161) % 1.48/1.59 [17]P5(x171)+P4(x171)+~P1(x171)+P14(x171) % 1.48/1.59 [18]P5(x181)+P18(x181)+~P1(x181)+P14(x181) % 1.48/1.59 [19]P6(x191)+P7(x191)+~P1(x191)+P14(x191) % 1.48/1.59 [20]P22(x201)+P20(x201)+~P1(x201)+P14(x201) % 1.48/1.59 [21]P9(x211)+P18(x211)+~P1(x211)+P14(x211) % 1.48/1.59 [22]P17(x221)+P20(x221)+~P1(x221)+P14(x221) % 1.48/1.59 [23]P5(x231)+P11(x231)+~P1(x231)+P15(x231) % 1.48/1.59 [24]P10(x241)+P9(x241)+~P1(x241)+P15(x241) % 1.48/1.59 [25]P10(x251)+P17(x251)+~P1(x251)+P15(x251) % 1.48/1.59 [26]P22(x261)+P9(x261)+~P1(x261)+P15(x261) % 1.48/1.59 [27]P9(x271)+P19(x271)+~P1(x271)+P15(x271) % 1.48/1.59 [28]P16(x281)+P7(x281)+~P1(x281)+P15(x281) % 1.48/1.59 [29]P17(x291)+P20(x291)+~P1(x291)+P15(x291) % 1.48/1.59 [30]P11(x301)+P19(x301)+~P1(x301)+P15(x301) % 1.48/1.59 [31]P19(x311)+P18(x311)+~P1(x311)+P15(x311) % 1.48/1.59 [32]P20(x321)+P7(x321)+~P1(x321)+P5(x321) % 1.48/1.59 [33]P8(x331)+P10(x331)+~P1(x331)+P6(x331) % 1.48/1.59 [34]P10(x341)+P19(x341)+~P1(x341)+P6(x341) % 1.48/1.59 [35]P22(x351)+P21(x351)+~P1(x351)+P6(x351) % 1.48/1.59 [36]P21(x361)+P18(x361)+~P1(x361)+P6(x361) % 1.48/1.59 [37]P9(x371)+P16(x371)+~P1(x371)+P6(x371) % 1.48/1.59 [38]P9(x381)+P11(x381)+~P1(x381)+P6(x381) % 1.48/1.59 [39]P22(x391)+P21(x391)+~P1(x391)+P8(x391) % 1.48/1.59 [40]P16(x401)+P20(x401)+~P1(x401)+P8(x401) % 1.48/1.59 [41]P17(x411)+P4(x411)+~P1(x411)+P8(x411) % 1.48/1.59 [42]P11(x421)+P18(x421)+~P1(x421)+P8(x421) % 1.48/1.59 [43]P4(x431)+P7(x431)+~P1(x431)+P8(x431) % 1.48/1.59 [44]P9(x441)+P4(x441)+~P1(x441)+P10(x441) % 1.48/1.59 [45]P16(x451)+P11(x451)+~P1(x451)+P10(x451) % 1.48/1.59 [46]P16(x461)+P20(x461)+~P1(x461)+P10(x461) % 1.48/1.59 [47]P17(x471)+P7(x471)+~P1(x471)+P10(x471) % 1.48/1.59 [48]P4(x481)+P7(x481)+~P1(x481)+P22(x481) % 1.48/1.59 [49]P9(x491)+P16(x491)+~P1(x491)+P21(x491) % 1.48/1.59 [50]P9(x501)+P18(x501)+~P1(x501)+P21(x501) % 1.48/1.59 [51]P17(x511)+P11(x511)+~P1(x511)+P21(x511) % 1.48/1.59 [52]P16(x521)+P17(x521)+~P1(x521)+P9(x521) % 1.48/1.59 [53]P16(x531)+P3(x531)+~P1(x531)+P9(x531) % 1.48/1.59 [54]P17(x541)+P20(x541)+~P1(x541)+P16(x541) % 1.48/1.59 [55]P11(x551)+P7(x551)+~P1(x551)+P16(x551) % 1.48/1.59 [56]P4(x561)+P20(x561)+~P1(x561)+P17(x561) % 1.48/1.59 [57]P4(x571)+P7(x571)+~P1(x571)+P17(x571) % 1.48/1.59 [58]P3(x581)+P18(x581)+~P1(x581)+P20(x581) % 1.48/1.59 %EqnAxiom % 1.48/1.59 % 1.48/1.59 %------------------------------------------- % 1.48/1.59 cnf(63,plain, % 1.48/1.59 (P7(a1)+P14(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,8,19])). % 1.48/1.59 cnf(64,plain, % 1.48/1.59 (P10(a1)+P6(a1)+~P19(a1)), % 1.48/1.59 inference(scs_inference,[],[1,9,33])). % 1.48/1.59 cnf(66,plain, % 1.48/1.59 (P20(a1)+P14(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[1,11,20])). % 1.48/1.59 cnf(67,plain, % 1.48/1.59 (P14(a1)+~P20(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[1,12,15])). % 1.48/1.59 cnf(68,plain, % 1.48/1.59 (P14(a1)+~P7(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,13,18])). % 1.48/1.59 cnf(69,plain, % 1.48/1.59 (~P18(a1)+P14(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[63,13])). % 1.48/1.59 cnf(71,plain, % 1.48/1.59 (~P9(a1)+P14(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[66,12])). % 1.48/1.59 cnf(72,plain, % 1.48/1.59 (~P3(a1)+~P20(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[67,5])). % 1.48/1.59 cnf(73,plain, % 1.48/1.59 (~P3(a1)+~P7(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[68,5])). % 1.48/1.59 cnf(74,plain, % 1.48/1.59 (P14(a1)+P5(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,69,18])). % 1.48/1.59 cnf(76,plain, % 1.48/1.59 (P14(a1)+P15(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[1,71,15])). % 1.48/1.59 cnf(78,plain, % 1.48/1.59 (~P3(a1)+P15(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[76,5])). % 1.48/1.59 cnf(80,plain, % 1.48/1.59 (~P14(a1)+P9(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,53])). % 1.48/1.59 cnf(81,plain, % 1.48/1.59 (P9(a1)+P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[1,80,16])). % 1.48/1.59 cnf(82,plain, % 1.48/1.59 (~P20(a1)+P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[81,12])). % 1.48/1.59 cnf(83,plain, % 1.48/1.59 (P7(a1)+P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[1,82,32])). % 1.48/1.59 cnf(84,plain, % 1.48/1.59 (~P18(a1)+P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[83,13])). % 1.48/1.59 cnf(89,plain, % 1.48/1.59 (~P14(a1)+P18(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,58])). % 1.48/1.59 cnf(90,plain, % 1.48/1.59 (P18(a1)+P20(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[89,66])). % 1.48/1.59 cnf(91,plain, % 1.48/1.59 (~P7(a1)+P20(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[90,13])). % 1.48/1.59 cnf(92,plain, % 1.48/1.59 (P5(a1)+P20(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[1,91,32])). % 1.48/1.59 cnf(97,plain, % 1.48/1.59 (~P3(a1)+~P18(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[5,69])). % 1.48/1.59 cnf(98,plain, % 1.48/1.59 (~P3(a1)+~P9(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[5,71])). % 1.48/1.59 cnf(99,plain, % 1.48/1.59 (P4(a1)+~P3(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,17])). % 1.48/1.59 cnf(100,plain, % 1.48/1.59 (~P15(a1)+~P3(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[99,6])). % 1.48/1.59 cnf(101,plain, % 1.48/1.59 (P5(a1)+~P3(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[100,72])). % 1.48/1.59 cnf(102,plain, % 1.48/1.59 (~P16(a1)+~P3(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[101,7])). % 1.48/1.59 cnf(103,plain, % 1.48/1.59 (P18(a1)+~P3(a1)+P9(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,21])). % 1.48/1.59 cnf(106,plain, % 1.48/1.59 (P20(a1)+~P3(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,22])). % 1.48/1.59 cnf(107,plain, % 1.48/1.59 (P17(a1)+~P3(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[106,72])). % 1.48/1.59 cnf(116,plain, % 1.48/1.59 (P7(a1)+~P3(a1)+P6(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,19])). % 1.48/1.59 cnf(120,plain, % 1.48/1.59 (P9(a1)+~P3(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,15])). % 1.48/1.59 cnf(121,plain, % 1.48/1.59 (P9(a1)+P16(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[1,120,53])). % 1.48/1.59 cnf(122,plain, % 1.48/1.59 (~P20(a1)+P16(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[121,12])). % 1.48/1.59 cnf(123,plain, % 1.48/1.59 (P15(a1)+P17(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[1,122,29])). % 1.48/1.59 cnf(124,plain, % 1.48/1.59 (~P4(a1)+P17(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[123,6])). % 1.48/1.59 cnf(127,plain, % 1.48/1.59 (P18(a1)+~P3(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,5,18])). % 1.48/1.59 cnf(128,plain, % 1.48/1.59 (P18(a1)+P20(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,127,58])). % 1.48/1.59 cnf(129,plain, % 1.48/1.59 (P20(a1)+P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[128,84])). % 1.48/1.59 cnf(130,plain, % 1.48/1.59 (P5(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[129,82])). % 1.48/1.59 cnf(132,plain, % 1.48/1.59 (~P15(a1)+P10(a1)+P9(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,44])). % 1.48/1.59 cnf(133,plain, % 1.48/1.59 (P10(a1)+P9(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[132,120])). % 1.48/1.59 cnf(134,plain, % 1.48/1.59 (~P21(a1)+P9(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[133,10])). % 1.48/1.59 cnf(135,plain, % 1.48/1.59 (P16(a1)+P9(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[1,134,49])). % 1.48/1.59 cnf(136,plain, % 1.48/1.59 (P9(a1)+~P3(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[135,102])). % 1.48/1.59 cnf(137,plain, % 1.48/1.59 (~P20(a1)+~P3(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[136,98])). % 1.48/1.59 cnf(138,plain, % 1.48/1.59 (~P3(a1)+P18(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[137,90])). % 1.48/1.59 cnf(139,plain, % 1.48/1.59 (P18(a1)+P8(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[1,138,42])). % 1.48/1.59 cnf(140,plain, % 1.48/1.59 (P8(a1)+~P3(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[139,97])). % 1.48/1.59 cnf(141,plain, % 1.48/1.59 (~P19(a1)+~P3(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[140,9])). % 1.48/1.59 cnf(142,plain, % 1.48/1.59 (~P4(a1)+P14(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[6,67])). % 1.48/1.59 cnf(143,plain, % 1.48/1.59 (P14(a1)+P5(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[1,142,17])). % 1.48/1.59 cnf(156,plain, % 1.48/1.59 (~P15(a1)+P20(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,56])). % 1.48/1.59 cnf(157,plain, % 1.48/1.59 (P20(a1)+P17(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[156,123])). % 1.48/1.59 cnf(159,plain, % 1.48/1.59 (~P4(a1)+P14(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[6,76])). % 1.48/1.59 cnf(161,plain, % 1.48/1.59 (~P15(a1)+P7(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,57])). % 1.48/1.59 cnf(162,plain, % 1.48/1.59 (P7(a1)+P17(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[161,107])). % 1.48/1.59 cnf(163,plain, % 1.48/1.59 (P17(a1)+~P3(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[162,73])). % 1.48/1.59 cnf(164,plain, % 1.48/1.59 (~P3(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[163,74])). % 1.48/1.59 cnf(165,plain, % 1.48/1.59 (~P3(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[164,5])). % 1.48/1.59 cnf(166,plain, % 1.48/1.59 (~P16(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[165,7])). % 1.48/1.59 cnf(168,plain, % 1.48/1.59 (~P4(a1)+~P3(a1)+~P11(a1)), % 1.48/1.59 inference(scs_inference,[],[6,78])). % 1.48/1.59 cnf(169,plain, % 1.48/1.59 (~P15(a1)+P8(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,41])). % 1.48/1.59 cnf(170,plain, % 1.48/1.59 (P8(a1)+P17(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[169,107])). % 1.48/1.59 cnf(171,plain, % 1.48/1.59 (~P19(a1)+P17(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[170,9])). % 1.48/1.59 cnf(172,plain, % 1.48/1.59 (~P19(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[171,141])). % 1.48/1.59 cnf(173,plain, % 1.48/1.59 (P15(a1)+P11(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[1,172,30])). % 1.48/1.59 cnf(174,plain, % 1.48/1.59 (~P4(a1)+P11(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[173,6])). % 1.48/1.59 cnf(175,plain, % 1.48/1.59 (~P4(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[174,168])). % 1.48/1.59 cnf(176,plain, % 1.48/1.59 (P18(a1)+P20(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[1,175,58])). % 1.48/1.59 cnf(183,plain, % 1.48/1.59 (~P4(a1)+P9(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[6,121])). % 1.48/1.59 cnf(191,plain, % 1.48/1.59 (~P15(a1)+P7(a1)+P8(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,43])). % 1.48/1.59 cnf(192,plain, % 1.48/1.59 (P7(a1)+P16(a1)+P8(a1)), % 1.48/1.59 inference(scs_inference,[],[1,191,28])). % 1.48/1.59 cnf(196,plain, % 1.48/1.59 (~P15(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,17])). % 1.48/1.59 cnf(197,plain, % 1.48/1.59 (P11(a1)+P5(a1)+P14(a1)), % 1.48/1.59 inference(scs_inference,[],[1,196,23])). % 1.48/1.59 cnf(198,plain, % 1.48/1.59 (P14(a1)+P5(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[197,92])). % 1.48/1.59 cnf(199,plain, % 1.48/1.59 (~P16(a1)+P14(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[198,7])). % 1.48/1.59 cnf(200,plain, % 1.48/1.59 (P14(a1)+P20(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[199,157])). % 1.48/1.59 cnf(201,plain, % 1.48/1.59 (P17(a1)+P18(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[200,89])). % 1.48/1.59 cnf(202,plain, % 1.48/1.59 (~P6(a1)+P18(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[201,8])). % 1.48/1.59 cnf(203,plain, % 1.48/1.59 (P18(a1)+P21(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[1,202,36])). % 1.48/1.59 cnf(204,plain, % 1.48/1.59 (~P7(a1)+P21(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[203,13])). % 1.48/1.59 cnf(206,plain, % 1.48/1.59 (P9(a1)+~P4(a1)+P10(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,24])). % 1.48/1.59 cnf(207,plain, % 1.48/1.59 (~P20(a1)+~P4(a1)+P10(a1)), % 1.48/1.59 inference(scs_inference,[],[206,12])). % 1.48/1.59 cnf(208,plain, % 1.48/1.59 (P10(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[207,176])). % 1.48/1.59 cnf(209,plain, % 1.48/1.59 (~P21(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[208,10])). % 1.48/1.59 cnf(210,plain, % 1.48/1.59 (P18(a1)+P6(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[1,209,36])). % 1.48/1.59 cnf(211,plain, % 1.48/1.59 (~P7(a1)+P6(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[210,13])). % 1.48/1.59 cnf(212,plain, % 1.48/1.59 (P14(a1)+P6(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[1,211,19])). % 1.48/1.59 cnf(219,plain, % 1.48/1.59 (P9(a1)+~P4(a1)+P22(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,26])). % 1.48/1.59 cnf(220,plain, % 1.48/1.59 (~P20(a1)+~P4(a1)+P22(a1)), % 1.48/1.59 inference(scs_inference,[],[219,12])). % 1.48/1.59 cnf(221,plain, % 1.48/1.59 (P22(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[220,176])). % 1.48/1.59 cnf(222,plain, % 1.48/1.59 (~P11(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[221,11])). % 1.48/1.59 cnf(236,plain, % 1.48/1.59 (P11(a1)+~P4(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,23])). % 1.48/1.59 cnf(237,plain, % 1.48/1.59 (~P4(a1)+P5(a1)+P20(a1)), % 1.48/1.59 inference(scs_inference,[],[236,92])). % 1.48/1.59 cnf(238,plain, % 1.48/1.59 (P20(a1)+P17(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,237,56])). % 1.48/1.59 cnf(239,plain, % 1.48/1.59 (P17(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[238,143])). % 1.48/1.59 cnf(240,plain, % 1.48/1.59 (~P6(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[239,8])). % 1.48/1.59 cnf(241,plain, % 1.48/1.59 (P7(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,240,19])). % 1.48/1.59 cnf(242,plain, % 1.48/1.59 (~P18(a1)+P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[241,13])). % 1.48/1.59 cnf(244,plain, % 1.48/1.59 (P7(a1)+~P4(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,28])). % 1.48/1.59 cnf(257,plain, % 1.48/1.59 (P20(a1)+~P4(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[1,6,29])). % 1.48/1.59 cnf(258,plain, % 1.48/1.59 (P17(a1)+~P4(a1)+P22(a1)), % 1.48/1.59 inference(scs_inference,[],[257,220])). % 1.48/1.59 cnf(278,plain, % 1.48/1.59 (~P5(a1)+~P14(a1)+P9(a1)), % 1.48/1.59 inference(scs_inference,[],[7,80])). % 1.48/1.59 cnf(285,plain, % 1.48/1.59 (~P5(a1)+~P20(a1)+P15(a1)), % 1.48/1.59 inference(scs_inference,[],[7,122])). % 1.48/1.59 cnf(286,plain, % 1.48/1.59 (P11(a1)+P15(a1)+~P20(a1)), % 1.48/1.59 inference(scs_inference,[],[1,285,23])). % 1.48/1.59 cnf(290,plain, % 1.48/1.59 (~P5(a1)+P15(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[7,123])). % 1.48/1.59 cnf(291,plain, % 1.48/1.59 (P15(a1)+P20(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[290,238])). % 1.48/1.59 cnf(292,plain, % 1.48/1.59 (P20(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[291,156])). % 1.48/1.59 cnf(293,plain, % 1.48/1.59 (~P9(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[292,12])). % 1.48/1.59 cnf(294,plain, % 1.48/1.59 (P17(a1)+~P14(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[293,80])). % 1.48/1.59 cnf(295,plain, % 1.48/1.59 (~P6(a1)+~P14(a1)+P16(a1)), % 1.48/1.59 inference(scs_inference,[],[294,8])). % 1.48/1.59 cnf(297,plain, % 1.48/1.59 (~P5(a1)+~P4(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[7,124])). % 1.48/1.59 cnf(298,plain, % 1.48/1.59 (P17(a1)+P11(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[297,236])). % 1.48/1.59 cnf(299,plain, % 1.48/1.59 (~P6(a1)+P11(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[298,8])). % 1.48/1.59 cnf(300,plain, % 1.48/1.59 (P11(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[299,210])). % 1.48/1.59 cnf(301,plain, % 1.48/1.59 (P18(a1)+~P4(a1)+P14(a1)), % 1.48/1.59 inference(scs_inference,[],[300,159])). % 1.48/1.59 cnf(302,plain, % 1.48/1.59 (P14(a1)+P5(a1)+P18(a1)), % 1.48/1.59 inference(scs_inference,[],[1,301,17])). % 1.48/1.59 cnf(303,plain, % 1.48/1.59 (P14(a1)+P5(a1)), % 1.48/1.59 inference(scs_inference,[],[302,242])). % 1.48/1.59 cnf(304,plain, % 1.48/1.59 (~P16(a1)+P14(a1)), % 1.48/1.59 inference(scs_inference,[],[303,7])). % 1.48/1.59 cnf(306,plain, % 1.48/1.59 (~P16(a1)+P11(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[7,236])). % 1.48/1.59 cnf(307,plain, % 1.48/1.59 (P11(a1)+~P4(a1)+P9(a1)), % 1.48/1.59 inference(scs_inference,[],[306,183])). % 1.48/1.59 cnf(308,plain, % 1.48/1.59 (P9(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[307,222])). % 1.48/1.59 cnf(309,plain, % 1.48/1.59 (~P20(a1)+P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[308,12])). % 1.48/1.59 cnf(310,plain, % 1.48/1.59 (~P4(a1)+~P14(a1)+P18(a1)), % 1.48/1.59 inference(scs_inference,[],[309,89])). % 1.48/1.59 cnf(311,plain, % 1.48/1.59 (P18(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[310,301])). % 1.48/1.59 cnf(312,plain, % 1.48/1.59 (~P7(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[311,13])). % 1.48/1.59 cnf(313,plain, % 1.48/1.59 (~P4(a1)+P14(a1)+~P17(a1)), % 1.48/1.59 inference(scs_inference,[],[312,63])). % 1.48/1.59 cnf(314,plain, % 1.48/1.59 (P14(a1)+~P5(a1)+~P4(a1)), % 1.48/1.59 inference(scs_inference,[],[313,297])). % 1.48/1.59 cnf(315,plain, % 1.48/1.59 (~P4(a1)+~P5(a1)+P9(a1)), % 1.48/1.59 inference(scs_inference,[],[314,278])). % 1.48/1.59 cnf(316,plain, % 1.48/1.59 (P10(a1)+P9(a1)+~P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,315,44])). % 1.48/1.59 cnf(317,plain, % 1.48/1.59 (~P21(a1)+P9(a1)+~P5(a1)), % 1.48/1.59 inference(scs_inference,[],[316,10])). % 1.48/1.59 cnf(318,plain, % 1.48/1.59 (P16(a1)+P9(a1)+~P5(a1)), % 1.48/1.59 inference(scs_inference,[],[1,317,49])). % 1.48/1.59 cnf(319,plain, % 1.48/1.59 (P9(a1)+~P5(a1)+~P3(a1)), % 1.48/1.59 inference(scs_inference,[],[318,166])). % 1.48/1.59 cnf(320,plain, % 1.48/1.59 (~P5(a1)+~P3(a1)+P17(a1)), % 1.48/1.59 inference(scs_inference,[],[319,293])). % 1.48/1.59 cnf(321,plain, % 1.48/1.59 (~P3(a1)+P17(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[320,130])). % 1.48/1.60 cnf(322,plain, % 1.48/1.60 (P17(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[321,166])). % 1.48/1.60 cnf(323,plain, % 1.48/1.60 (~P6(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[322,8])). % 1.48/1.60 cnf(324,plain, % 1.48/1.60 (P7(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[323,116])). % 1.48/1.60 cnf(325,plain, % 1.48/1.60 (~P18(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[324,13])). % 1.48/1.60 cnf(326,plain, % 1.48/1.60 (~P3(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[325,103])). % 1.48/1.60 cnf(327,plain, % 1.48/1.60 (P9(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[1,326,53])). % 1.48/1.60 cnf(328,plain, % 1.48/1.60 (~P20(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[327,12])). % 1.48/1.60 cnf(329,plain, % 1.48/1.60 (P16(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[328,292])). % 1.48/1.60 cnf(333,plain, % 1.48/1.60 (~P5(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[7,327])). % 1.48/1.60 cnf(334,plain, % 1.48/1.60 (P9(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[333,303])). % 1.48/1.60 cnf(335,plain, % 1.48/1.60 (~P20(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[334,12])). % 1.48/1.60 cnf(336,plain, % 1.48/1.60 (P14(a1)+~P11(a1)), % 1.48/1.60 inference(scs_inference,[],[335,66])). % 1.48/1.60 cnf(337,plain, % 1.48/1.60 (~P11(a1)+~P6(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[336,295])). % 1.48/1.60 cnf(338,plain, % 1.48/1.60 (P16(a1)+~P6(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[337,299])). % 1.48/1.60 cnf(339,plain, % 1.48/1.60 (P16(a1)+P14(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[338,212])). % 1.48/1.60 cnf(340,plain, % 1.48/1.60 (P14(a1)+P11(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[339,306])). % 1.48/1.60 cnf(341,plain, % 1.48/1.60 (~P4(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[340,336])). % 1.48/1.60 cnf(342,plain, % 1.48/1.60 (P7(a1)+P8(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[1,341,43])). % 1.48/1.60 cnf(343,plain, % 1.48/1.60 (~P18(a1)+P8(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[342,13])). % 1.48/1.60 cnf(344,plain, % 1.48/1.60 (P14(a1)+P8(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[343,139])). % 1.48/1.60 cnf(345,plain, % 1.48/1.60 (~P3(a1)+P8(a1)), % 1.48/1.60 inference(scs_inference,[],[344,5])). % 1.48/1.60 cnf(346,plain, % 1.48/1.60 (P18(a1)+P20(a1)+P8(a1)), % 1.48/1.60 inference(scs_inference,[],[1,345,58])). % 1.48/1.60 cnf(347,plain, % 1.48/1.60 (P20(a1)+P8(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[346,343])). % 1.48/1.60 cnf(348,plain, % 1.48/1.60 (P8(a1)+P14(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[347,328])). % 1.48/1.60 cnf(349,plain, % 1.48/1.60 (~P19(a1)+P14(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[348,9])). % 1.48/1.60 cnf(350,plain, % 1.48/1.60 (~P19(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[349,304])). % 1.48/1.60 cnf(351,plain, % 1.48/1.60 (P6(a1)+P10(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[1,350,34])). % 1.48/1.60 cnf(352,plain, % 1.48/1.60 (~P16(a1)+~P4(a1)+P20(a1)), % 1.48/1.60 inference(scs_inference,[],[7,237])). % 1.48/1.60 cnf(353,plain, % 1.48/1.60 (P20(a1)+P7(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[352,244])). % 1.48/1.60 cnf(354,plain, % 1.48/1.60 (~P9(a1)+P7(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[353,12])). % 1.48/1.60 cnf(355,plain, % 1.48/1.60 (P7(a1)+~P4(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[354,206])). % 1.48/1.60 cnf(356,plain, % 1.48/1.60 (~P18(a1)+~P4(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[355,13])). % 1.48/1.60 cnf(357,plain, % 1.48/1.60 (P10(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[356,311])). % 1.48/1.60 cnf(358,plain, % 1.48/1.60 (~P21(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[357,10])). % 1.48/1.60 cnf(359,plain, % 1.48/1.60 (P6(a1)+P22(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[1,358,35])). % 1.48/1.60 cnf(362,plain, % 1.48/1.60 (~P5(a1)+~P20(a1)), % 1.48/1.60 inference(scs_inference,[],[7,328])). % 1.48/1.60 cnf(363,plain, % 1.48/1.60 (~P20(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[362,165])). % 1.48/1.60 cnf(364,plain, % 1.48/1.60 (~P3(a1)+P18(a1)+P21(a1)), % 1.48/1.60 inference(scs_inference,[],[363,203])). % 1.48/1.60 cnf(365,plain, % 1.48/1.60 (~P7(a1)+~P3(a1)+P21(a1)), % 1.48/1.60 inference(scs_inference,[],[364,13])). % 1.48/1.60 cnf(366,plain, % 1.48/1.60 (P21(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[365,324])). % 1.48/1.60 cnf(367,plain, % 1.48/1.60 (~P10(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[366,10])). % 1.48/1.60 cnf(368,plain, % 1.48/1.60 (~P3(a1)+P6(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[367,351])). % 1.48/1.60 cnf(369,plain, % 1.48/1.60 (P14(a1)+~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[368,323])). % 1.48/1.60 cnf(370,plain, % 1.48/1.60 (~P3(a1)), % 1.48/1.60 inference(scs_inference,[],[369,5])). % 1.48/1.60 cnf(373,plain, % 1.48/1.60 (~P5(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[7,329])). % 1.48/1.60 cnf(374,plain, % 1.48/1.60 (P11(a1)+P15(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[1,373,23])). % 1.48/1.60 cnf(375,plain, % 1.48/1.60 (~P22(a1)+P15(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[374,11])). % 1.48/1.60 cnf(376,plain, % 1.48/1.60 (P15(a1)+P17(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[375,258])). % 1.48/1.60 cnf(377,plain, % 1.48/1.60 (~P4(a1)+P7(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[376,161])). % 1.48/1.60 cnf(378,plain, % 1.48/1.60 (P7(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[1,377,57])). % 1.48/1.60 cnf(379,plain, % 1.48/1.60 (~P18(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[378,13])). % 1.48/1.60 cnf(380,plain, % 1.48/1.60 (P17(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[379,311])). % 1.48/1.60 cnf(381,plain, % 1.48/1.60 (~P6(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[380,8])). % 1.48/1.60 cnf(382,plain, % 1.48/1.60 (P22(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[381,359])). % 1.48/1.60 cnf(383,plain, % 1.48/1.60 (~P11(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[382,11])). % 1.48/1.60 cnf(384,plain, % 1.48/1.60 (P5(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[383,236])). % 1.48/1.60 cnf(385,plain, % 1.48/1.60 (~P4(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[384,333])). % 1.48/1.60 cnf(386,plain, % 1.48/1.60 (P8(a1)+P17(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[1,385,41])). % 1.48/1.60 cnf(387,plain, % 1.48/1.60 (~P19(a1)+P17(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[386,9])). % 1.48/1.60 cnf(388,plain, % 1.48/1.60 (P15(a1)+P9(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[1,387,27])). % 1.48/1.60 cnf(389,plain, % 1.48/1.60 (P15(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[388,293])). % 1.48/1.60 cnf(390,plain, % 1.48/1.60 (P17(a1)+P10(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[389,132])). % 1.48/1.60 cnf(391,plain, % 1.48/1.60 (~P6(a1)+P10(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[390,8])). % 1.48/1.60 cnf(392,plain, % 1.48/1.60 (P19(a1)+P10(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[1,391,34])). % 1.48/1.60 cnf(393,plain, % 1.48/1.60 (~P21(a1)+P19(a1)+P9(a1)), % 1.48/1.60 inference(scs_inference,[],[392,10])). % 1.48/1.60 cnf(394,plain, % 1.48/1.60 (P18(a1)+P9(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[1,393,50])). % 1.48/1.60 cnf(395,plain, % 1.48/1.60 (~P7(a1)+P9(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[394,13])). % 1.48/1.60 cnf(396,plain, % 1.48/1.60 (P9(a1)+P19(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[395,378])). % 1.48/1.60 cnf(397,plain, % 1.48/1.60 (~P20(a1)+P19(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[396,12])). % 1.48/1.60 cnf(398,plain, % 1.48/1.60 (P17(a1)+P4(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[1,397,56])). % 1.48/1.60 cnf(399,plain, % 1.48/1.60 (~P6(a1)+P4(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[398,8])). % 1.48/1.60 cnf(400,plain, % 1.48/1.60 (P19(a1)+P10(a1)+P4(a1)), % 1.48/1.60 inference(scs_inference,[],[1,399,34])). % 1.48/1.60 cnf(401,plain, % 1.48/1.60 (P19(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[400,357])). % 1.48/1.60 cnf(405,plain, % 1.48/1.60 (~P16(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[7,384])). % 1.48/1.60 cnf(406,plain, % 1.48/1.60 (~P4(a1)+~P20(a1)), % 1.48/1.60 inference(scs_inference,[],[405,328])). % 1.48/1.60 cnf(407,plain, % 1.48/1.60 (~P20(a1)+~P6(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[406,399])). % 1.48/1.60 cnf(408,plain, % 1.48/1.60 (P18(a1)+~P6(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[370,1,407,58])). % 1.48/1.60 cnf(409,plain, % 1.48/1.60 (~P7(a1)+~P6(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[408,13])). % 1.48/1.60 cnf(410,plain, % 1.48/1.60 (~P6(a1)+P19(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[409,378])). % 1.48/1.60 cnf(411,plain, % 1.48/1.60 (~P6(a1)+P19(a1)), % 1.48/1.60 inference(scs_inference,[],[410,8])). % 1.48/1.60 cnf(413,plain, % 1.48/1.60 (P7(a1)+~P16(a1)+P20(a1)), % 1.48/1.60 inference(scs_inference,[],[1,7,32])). % 1.48/1.60 cnf(414,plain, % 1.48/1.60 (~P18(a1)+~P16(a1)+P20(a1)), % 1.48/1.60 inference(scs_inference,[],[413,13])). % 1.48/1.60 cnf(415,plain, % 1.48/1.60 (P20(a1)+~P16(a1)), % 1.48/1.60 inference(scs_inference,[],[370,1,414,58])). % 1.48/1.60 cnf(475,plain, % 1.48/1.60 (~P6(a1)+P7(a1)), % 1.48/1.60 inference(scs_inference,[],[8,378])). % 1.48/1.60 cnf(476,plain, % 1.48/1.60 (P7(a1)+P10(a1)+~P19(a1)), % 1.48/1.60 inference(scs_inference,[],[475,64])). % 1.48/1.60 cnf(477,plain, % 1.48/1.60 (P7(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[476,401])). % 1.48/1.60 cnf(478,plain, % 1.48/1.60 (~P18(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[477,13])). % 1.48/1.60 cnf(479,plain, % 1.48/1.60 (P20(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[370,1,478,58])). % 1.48/1.60 cnf(480,plain, % 1.48/1.60 (~P9(a1)+P10(a1)), % 1.48/1.60 inference(scs_inference,[],[479,12])). % 1.48/1.60 cnf(481,plain, % 1.48/1.60 (~P21(a1)+~P9(a1)), % 1.48/1.60 inference(scs_inference,[],[480,10])). % 1.48/1.60 cnf(482,plain, % 1.48/1.60 (P18(a1)+P6(a1)+~P9(a1)), % 1.48/1.60 inference(scs_inference,[],[1,481,36])). % 1.48/1.60 cnf(483,plain, % 1.48/1.60 (~P7(a1)+P6(a1)+~P9(a1)), % 1.48/1.60 inference(scs_inference,[],[482,13])). % 1.48/1.60 cnf(484,plain, % 1.48/1.60 (P6(a1)+~P9(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[483,354])). % 1.48/1.60 cnf(485,plain, % 1.48/1.60 (~P9(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[484,381])). % 1.48/1.60 cnf(486,plain, % 1.48/1.60 (~P4(a1)+P16(a1)), % 1.48/1.60 inference(scs_inference,[],[485,327])). % 1.48/1.60 cnf(487,plain, % 1.48/1.60 (~P5(a1)+~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[486,7])). % 1.48/1.60 cnf(488,plain, % 1.48/1.60 (~P4(a1)), % 1.48/1.60 inference(scs_inference,[],[487,384])). % 1.48/1.60 cnf(492,plain, % 1.48/1.60 (~P19(a1)+P17(a1)), % 1.48/1.60 inference(scs_inference,[],[488,1,41,9])). % 1.48/1.60 cnf(504,plain, % 1.48/1.60 (P17(a1)+~P6(a1)), % 1.48/1.60 inference(scs_inference,[],[492,411])). % 1.48/1.60 cnf(509,plain, % 1.48/1.60 (~P6(a1)), % 1.48/1.60 inference(scs_inference,[],[504,8])). % 1.48/1.60 cnf(510,plain, % 1.48/1.60 (P10(a1)+~P19(a1)), % 1.48/1.60 inference(scs_inference,[],[509,64])). % 1.48/1.60 cnf(516,plain, % 1.48/1.60 (P10(a1)), % 1.48/1.60 inference(scs_inference,[],[510,401])). % 1.48/1.60 cnf(517,plain, % 1.48/1.60 (~P21(a1)), % 1.48/1.60 inference(scs_inference,[],[516,10])). % 1.48/1.60 cnf(521,plain, % 1.48/1.60 (~P11(a1)), % 1.48/1.60 inference(scs_inference,[],[1,509,516,10,35,11])). % 1.48/1.60 cnf(526,plain, % 1.48/1.60 (P17(a1)), % 1.48/1.60 inference(scs_inference,[],[1,509,516,10,35,11,286,38,51])). % 1.48/1.60 cnf(528,plain, % 1.48/1.60 (~P20(a1)), % 1.48/1.60 inference(scs_inference,[],[1,509,516,10,35,11,286,38,51,12])). % 1.48/1.60 cnf(530,plain, % 1.48/1.60 (~P16(a1)), % 1.48/1.60 inference(scs_inference,[],[1,509,516,10,35,11,286,38,51,12,415])). % 1.48/1.60 cnf(534,plain, % 1.48/1.60 (P7(a1)+P14(a1)), % 1.48/1.60 inference(scs_inference,[],[526,63])). % 1.48/1.60 cnf(537,plain, % 1.48/1.60 (P7(a1)+P8(a1)), % 1.48/1.60 inference(scs_inference,[],[530,192])). % 1.48/1.60 cnf(539,plain, % 1.48/1.60 (~P7(a1)), % 1.48/1.60 inference(scs_inference,[],[517,528,204])). % 1.48/1.60 cnf(561,plain, % 1.48/1.60 ($false), % 1.48/1.60 inference(scs_inference,[],[1,521,530,539,534,537,9,28,55]), % 1.48/1.60 ['proof']). % 1.48/1.60 % SZS output end Proof % 1.48/1.60 % Total time :0.940000s %------------------------------------------------------------------------------