%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYO578+1 : TPTP v8.2.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 20:27:21 EDT 2024 % Result : Theorem 16.12s 16.20s % Output : CNFRefutation 16.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO578+1 : TPTP v8.2.0. Released v5.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 09:14:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.49/0.58 start to proof:theBenchmark % 16.12/16.18 %------------------------------------------- % 16.12/16.18 % File :CSE---1.7 % 16.12/16.18 % Problem :theBenchmark % 16.12/16.18 % Transform :cnf % 16.12/16.18 % Format :tptp:raw % 16.12/16.18 % Command :java -jar mcs_scs.jar %d %s % 16.12/16.18 % 16.12/16.18 % Result :Theorem 15.470000s % 16.12/16.18 % Output :CNFRefutation 15.470000s % 16.12/16.18 %------------------------------------------- % 16.12/16.19 %------------------------------------------------------------------------------ % 16.12/16.19 % File : SYO578+1 : TPTP v8.2.0. Released v5.5.0. % 16.12/16.19 % Domain : Syntactic % 16.12/16.19 % Problem : Small buttercup theorem % 16.12/16.19 % Version : Especial. % 16.12/16.19 % English : % 16.12/16.19 % 16.12/16.19 % Refs : [Tha10] Thau (2010), Email to Geoff Sutcliffe % 16.12/16.19 % Source : TPTP % 16.12/16.19 % Names : small_entailed.txt [Tha10] % 16.12/16.19 % 16.12/16.19 % Status : Theorem % 16.12/16.19 % Rating : 0.00 v6.0.0, 0.33 v5.5.0 % 16.12/16.19 % Syntax : Number of formulae : 86 ( 12 unt; 0 def) % 16.12/16.19 % Number of atoms : 295 ( 0 equ) % 16.12/16.19 % Maximal formula atoms : 16 ( 3 avg) % 16.12/16.19 % Number of connectives : 303 ( 94 ~; 31 |; 88 &) % 16.12/16.19 % ( 1 <=>; 89 =>; 0 <=; 0 <~>) % 16.12/16.19 % Maximal formula depth : 13 ( 4 avg) % 16.12/16.19 % Maximal term depth : 1 ( 1 avg) % 16.12/16.19 % Number of predicates : 12 ( 12 usr; 0 prp; 1-1 aty) % 16.12/16.19 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 16.12/16.19 % Number of variables : 150 ( 90 !; 60 ?) % 16.12/16.19 % SPC : FOF_THM_EPR_NEQ % 16.12/16.19 % 16.12/16.19 % Comments : % 16.12/16.19 %------------------------------------------------------------------------------ % 16.12/16.19 fof(sos_01,axiom, % 16.12/16.19 ! [X0] : % 16.12/16.19 ( k04_buttercup10620(X0) % 16.12/16.19 => k04_buttercup10619(X0) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_02,axiom, % 16.12/16.19 ! [X1] : % 16.12/16.19 ( k04_buttercup10622(X1) % 16.12/16.19 => k04_buttercup10619(X1) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_03,axiom, % 16.12/16.19 ! [X2] : % 16.12/16.19 ( b48_buttercup10102(X2) % 16.12/16.19 => b48_buttercup10098(X2) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_04,axiom, % 16.12/16.19 ! [X3] : % 16.12/16.19 ( b48_buttercup10104(X3) % 16.12/16.19 => b48_buttercup10098(X3) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_05,axiom, % 16.12/16.19 ! [X4] : % 16.12/16.19 ( b48_buttercup10107(X4) % 16.12/16.19 => b48_buttercup10098(X4) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_06,axiom, % 16.12/16.19 ! [X5] : % 16.12/16.19 ( b48_buttercup10108(X5) % 16.12/16.19 => b48_buttercup10098(X5) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_07,axiom, % 16.12/16.19 ! [X6] : % 16.12/16.19 ( b48_buttercup10109(X6) % 16.12/16.19 => b48_buttercup10098(X6) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_08,axiom, % 16.12/16.19 ! [X7] : % 16.12/16.19 ( b48_buttercup10110(X7) % 16.12/16.19 => b48_buttercup10098(X7) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_09,axiom, % 16.12/16.19 ! [X8] : % 16.12/16.19 ( b48_buttercup10111(X8) % 16.12/16.19 => b48_buttercup10098(X8) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_10,axiom, % 16.12/16.19 ( ? [X9,X10,X11] : % 16.12/16.19 ( k04_buttercup10100(X9) % 16.12/16.19 & b48_buttercup10104(X9) % 16.12/16.19 & k04_buttercup10100(X10) % 16.12/16.19 & ~ b48_buttercup10104(X10) % 16.12/16.19 & ~ k04_buttercup10100(X11) % 16.12/16.19 & b48_buttercup10104(X11) ) % 16.12/16.19 | ( ! [X12] : % 16.12/16.19 ( b48_buttercup10104(X12) % 16.12/16.19 => k04_buttercup10100(X12) ) % 16.12/16.19 & ? [X13] : % 16.12/16.19 ( k04_buttercup10100(X13) % 16.12/16.19 & ~ b48_buttercup10104(X13) ) ) % 16.12/16.19 | ( ! [X14] : % 16.12/16.19 ( k04_buttercup10100(X14) % 16.12/16.19 => b48_buttercup10104(X14) ) % 16.12/16.19 & ? [X15] : % 16.12/16.19 ( b48_buttercup10104(X15) % 16.12/16.19 & ~ k04_buttercup10100(X15) ) ) % 16.12/16.19 | ! [X16] : % 16.12/16.19 ( k04_buttercup10100(X16) % 16.12/16.19 => ~ b48_buttercup10104(X16) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_11,axiom, % 16.12/16.19 ( ! [X17] : % 16.12/16.19 ( b48_buttercup10109(X17) % 16.12/16.19 => k04_buttercup10100(X17) ) % 16.12/16.19 & ? [X18] : % 16.12/16.19 ( k04_buttercup10100(X18) % 16.12/16.19 & ~ b48_buttercup10109(X18) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_12,axiom, % 16.12/16.19 ( ? [X19,X20,X21] : % 16.12/16.19 ( k04_buttercup10619(X19) % 16.12/16.19 & b48_buttercup10111(X19) % 16.12/16.19 & k04_buttercup10619(X20) % 16.12/16.19 & ~ b48_buttercup10111(X20) % 16.12/16.19 & ~ k04_buttercup10619(X21) % 16.12/16.19 & b48_buttercup10111(X21) ) % 16.12/16.19 | ( ! [X22] : % 16.12/16.19 ( b48_buttercup10111(X22) % 16.12/16.19 => k04_buttercup10619(X22) ) % 16.12/16.19 & ? [X23] : % 16.12/16.19 ( k04_buttercup10619(X23) % 16.12/16.19 & ~ b48_buttercup10111(X23) ) ) % 16.12/16.19 | ( ! [X24] : % 16.12/16.19 ( k04_buttercup10619(X24) % 16.12/16.19 => b48_buttercup10111(X24) ) % 16.12/16.19 & ? [X25] : % 16.12/16.19 ( b48_buttercup10111(X25) % 16.12/16.19 & ~ k04_buttercup10619(X25) ) ) % 16.12/16.19 | ! [X26] : % 16.12/16.19 ( k04_buttercup10619(X26) % 16.12/16.19 => ~ b48_buttercup10111(X26) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_13,axiom, % 16.12/16.19 ( ! [X27] : % 16.12/16.19 ( k04_buttercup10619(X27) % 16.12/16.19 => b48_buttercup10098(X27) ) % 16.12/16.19 & ? [X28] : % 16.12/16.19 ( b48_buttercup10098(X28) % 16.12/16.19 & ~ k04_buttercup10619(X28) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_14,axiom, % 16.12/16.19 ( ? [X29,X30,X31] : % 16.12/16.19 ( k04_buttercup10619(X29) % 16.12/16.19 & b48_buttercup10109(X29) % 16.12/16.19 & k04_buttercup10619(X30) % 16.12/16.19 & ~ b48_buttercup10109(X30) % 16.12/16.19 & ~ k04_buttercup10619(X31) % 16.12/16.19 & b48_buttercup10109(X31) ) % 16.12/16.19 | ( ! [X32] : % 16.12/16.19 ( b48_buttercup10109(X32) % 16.12/16.19 => k04_buttercup10619(X32) ) % 16.12/16.19 & ? [X33] : % 16.12/16.19 ( k04_buttercup10619(X33) % 16.12/16.19 & ~ b48_buttercup10109(X33) ) ) % 16.12/16.19 | ( ! [X34] : % 16.12/16.19 ( k04_buttercup10619(X34) % 16.12/16.19 => b48_buttercup10109(X34) ) % 16.12/16.19 & ? [X35] : % 16.12/16.19 ( b48_buttercup10109(X35) % 16.12/16.19 & ~ k04_buttercup10619(X35) ) ) % 16.12/16.19 | ! [X36] : % 16.12/16.19 ( k04_buttercup10619(X36) % 16.12/16.19 => ~ b48_buttercup10109(X36) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_15,axiom, % 16.12/16.19 ( ! [X37] : % 16.12/16.19 ( b48_buttercup10111(X37) % 16.12/16.19 => k04_buttercup10100(X37) ) % 16.12/16.19 & ? [X38] : % 16.12/16.19 ( k04_buttercup10100(X38) % 16.12/16.19 & ~ b48_buttercup10111(X38) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_16,axiom, % 16.12/16.19 ( ? [X39,X40,X41] : % 16.12/16.19 ( k04_buttercup10100(X39) % 16.12/16.19 & b48_buttercup10108(X39) % 16.12/16.19 & k04_buttercup10100(X40) % 16.12/16.19 & ~ b48_buttercup10108(X40) % 16.12/16.19 & ~ k04_buttercup10100(X41) % 16.12/16.19 & b48_buttercup10108(X41) ) % 16.12/16.19 | ( ! [X42] : % 16.12/16.19 ( b48_buttercup10108(X42) % 16.12/16.19 => k04_buttercup10100(X42) ) % 16.12/16.19 & ? [X43] : % 16.12/16.19 ( k04_buttercup10100(X43) % 16.12/16.19 & ~ b48_buttercup10108(X43) ) ) % 16.12/16.19 | ( ! [X44] : % 16.12/16.19 ( k04_buttercup10100(X44) % 16.12/16.19 => b48_buttercup10108(X44) ) % 16.12/16.19 & ? [X45] : % 16.12/16.19 ( b48_buttercup10108(X45) % 16.12/16.19 & ~ k04_buttercup10100(X45) ) ) % 16.12/16.19 | ! [X46] : % 16.12/16.19 ( k04_buttercup10100(X46) % 16.12/16.19 => ~ b48_buttercup10108(X46) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_17,axiom, % 16.12/16.19 ( ? [X47,X48,X49] : % 16.12/16.19 ( k04_buttercup10100(X47) % 16.12/16.19 & b48_buttercup10110(X47) % 16.12/16.19 & k04_buttercup10100(X48) % 16.12/16.19 & ~ b48_buttercup10110(X48) % 16.12/16.19 & ~ k04_buttercup10100(X49) % 16.12/16.19 & b48_buttercup10110(X49) ) % 16.12/16.19 | ( ! [X50] : % 16.12/16.19 ( b48_buttercup10110(X50) % 16.12/16.19 => k04_buttercup10100(X50) ) % 16.12/16.19 & ? [X51] : % 16.12/16.19 ( k04_buttercup10100(X51) % 16.12/16.19 & ~ b48_buttercup10110(X51) ) ) % 16.12/16.19 | ( ! [X52] : % 16.12/16.19 ( k04_buttercup10100(X52) % 16.12/16.19 => b48_buttercup10110(X52) ) % 16.12/16.19 & ? [X53] : % 16.12/16.19 ( b48_buttercup10110(X53) % 16.12/16.19 & ~ k04_buttercup10100(X53) ) ) % 16.12/16.19 | ! [X54] : % 16.12/16.19 ( k04_buttercup10100(X54) % 16.12/16.19 => ~ b48_buttercup10110(X54) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_18,axiom, % 16.12/16.19 ( ! [X55] : % 16.12/16.19 ( b48_buttercup10104(X55) % 16.12/16.19 => k04_buttercup10622(X55) ) % 16.12/16.19 & ? [X56] : % 16.12/16.19 ( k04_buttercup10622(X56) % 16.12/16.19 & ~ b48_buttercup10104(X56) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_19,axiom, % 16.12/16.19 ( ! [X57] : % 16.12/16.19 ( b48_buttercup10110(X57) % 16.12/16.19 => k04_buttercup10622(X57) ) % 16.12/16.19 & ? [X58] : % 16.12/16.19 ( k04_buttercup10622(X58) % 16.12/16.19 & ~ b48_buttercup10110(X58) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_20,axiom, % 16.12/16.19 ( ! [X59] : % 16.12/16.19 ( b48_buttercup10108(X59) % 16.12/16.19 => k04_buttercup10622(X59) ) % 16.12/16.19 & ? [X60] : % 16.12/16.19 ( k04_buttercup10622(X60) % 16.12/16.19 & ~ b48_buttercup10108(X60) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_21,axiom, % 16.12/16.19 ( ! [X61] : % 16.12/16.19 ( k04_buttercup10100(X61) % 16.12/16.19 => b48_buttercup10098(X61) ) % 16.12/16.19 & ? [X62] : % 16.12/16.19 ( b48_buttercup10098(X62) % 16.12/16.19 & ~ k04_buttercup10100(X62) ) ) ). % 16.12/16.19 % 16.12/16.19 fof(sos_22,axiom, % 16.12/16.19 ( ? [X63,X64,X65] : % 16.12/16.19 ( k04_buttercup10100(X63) % 16.12/16.19 & b48_buttercup10102(X63) % 16.12/16.20 & k04_buttercup10100(X64) % 16.12/16.20 & ~ b48_buttercup10102(X64) % 16.12/16.20 & ~ k04_buttercup10100(X65) % 16.12/16.20 & b48_buttercup10102(X65) ) % 16.12/16.20 | ( ! [X66] : % 16.12/16.20 ( b48_buttercup10102(X66) % 16.12/16.20 => k04_buttercup10100(X66) ) % 16.12/16.20 & ? [X67] : % 16.12/16.20 ( k04_buttercup10100(X67) % 16.12/16.20 & ~ b48_buttercup10102(X67) ) ) % 16.12/16.20 | ( ! [X68] : % 16.12/16.20 ( k04_buttercup10100(X68) % 16.12/16.20 => b48_buttercup10102(X68) ) % 16.12/16.20 & ? [X69] : % 16.12/16.20 ( b48_buttercup10102(X69) % 16.12/16.20 & ~ k04_buttercup10100(X69) ) ) % 16.12/16.20 | ! [X70] : % 16.12/16.20 ( k04_buttercup10100(X70) % 16.12/16.20 => ~ b48_buttercup10102(X70) ) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_23,axiom, % 16.12/16.20 ( ! [X71] : % 16.12/16.20 ( b48_buttercup10102(X71) % 16.12/16.20 => k04_buttercup10622(X71) ) % 16.12/16.20 & ? [X72] : % 16.12/16.20 ( k04_buttercup10622(X72) % 16.12/16.20 & ~ b48_buttercup10102(X72) ) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_24,axiom, % 16.12/16.20 ! [X73] : % 16.12/16.20 ( k04_buttercup10620(X73) % 16.12/16.20 <=> b48_buttercup10107(X73) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_25,axiom, % 16.12/16.20 ( ? [X74,X75,X76] : % 16.12/16.20 ( k04_buttercup10100(X74) % 16.12/16.20 & b48_buttercup10107(X74) % 16.12/16.20 & k04_buttercup10100(X75) % 16.12/16.20 & ~ b48_buttercup10107(X75) % 16.12/16.20 & ~ k04_buttercup10100(X76) % 16.12/16.20 & b48_buttercup10107(X76) ) % 16.12/16.20 | ( ! [X77] : % 16.12/16.20 ( b48_buttercup10107(X77) % 16.12/16.20 => k04_buttercup10100(X77) ) % 16.12/16.20 & ? [X78] : % 16.12/16.20 ( k04_buttercup10100(X78) % 16.12/16.20 & ~ b48_buttercup10107(X78) ) ) % 16.12/16.20 | ( ! [X79] : % 16.12/16.20 ( k04_buttercup10100(X79) % 16.12/16.20 => b48_buttercup10107(X79) ) % 16.12/16.20 & ? [X80] : % 16.12/16.20 ( b48_buttercup10107(X80) % 16.12/16.20 & ~ k04_buttercup10100(X80) ) ) % 16.12/16.20 | ! [X81] : % 16.12/16.20 ( k04_buttercup10100(X81) % 16.12/16.20 => ~ b48_buttercup10107(X81) ) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_26,axiom, % 16.12/16.20 ? [X82] : k04_buttercup10100(X82) ). % 16.12/16.20 % 16.12/16.20 fof(sos_27,axiom, % 16.12/16.20 ? [X83] : k04_buttercup10619(X83) ). % 16.12/16.20 % 16.12/16.20 fof(sos_28,axiom, % 16.12/16.20 ? [X84] : k04_buttercup10620(X84) ). % 16.12/16.20 % 16.12/16.20 fof(sos_29,axiom, % 16.12/16.20 ? [X85] : k04_buttercup10622(X85) ). % 16.12/16.20 % 16.12/16.20 fof(sos_30,axiom, % 16.12/16.20 ? [X86] : b48_buttercup10098(X86) ). % 16.12/16.20 % 16.12/16.20 fof(sos_31,axiom, % 16.12/16.20 ? [X87] : b48_buttercup10111(X87) ). % 16.12/16.20 % 16.12/16.20 fof(sos_32,axiom, % 16.12/16.20 ? [X88] : b48_buttercup10110(X88) ). % 16.12/16.20 % 16.12/16.20 fof(sos_33,axiom, % 16.12/16.20 ? [X89] : b48_buttercup10102(X89) ). % 16.12/16.20 % 16.12/16.20 fof(sos_34,axiom, % 16.12/16.20 ? [X90] : b48_buttercup10104(X90) ). % 16.12/16.20 % 16.12/16.20 fof(sos_35,axiom, % 16.12/16.20 ? [X91] : b48_buttercup10107(X91) ). % 16.12/16.20 % 16.12/16.20 fof(sos_36,axiom, % 16.12/16.20 ? [X92] : b48_buttercup10108(X92) ). % 16.12/16.20 % 16.12/16.20 fof(sos_37,axiom, % 16.12/16.20 ? [X93] : b48_buttercup10109(X93) ). % 16.12/16.20 % 16.12/16.20 fof(sos_38,axiom, % 16.12/16.20 ! [X94] : % 16.12/16.20 ( k04_buttercup10100(X94) % 16.12/16.20 => ~ k04_buttercup10619(X94) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_39,axiom, % 16.12/16.20 ! [X95] : % 16.12/16.20 ( k04_buttercup10620(X95) % 16.12/16.20 => ~ k04_buttercup10622(X95) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_40,axiom, % 16.12/16.20 ! [X96] : % 16.12/16.20 ( k04_buttercup10622(X96) % 16.12/16.20 => ~ k04_buttercup10620(X96) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_41,axiom, % 16.12/16.20 ! [X97] : % 16.12/16.20 ( k04_buttercup10619(X97) % 16.12/16.20 => ~ k04_buttercup10100(X97) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_42,axiom, % 16.12/16.20 ! [X98] : % 16.12/16.20 ( b48_buttercup10102(X98) % 16.12/16.20 => ~ b48_buttercup10104(X98) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_43,axiom, % 16.12/16.20 ! [X99] : % 16.12/16.20 ( b48_buttercup10102(X99) % 16.12/16.20 => ~ b48_buttercup10107(X99) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_44,axiom, % 16.12/16.20 ! [X100] : % 16.12/16.20 ( b48_buttercup10102(X100) % 16.12/16.20 => ~ b48_buttercup10108(X100) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_45,axiom, % 16.12/16.20 ! [X101] : % 16.12/16.20 ( b48_buttercup10102(X101) % 16.12/16.20 => ~ b48_buttercup10109(X101) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_46,axiom, % 16.12/16.20 ! [X102] : % 16.12/16.20 ( b48_buttercup10102(X102) % 16.12/16.20 => ~ b48_buttercup10110(X102) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_47,axiom, % 16.12/16.20 ! [X103] : % 16.12/16.20 ( b48_buttercup10102(X103) % 16.12/16.20 => ~ b48_buttercup10111(X103) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_48,axiom, % 16.12/16.20 ! [X104] : % 16.12/16.20 ( b48_buttercup10104(X104) % 16.12/16.20 => ~ b48_buttercup10102(X104) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_49,axiom, % 16.12/16.20 ! [X105] : % 16.12/16.20 ( b48_buttercup10104(X105) % 16.12/16.20 => ~ b48_buttercup10107(X105) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_50,axiom, % 16.12/16.20 ! [X106] : % 16.12/16.20 ( b48_buttercup10104(X106) % 16.12/16.20 => ~ b48_buttercup10108(X106) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_51,axiom, % 16.12/16.20 ! [X107] : % 16.12/16.20 ( b48_buttercup10104(X107) % 16.12/16.20 => ~ b48_buttercup10109(X107) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_52,axiom, % 16.12/16.20 ! [X108] : % 16.12/16.20 ( b48_buttercup10104(X108) % 16.12/16.20 => ~ b48_buttercup10110(X108) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_53,axiom, % 16.12/16.20 ! [X109] : % 16.12/16.20 ( b48_buttercup10104(X109) % 16.12/16.20 => ~ b48_buttercup10111(X109) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_54,axiom, % 16.12/16.20 ! [X110] : % 16.12/16.20 ( b48_buttercup10107(X110) % 16.12/16.20 => ~ b48_buttercup10102(X110) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_55,axiom, % 16.12/16.20 ! [X111] : % 16.12/16.20 ( b48_buttercup10107(X111) % 16.12/16.20 => ~ b48_buttercup10104(X111) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_56,axiom, % 16.12/16.20 ! [X112] : % 16.12/16.20 ( b48_buttercup10107(X112) % 16.12/16.20 => ~ b48_buttercup10108(X112) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_57,axiom, % 16.12/16.20 ! [X113] : % 16.12/16.20 ( b48_buttercup10107(X113) % 16.12/16.20 => ~ b48_buttercup10109(X113) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_58,axiom, % 16.12/16.20 ! [X114] : % 16.12/16.20 ( b48_buttercup10107(X114) % 16.12/16.20 => ~ b48_buttercup10110(X114) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_59,axiom, % 16.12/16.20 ! [X115] : % 16.12/16.20 ( b48_buttercup10107(X115) % 16.12/16.20 => ~ b48_buttercup10111(X115) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_60,axiom, % 16.12/16.20 ! [X116] : % 16.12/16.20 ( b48_buttercup10108(X116) % 16.12/16.20 => ~ b48_buttercup10102(X116) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_61,axiom, % 16.12/16.20 ! [X117] : % 16.12/16.20 ( b48_buttercup10108(X117) % 16.12/16.20 => ~ b48_buttercup10104(X117) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_62,axiom, % 16.12/16.20 ! [X118] : % 16.12/16.20 ( b48_buttercup10108(X118) % 16.12/16.20 => ~ b48_buttercup10107(X118) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_63,axiom, % 16.12/16.20 ! [X119] : % 16.12/16.20 ( b48_buttercup10108(X119) % 16.12/16.20 => ~ b48_buttercup10109(X119) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_64,axiom, % 16.12/16.20 ! [X120] : % 16.12/16.20 ( b48_buttercup10108(X120) % 16.12/16.20 => ~ b48_buttercup10110(X120) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_65,axiom, % 16.12/16.20 ! [X121] : % 16.12/16.20 ( b48_buttercup10108(X121) % 16.12/16.20 => ~ b48_buttercup10111(X121) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_66,axiom, % 16.12/16.20 ! [X122] : % 16.12/16.20 ( b48_buttercup10109(X122) % 16.12/16.20 => ~ b48_buttercup10102(X122) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_67,axiom, % 16.12/16.20 ! [X123] : % 16.12/16.20 ( b48_buttercup10109(X123) % 16.12/16.20 => ~ b48_buttercup10104(X123) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_68,axiom, % 16.12/16.20 ! [X124] : % 16.12/16.20 ( b48_buttercup10109(X124) % 16.12/16.20 => ~ b48_buttercup10107(X124) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_69,axiom, % 16.12/16.20 ! [X125] : % 16.12/16.20 ( b48_buttercup10109(X125) % 16.12/16.20 => ~ b48_buttercup10108(X125) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_70,axiom, % 16.12/16.20 ! [X126] : % 16.12/16.20 ( b48_buttercup10109(X126) % 16.12/16.20 => ~ b48_buttercup10110(X126) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_71,axiom, % 16.12/16.20 ! [X127] : % 16.12/16.20 ( b48_buttercup10109(X127) % 16.12/16.20 => ~ b48_buttercup10111(X127) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_72,axiom, % 16.12/16.20 ! [X128] : % 16.12/16.20 ( b48_buttercup10110(X128) % 16.12/16.20 => ~ b48_buttercup10102(X128) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_73,axiom, % 16.12/16.20 ! [X129] : % 16.12/16.20 ( b48_buttercup10110(X129) % 16.12/16.20 => ~ b48_buttercup10104(X129) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_74,axiom, % 16.12/16.20 ! [X130] : % 16.12/16.20 ( b48_buttercup10110(X130) % 16.12/16.20 => ~ b48_buttercup10107(X130) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_75,axiom, % 16.12/16.20 ! [X131] : % 16.12/16.20 ( b48_buttercup10110(X131) % 16.12/16.20 => ~ b48_buttercup10108(X131) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_76,axiom, % 16.12/16.20 ! [X132] : % 16.12/16.20 ( b48_buttercup10110(X132) % 16.12/16.20 => ~ b48_buttercup10109(X132) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_77,axiom, % 16.12/16.20 ! [X133] : % 16.12/16.20 ( b48_buttercup10110(X133) % 16.12/16.20 => ~ b48_buttercup10111(X133) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_78,axiom, % 16.12/16.20 ! [X134] : % 16.12/16.20 ( b48_buttercup10111(X134) % 16.12/16.20 => ~ b48_buttercup10102(X134) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_79,axiom, % 16.12/16.20 ! [X135] : % 16.12/16.20 ( b48_buttercup10111(X135) % 16.12/16.20 => ~ b48_buttercup10104(X135) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_80,axiom, % 16.12/16.20 ! [X136] : % 16.12/16.20 ( b48_buttercup10111(X136) % 16.12/16.20 => ~ b48_buttercup10107(X136) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_81,axiom, % 16.12/16.20 ! [X137] : % 16.12/16.20 ( b48_buttercup10111(X137) % 16.12/16.20 => ~ b48_buttercup10108(X137) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_82,axiom, % 16.12/16.20 ! [X138] : % 16.12/16.20 ( b48_buttercup10111(X138) % 16.12/16.20 => ~ b48_buttercup10109(X138) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_83,axiom, % 16.12/16.20 ! [X139] : % 16.12/16.20 ( b48_buttercup10111(X139) % 16.12/16.20 => ~ b48_buttercup10110(X139) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_84,axiom, % 16.12/16.20 ! [X140] : % 16.12/16.20 ( k04_buttercup10619(X140) % 16.12/16.20 => ( k04_buttercup10620(X140) % 16.12/16.20 | k04_buttercup10622(X140) ) ) ). % 16.12/16.20 % 16.12/16.20 fof(sos_85,axiom, % 16.12/16.20 ! [X141] : % 16.12/16.20 ( b48_buttercup10098(X141) % 16.12/16.20 => ( b48_buttercup10102(X141) % 16.12/16.20 | b48_buttercup10104(X141) % 16.12/16.20 | b48_buttercup10107(X141) % 16.12/16.20 | b48_buttercup10108(X141) % 16.12/16.20 | b48_buttercup10109(X141) % 16.12/16.20 | b48_buttercup10110(X141) % 16.12/16.20 | b48_buttercup10111(X141) ) ) ). % 16.12/16.20 % 16.12/16.20 fof(goals_86,conjecture, % 16.12/16.20 ( ( ! [X142] : % 16.12/16.20 ( b48_buttercup10098(X142) % 16.12/16.20 => k04_buttercup10100(X142) ) % 16.12/16.20 & ? [X143] : % 16.12/16.20 ( k04_buttercup10100(X143) % 16.12/16.20 & ~ b48_buttercup10098(X143) ) ) % 16.12/16.20 | ( ! [X144] : % 16.12/16.20 ( k04_buttercup10100(X144) % 16.12/16.20 => b48_buttercup10098(X144) ) % 16.12/16.20 & ? [X145] : % 16.12/16.20 ( b48_buttercup10098(X145) % 16.12/16.20 & ~ k04_buttercup10100(X145) ) ) % 16.12/16.20 | ? [X146,X147,X148] : % 16.12/16.20 ( k04_buttercup10100(X146) % 16.12/16.20 & b48_buttercup10098(X146) % 16.12/16.20 & k04_buttercup10100(X147) % 16.12/16.20 & ~ b48_buttercup10098(X147) % 16.12/16.20 & ~ k04_buttercup10100(X148) % 16.12/16.20 & b48_buttercup10098(X148) ) % 16.12/16.20 | ! [X149] : % 16.12/16.20 ( k04_buttercup10100(X149) % 16.12/16.20 => ~ b48_buttercup10098(X149) ) ) ). % 16.12/16.20 % 16.12/16.20 %------------------------------------------------------------------------------ % 16.12/16.20 %------------------------------------------- % 16.12/16.20 % Proof found % 16.12/16.20 % SZS status Theorem for theBenchmark % 16.12/16.20 % SZS output start Proof % 16.12/16.20 %ClaNum:487(EqnAxiom:0) % 16.12/16.20 %VarNum:617(SingletonVarNum:305) % 16.12/16.20 %MaxLitNum:8 % 16.12/16.20 %MaxfuncDepth:0 % 16.12/16.20 %SharedTerms:177 % 16.12/16.20 %goalClause: 12 22 251 275 % 16.12/16.20 %singleGoalClaCount:2 % 16.12/16.20 [1]P1(a1) % 16.12/16.20 [2]P2(a2) % 16.12/16.20 [3]P19(a3) % 16.12/16.20 [4]P19(a45) % 16.12/16.20 [5]P19(a55) % 16.12/16.20 [6]P19(a56) % 16.12/16.20 [7]P19(a4) % 16.12/16.20 [8]P3(a5) % 16.12/16.20 [9]P4(a9) % 16.12/16.20 [10]P4(a57) % 16.12/16.20 [11]P4(a6) % 16.12/16.20 [12]P4(a10) % 16.12/16.20 [13]P5(a11) % 16.12/16.20 [14]P6(a12) % 16.12/16.20 [15]P7(a13) % 16.12/16.20 [16]P8(a14) % 16.12/16.20 [17]P9(a7) % 16.12/16.20 [18]P10(a8) % 16.12/16.20 [19]P11(a15) % 16.12/16.20 [20]P11(a24) % 16.12/16.20 [21]P11(a58) % 16.12/16.20 [22]P11(a10) % 16.12/16.20 [23]~P2(a9) % 16.12/16.20 [24]~P3(a56) % 16.12/16.20 [25]~P5(a3) % 16.12/16.20 [26]~P7(a55) % 16.12/16.20 [27]~P8(a15) % 16.12/16.20 [28]~P9(a45) % 16.12/16.20 [29]~P10(a24) % 16.12/16.20 [30]~P11(a57) % 16.12/16.20 [59]~P6(x591)+P1(x591) % 16.12/16.21 [60]~P1(x601)+P2(x601) % 16.12/16.21 [61]~P19(x611)+P2(x611) % 16.12/16.21 [62]~P3(x621)+P19(x621) % 16.12/16.21 [63]~P5(x631)+P19(x631) % 16.12/16.21 [64]~P7(x641)+P19(x641) % 16.12/16.21 [65]~P9(x651)+P19(x651) % 16.12/16.21 [66]~P2(x661)+P4(x661) % 16.12/16.21 [67]~P3(x671)+P4(x671) % 16.12/16.21 [68]~P5(x681)+P4(x681) % 16.12/16.21 [69]~P6(x691)+P4(x691) % 16.12/16.21 [70]~P7(x701)+P4(x701) % 16.12/16.21 [71]~P8(x711)+P4(x711) % 16.12/16.21 [72]~P9(x721)+P4(x721) % 16.12/16.21 [73]~P10(x731)+P4(x731) % 16.12/16.21 [74]~P11(x741)+P4(x741) % 16.12/16.21 [75]~P1(x751)+P6(x751) % 16.12/16.21 [76]~P8(x761)+P11(x761) % 16.12/16.21 [77]~P10(x771)+P11(x771) % 16.12/16.21 [205]~P19(x2051)+~P1(x2051) % 16.12/16.21 [207]~P11(x2071)+~P2(x2071) % 16.12/16.21 [209]~P5(x2091)+~P3(x2091) % 16.12/16.21 [211]~P6(x2111)+~P3(x2111) % 16.12/16.21 [213]~P7(x2131)+~P3(x2131) % 16.12/16.21 [215]~P8(x2151)+~P3(x2151) % 16.12/16.21 [217]~P9(x2171)+~P3(x2171) % 16.12/16.21 [219]~P10(x2191)+~P3(x2191) % 16.12/16.21 [221]~P6(x2211)+~P5(x2211) % 16.12/16.21 [223]~P7(x2231)+~P5(x2231) % 16.12/16.21 [225]~P8(x2251)+~P5(x2251) % 16.12/16.21 [227]~P9(x2271)+~P5(x2271) % 16.12/16.21 [229]~P10(x2291)+~P5(x2291) % 16.12/16.21 [231]~P7(x2311)+~P6(x2311) % 16.12/16.21 [233]~P8(x2331)+~P6(x2331) % 16.12/16.21 [235]~P9(x2351)+~P6(x2351) % 16.12/16.21 [237]~P10(x2371)+~P6(x2371) % 16.12/16.21 [239]~P8(x2391)+~P7(x2391) % 16.12/16.21 [241]~P9(x2411)+~P7(x2411) % 16.12/16.21 [243]~P10(x2431)+~P7(x2431) % 16.12/16.21 [245]~P9(x2451)+~P8(x2451) % 16.12/16.21 [247]~P10(x2471)+~P8(x2471) % 16.12/16.21 [249]~P10(x2491)+~P9(x2491) % 16.12/16.21 [251]~P4(x2511)+P11(x2511)+P11(a17) % 16.12/16.21 [252]~P11(x2521)+~P5(x2521)+P13(a5000) % 16.12/16.21 [253]~P10(x2531)+~P2(x2531)+P12(a5000) % 16.12/16.21 [254]~P8(x2541)+~P2(x2541)+P14(a5000) % 16.12/16.21 [255]~P11(x2551)+~P7(x2551)+P16(a5000) % 16.12/16.21 [256]~P11(x2561)+~P9(x2561)+P17(a5000) % 16.12/16.21 [257]~P11(x2571)+~P3(x2571)+P15(a5000) % 16.12/16.21 [258]~P11(x2581)+~P6(x2581)+P18(a5000) % 16.12/16.21 [273]P19(x2731)+~P2(x2731)+P1(x2731) % 16.12/16.21 [275]~P4(x2751)+P11(x2751)+~P4(a17) % 16.12/16.21 [31]P2(a18)+P2(a25)+P10(a28)+~P12(a5000) % 16.12/16.21 [32]P2(a26)+P2(a25)+P10(a28)+~P12(a5000) % 16.12/16.21 [33]P2(a25)+P10(a18)+P10(a28)+~P12(a5000) % 16.12/16.21 [34]P2(a25)+P10(a27)+P10(a28)+~P12(a5000) % 16.12/16.21 [35]P2(a29)+P2(a30)+P8(a33)+~P14(a5000) % 16.12/16.21 [36]P2(a31)+P2(a30)+P8(a33)+~P14(a5000) % 16.12/16.21 [37]P2(a30)+P8(a29)+P8(a33)+~P14(a5000) % 16.12/16.21 [38]P2(a30)+P8(a32)+P8(a33)+~P14(a5000) % 16.12/16.21 [39]P3(a35)+P3(a46)+P11(a47)+~P15(a5000) % 16.12/16.21 [40]P3(a48)+P3(a46)+P11(a47)+~P15(a5000) % 16.12/16.21 [41]P3(a46)+P11(a35)+P11(a47)+~P15(a5000) % 16.12/16.21 [42]P3(a46)+P11(a49)+P11(a47)+~P15(a5000) % 16.12/16.21 [43]P5(a19)+P5(a20)+P11(a21)+~P13(a5000) % 16.12/16.21 [44]P5(a22)+P5(a20)+P11(a21)+~P13(a5000) % 16.12/16.21 [45]P5(a20)+P11(a19)+P11(a21)+~P13(a5000) % 16.12/16.21 [46]P5(a20)+P11(a23)+P11(a21)+~P13(a5000) % 16.12/16.21 [47]P6(a50)+P6(a51)+P11(a52)+~P18(a5000) % 16.12/16.21 [48]P6(a53)+P6(a51)+P11(a52)+~P18(a5000) % 16.12/16.21 [49]P6(a51)+P11(a50)+P11(a52)+~P18(a5000) % 16.12/16.21 [50]P6(a51)+P11(a54)+P11(a52)+~P18(a5000) % 16.12/16.21 [51]P7(a34)+P7(a36)+P11(a37)+~P16(a5000) % 16.12/16.21 [52]P7(a38)+P7(a36)+P11(a37)+~P16(a5000) % 16.12/16.21 [53]P7(a36)+P11(a34)+P11(a37)+~P16(a5000) % 16.12/16.21 [54]P7(a36)+P11(a39)+P11(a37)+~P16(a5000) % 16.12/16.21 [55]P9(a40)+P9(a41)+P11(a42)+~P17(a5000) % 16.12/16.21 [56]P9(a43)+P9(a41)+P11(a42)+~P17(a5000) % 16.12/16.21 [57]P9(a41)+P11(a40)+P11(a42)+~P17(a5000) % 16.12/16.21 [58]P9(a41)+P11(a44)+P11(a42)+~P17(a5000) % 16.12/16.21 [78]P2(a18)+P2(a25)+~P12(a5000)+~P2(a28) % 16.12/16.21 [79]P2(a18)+P10(a28)+~P12(a5000)+~P10(a25) % 16.12/16.21 [80]P2(a26)+P2(a25)+~P12(a5000)+~P2(a28) % 16.12/16.21 [81]P2(a26)+P10(a28)+~P12(a5000)+~P10(a25) % 16.12/16.21 [82]P2(a25)+P10(a18)+~P12(a5000)+~P2(a28) % 16.12/16.21 [83]P2(a25)+P10(a27)+~P12(a5000)+~P2(a28) % 16.12/16.21 [84]P2(a25)+P10(a28)+~P12(a5000)+~P2(a27) % 16.12/16.21 [85]P2(a25)+P10(a28)+~P12(a5000)+~P10(a26) % 16.12/16.21 [86]P2(a29)+P2(a30)+~P14(a5000)+~P2(a33) % 16.12/16.21 [87]P2(a29)+P8(a33)+~P14(a5000)+~P8(a30) % 16.12/16.21 [88]P2(a31)+P2(a30)+~P14(a5000)+~P2(a33) % 16.12/16.21 [89]P2(a31)+P8(a33)+~P14(a5000)+~P8(a30) % 16.12/16.21 [90]P2(a30)+P8(a29)+~P14(a5000)+~P2(a33) % 16.12/16.21 [91]P2(a30)+P8(a32)+~P14(a5000)+~P2(a33) % 16.12/16.21 [92]P2(a30)+P8(a33)+~P14(a5000)+~P2(a32) % 16.12/16.21 [93]P2(a30)+P8(a33)+~P14(a5000)+~P8(a31) % 16.12/16.21 [94]P3(a35)+P3(a46)+~P15(a5000)+~P3(a47) % 16.12/16.21 [95]P3(a35)+P11(a47)+~P15(a5000)+~P11(a46) % 16.12/16.21 [96]P3(a48)+P3(a46)+~P15(a5000)+~P3(a47) % 16.12/16.21 [97]P3(a48)+P11(a47)+~P15(a5000)+~P11(a46) % 16.12/16.21 [98]P3(a46)+P11(a35)+~P15(a5000)+~P3(a47) % 16.12/16.21 [99]P3(a46)+P11(a49)+~P15(a5000)+~P3(a47) % 16.12/16.21 [100]P3(a46)+P11(a47)+~P15(a5000)+~P3(a49) % 16.12/16.21 [101]P3(a46)+P11(a47)+~P15(a5000)+~P11(a48) % 16.12/16.21 [102]P5(a19)+P5(a20)+~P13(a5000)+~P5(a21) % 16.12/16.21 [103]P5(a19)+P11(a21)+~P13(a5000)+~P11(a20) % 16.12/16.21 [104]P5(a22)+P5(a20)+~P13(a5000)+~P5(a21) % 16.12/16.21 [105]P5(a22)+P11(a21)+~P13(a5000)+~P11(a20) % 16.12/16.21 [106]P5(a20)+P11(a19)+~P13(a5000)+~P5(a21) % 16.12/16.21 [107]P5(a20)+P11(a23)+~P13(a5000)+~P5(a21) % 16.12/16.21 [108]P5(a20)+P11(a21)+~P13(a5000)+~P5(a23) % 16.12/16.21 [109]P5(a20)+P11(a21)+~P13(a5000)+~P11(a22) % 16.12/16.21 [110]P6(a50)+P6(a51)+~P18(a5000)+~P6(a52) % 16.12/16.21 [111]P6(a50)+P11(a52)+~P18(a5000)+~P11(a51) % 16.12/16.21 [112]P6(a53)+P6(a51)+~P18(a5000)+~P6(a52) % 16.12/16.21 [113]P6(a53)+P11(a52)+~P18(a5000)+~P11(a51) % 16.12/16.21 [114]P6(a51)+P11(a50)+~P18(a5000)+~P6(a52) % 16.12/16.21 [115]P6(a51)+P11(a54)+~P18(a5000)+~P6(a52) % 16.12/16.21 [116]P6(a51)+P11(a52)+~P18(a5000)+~P6(a54) % 16.12/16.21 [117]P6(a51)+P11(a52)+~P18(a5000)+~P11(a53) % 16.12/16.21 [118]P7(a34)+P7(a36)+~P16(a5000)+~P7(a37) % 16.12/16.21 [119]P7(a34)+P11(a37)+~P16(a5000)+~P11(a36) % 16.12/16.21 [120]P7(a38)+P7(a36)+~P16(a5000)+~P7(a37) % 16.12/16.21 [121]P7(a38)+P11(a37)+~P16(a5000)+~P11(a36) % 16.12/16.21 [122]P7(a36)+P11(a34)+~P16(a5000)+~P7(a37) % 16.12/16.21 [123]P7(a36)+P11(a39)+~P16(a5000)+~P7(a37) % 16.12/16.21 [124]P7(a36)+P11(a37)+~P16(a5000)+~P7(a39) % 16.12/16.21 [125]P7(a36)+P11(a37)+~P16(a5000)+~P11(a38) % 16.12/16.21 [126]P8(a29)+P8(a33)+~P14(a5000)+~P8(a30) % 16.12/16.21 [127]P8(a32)+P8(a33)+~P14(a5000)+~P8(a30) % 16.12/16.21 [128]P9(a40)+P9(a41)+~P17(a5000)+~P9(a42) % 16.12/16.21 [129]P9(a40)+P11(a42)+~P17(a5000)+~P11(a41) % 16.12/16.21 [130]P9(a43)+P9(a41)+~P17(a5000)+~P9(a42) % 16.12/16.21 [131]P9(a43)+P11(a42)+~P17(a5000)+~P11(a41) % 16.12/16.21 [132]P9(a41)+P11(a40)+~P17(a5000)+~P9(a42) % 16.12/16.21 [133]P9(a41)+P11(a44)+~P17(a5000)+~P9(a42) % 16.12/16.21 [134]P9(a41)+P11(a42)+~P17(a5000)+~P9(a44) % 16.12/16.21 [135]P9(a41)+P11(a42)+~P17(a5000)+~P11(a43) % 16.12/16.21 [136]P10(a18)+P10(a28)+~P12(a5000)+~P10(a25) % 16.12/16.21 [137]P10(a27)+P10(a28)+~P12(a5000)+~P10(a25) % 16.12/16.21 [138]P11(a19)+P11(a21)+~P13(a5000)+~P11(a20) % 16.12/16.21 [139]P11(a23)+P11(a21)+~P13(a5000)+~P11(a20) % 16.12/16.21 [140]P11(a34)+P11(a37)+~P16(a5000)+~P11(a36) % 16.12/16.21 [141]P11(a39)+P11(a37)+~P16(a5000)+~P11(a36) % 16.12/16.21 [142]P11(a40)+P11(a42)+~P17(a5000)+~P11(a41) % 16.12/16.21 [143]P11(a44)+P11(a42)+~P17(a5000)+~P11(a41) % 16.12/16.21 [144]P11(a35)+P11(a47)+~P15(a5000)+~P11(a46) % 16.12/16.21 [145]P11(a49)+P11(a47)+~P15(a5000)+~P11(a46) % 16.12/16.21 [146]P11(a50)+P11(a52)+~P18(a5000)+~P11(a51) % 16.12/16.21 [147]P11(a54)+P11(a52)+~P18(a5000)+~P11(a51) % 16.12/16.21 [148]P2(a18)+~P12(a5000)+~P2(a28)+~P10(a25) % 16.12/16.21 [149]P2(a26)+~P12(a5000)+~P2(a28)+~P10(a25) % 16.12/16.21 [150]P2(a25)+~P12(a5000)+~P2(a27)+~P2(a28) % 16.12/16.21 [151]P2(a25)+~P12(a5000)+~P2(a28)+~P10(a26) % 16.12/16.21 [152]P2(a29)+~P14(a5000)+~P2(a33)+~P8(a30) % 16.12/16.21 [153]P2(a31)+~P14(a5000)+~P2(a33)+~P8(a30) % 16.12/16.21 [154]P2(a30)+~P14(a5000)+~P2(a32)+~P2(a33) % 16.12/16.21 [155]P2(a30)+~P14(a5000)+~P2(a33)+~P8(a31) % 16.12/16.21 [156]P3(a35)+~P15(a5000)+~P3(a47)+~P11(a46) % 16.12/16.21 [157]P3(a48)+~P15(a5000)+~P3(a47)+~P11(a46) % 16.12/16.21 [158]P3(a46)+~P15(a5000)+~P3(a49)+~P3(a47) % 16.12/16.21 [159]P3(a46)+~P15(a5000)+~P3(a47)+~P11(a48) % 16.12/16.21 [160]P5(a19)+~P13(a5000)+~P5(a21)+~P11(a20) % 16.12/16.21 [161]P5(a22)+~P13(a5000)+~P5(a21)+~P11(a20) % 16.12/16.21 [162]P5(a20)+~P13(a5000)+~P5(a23)+~P5(a21) % 16.12/16.21 [163]P5(a20)+~P13(a5000)+~P5(a21)+~P11(a22) % 16.12/16.21 [164]P6(a50)+~P18(a5000)+~P6(a52)+~P11(a51) % 16.12/16.21 [165]P6(a53)+~P18(a5000)+~P6(a52)+~P11(a51) % 16.12/16.21 [166]P6(a51)+~P18(a5000)+~P6(a54)+~P6(a52) % 16.12/16.21 [167]P6(a51)+~P18(a5000)+~P6(a52)+~P11(a53) % 16.12/16.21 [168]P7(a34)+~P16(a5000)+~P7(a37)+~P11(a36) % 16.12/16.21 [169]P7(a38)+~P16(a5000)+~P7(a37)+~P11(a36) % 16.12/16.21 [170]P7(a36)+~P16(a5000)+~P7(a39)+~P7(a37) % 16.12/16.21 [171]P7(a36)+~P16(a5000)+~P7(a37)+~P11(a38) % 16.12/16.21 [172]P8(a29)+~P14(a5000)+~P2(a33)+~P8(a30) % 16.12/16.21 [173]P8(a32)+~P14(a5000)+~P2(a33)+~P8(a30) % 16.12/16.21 [174]P8(a33)+~P14(a5000)+~P2(a32)+~P8(a30) % 16.12/16.21 [175]P8(a33)+~P14(a5000)+~P8(a31)+~P8(a30) % 16.12/16.21 [176]P9(a40)+~P17(a5000)+~P9(a42)+~P11(a41) % 16.12/16.21 [177]P9(a43)+~P17(a5000)+~P9(a42)+~P11(a41) % 16.12/16.21 [178]P9(a41)+~P17(a5000)+~P9(a44)+~P9(a42) % 16.12/16.21 [179]P9(a41)+~P17(a5000)+~P9(a42)+~P11(a43) % 16.12/16.21 [180]P10(a18)+~P12(a5000)+~P2(a28)+~P10(a25) % 16.12/16.21 [181]P10(a27)+~P12(a5000)+~P2(a28)+~P10(a25) % 16.12/16.21 [182]P10(a28)+~P12(a5000)+~P2(a27)+~P10(a25) % 16.12/16.21 [183]P10(a28)+~P12(a5000)+~P10(a26)+~P10(a25) % 16.12/16.21 [184]P11(a19)+~P13(a5000)+~P5(a21)+~P11(a20) % 16.12/16.21 [185]P11(a23)+~P13(a5000)+~P5(a21)+~P11(a20) % 16.12/16.21 [186]P11(a21)+~P13(a5000)+~P5(a23)+~P11(a20) % 16.12/16.21 [187]P11(a21)+~P13(a5000)+~P11(a22)+~P11(a20) % 16.12/16.21 [188]P11(a34)+~P16(a5000)+~P7(a37)+~P11(a36) % 16.12/16.21 [189]P11(a39)+~P16(a5000)+~P7(a37)+~P11(a36) % 16.12/16.21 [190]P11(a37)+~P16(a5000)+~P7(a39)+~P11(a36) % 16.12/16.21 [191]P11(a37)+~P16(a5000)+~P11(a38)+~P11(a36) % 16.12/16.21 [192]P11(a40)+~P17(a5000)+~P9(a42)+~P11(a41) % 16.12/16.21 [193]P11(a44)+~P17(a5000)+~P9(a42)+~P11(a41) % 16.12/16.21 [194]P11(a42)+~P17(a5000)+~P9(a44)+~P11(a41) % 16.12/16.21 [195]P11(a42)+~P17(a5000)+~P11(a43)+~P11(a41) % 16.12/16.21 [196]P11(a35)+~P15(a5000)+~P3(a47)+~P11(a46) % 16.12/16.21 [197]P11(a49)+~P15(a5000)+~P3(a47)+~P11(a46) % 16.12/16.21 [198]P11(a47)+~P15(a5000)+~P3(a49)+~P11(a46) % 16.12/16.21 [199]P11(a47)+~P15(a5000)+~P11(a48)+~P11(a46) % 16.12/16.21 [200]P11(a50)+~P18(a5000)+~P6(a52)+~P11(a51) % 16.12/16.21 [201]P11(a54)+~P18(a5000)+~P6(a52)+~P11(a51) % 16.12/16.21 [202]P11(a52)+~P18(a5000)+~P6(a54)+~P11(a51) % 16.12/16.21 [203]P11(a52)+~P18(a5000)+~P11(a53)+~P11(a51) % 16.12/16.21 [259]~P13(a5000)+~P5(a23)+~P5(a21)+~P11(a20) % 16.12/16.21 [260]~P13(a5000)+~P5(a21)+~P11(a22)+~P11(a20) % 16.12/16.21 [261]~P12(a5000)+~P2(a27)+~P2(a28)+~P10(a25) % 16.12/16.21 [262]~P12(a5000)+~P2(a28)+~P10(a26)+~P10(a25) % 16.12/16.21 [263]~P14(a5000)+~P2(a32)+~P2(a33)+~P8(a30) % 16.12/16.21 [264]~P14(a5000)+~P2(a33)+~P8(a31)+~P8(a30) % 16.12/16.21 [265]~P16(a5000)+~P7(a39)+~P7(a37)+~P11(a36) % 16.12/16.21 [266]~P16(a5000)+~P7(a37)+~P11(a38)+~P11(a36) % 16.12/16.21 [267]~P17(a5000)+~P9(a44)+~P9(a42)+~P11(a41) % 16.12/16.21 [268]~P17(a5000)+~P9(a42)+~P11(a43)+~P11(a41) % 16.12/16.21 [269]~P15(a5000)+~P3(a49)+~P3(a47)+~P11(a46) % 16.12/16.21 [270]~P15(a5000)+~P3(a47)+~P11(a48)+~P11(a46) % 16.12/16.21 [271]~P18(a5000)+~P6(a54)+~P6(a52)+~P11(a51) % 16.12/16.21 [272]~P18(a5000)+~P6(a52)+~P11(a53)+~P11(a51) % 16.12/16.21 [276]~P10(x2761)+P2(x2761)+P2(a18)+P10(a28)+~P12(a5000) % 16.12/16.21 [277]~P10(x2771)+P2(x2771)+P2(a26)+P10(a28)+~P12(a5000) % 16.12/16.21 [278]~P8(x2781)+P2(x2781)+P2(a29)+P8(a33)+~P14(a5000) % 16.12/16.21 [279]~P8(x2791)+P2(x2791)+P2(a31)+P8(a33)+~P14(a5000) % 16.12/16.21 [280]~P8(x2801)+P2(x2801)+P8(a29)+P8(a33)+~P14(a5000) % 16.12/16.21 [281]~P8(x2811)+P2(x2811)+P8(a32)+P8(a33)+~P14(a5000) % 16.12/16.21 [282]~P10(x2821)+P2(x2821)+P10(a18)+P10(a28)+~P12(a5000) % 16.12/16.21 [283]~P10(x2831)+P2(x2831)+P10(a27)+P10(a28)+~P12(a5000) % 16.12/16.21 [284]~P11(x2841)+P3(x2841)+P3(a35)+P11(a47)+~P15(a5000) % 16.12/16.21 [285]~P11(x2851)+P3(x2851)+P3(a48)+P11(a47)+~P15(a5000) % 16.12/16.21 [286]~P11(x2861)+P3(x2861)+P11(a35)+P11(a47)+~P15(a5000) % 16.12/16.21 [287]~P11(x2871)+P3(x2871)+P11(a49)+P11(a47)+~P15(a5000) % 16.12/16.21 [288]~P11(x2881)+P5(x2881)+P5(a19)+P11(a21)+~P13(a5000) % 16.12/16.21 [289]~P11(x2891)+P5(x2891)+P5(a22)+P11(a21)+~P13(a5000) % 16.12/16.21 [290]~P11(x2901)+P5(x2901)+P11(a19)+P11(a21)+~P13(a5000) % 16.12/16.21 [291]~P11(x2911)+P5(x2911)+P11(a23)+P11(a21)+~P13(a5000) % 16.12/16.21 [292]~P11(x2921)+P6(x2921)+P6(a50)+P11(a52)+~P18(a5000) % 16.12/16.21 [293]~P11(x2931)+P6(x2931)+P6(a53)+P11(a52)+~P18(a5000) % 16.12/16.21 [294]~P11(x2941)+P6(x2941)+P11(a50)+P11(a52)+~P18(a5000) % 16.12/16.21 [295]~P11(x2951)+P6(x2951)+P11(a54)+P11(a52)+~P18(a5000) % 16.12/16.21 [296]~P11(x2961)+P7(x2961)+P7(a34)+P11(a37)+~P16(a5000) % 16.12/16.21 [297]~P11(x2971)+P7(x2971)+P7(a38)+P11(a37)+~P16(a5000) % 16.12/16.21 [298]~P11(x2981)+P7(x2981)+P11(a34)+P11(a37)+~P16(a5000) % 16.12/16.21 [299]~P11(x2991)+P7(x2991)+P11(a39)+P11(a37)+~P16(a5000) % 16.12/16.21 [300]~P2(x3001)+P8(x3001)+P2(a29)+P2(a30)+~P14(a5000) % 16.12/16.21 [301]~P2(x3011)+P8(x3011)+P2(a31)+P2(a30)+~P14(a5000) % 16.12/16.21 [302]~P2(x3021)+P8(x3021)+P2(a30)+P8(a29)+~P14(a5000) % 16.12/16.21 [303]~P2(x3031)+P8(x3031)+P2(a30)+P8(a32)+~P14(a5000) % 16.12/16.21 [304]~P11(x3041)+P9(x3041)+P9(a40)+P11(a42)+~P17(a5000) % 16.12/16.21 [305]~P11(x3051)+P9(x3051)+P9(a43)+P11(a42)+~P17(a5000) % 16.12/16.21 [306]~P11(x3061)+P9(x3061)+P11(a40)+P11(a42)+~P17(a5000) % 16.12/16.21 [307]~P11(x3071)+P9(x3071)+P11(a44)+P11(a42)+~P17(a5000) % 16.12/16.21 [308]~P2(x3081)+P10(x3081)+P2(a18)+P2(a25)+~P12(a5000) % 16.12/16.21 [309]~P2(x3091)+P10(x3091)+P2(a26)+P2(a25)+~P12(a5000) % 16.12/16.21 [310]~P2(x3101)+P10(x3101)+P2(a25)+P10(a18)+~P12(a5000) % 16.12/16.21 [311]~P2(x3111)+P10(x3111)+P2(a25)+P10(a27)+~P12(a5000) % 16.12/16.21 [312]~P3(x3121)+P11(x3121)+P3(a35)+P3(a46)+~P15(a5000) % 16.12/16.21 [313]~P3(x3131)+P11(x3131)+P3(a48)+P3(a46)+~P15(a5000) % 16.12/16.21 [314]~P3(x3141)+P11(x3141)+P3(a46)+P11(a35)+~P15(a5000) % 16.12/16.21 [315]~P3(x3151)+P11(x3151)+P3(a46)+P11(a49)+~P15(a5000) % 16.12/16.21 [316]~P5(x3161)+P11(x3161)+P5(a19)+P5(a20)+~P13(a5000) % 16.12/16.21 [317]~P5(x3171)+P11(x3171)+P5(a22)+P5(a20)+~P13(a5000) % 16.12/16.21 [318]~P5(x3181)+P11(x3181)+P5(a20)+P11(a19)+~P13(a5000) % 16.12/16.21 [319]~P5(x3191)+P11(x3191)+P5(a20)+P11(a23)+~P13(a5000) % 16.12/16.21 [320]~P6(x3201)+P11(x3201)+P6(a50)+P6(a51)+~P18(a5000) % 16.12/16.21 [321]~P6(x3211)+P11(x3211)+P6(a53)+P6(a51)+~P18(a5000) % 16.12/16.21 [322]~P6(x3221)+P11(x3221)+P6(a51)+P11(a50)+~P18(a5000) % 16.12/16.21 [323]~P6(x3231)+P11(x3231)+P6(a51)+P11(a54)+~P18(a5000) % 16.12/16.21 [324]~P7(x3241)+P11(x3241)+P7(a34)+P7(a36)+~P16(a5000) % 16.12/16.21 [325]~P7(x3251)+P11(x3251)+P7(a38)+P7(a36)+~P16(a5000) % 16.12/16.21 [326]~P7(x3261)+P11(x3261)+P7(a36)+P11(a34)+~P16(a5000) % 16.12/16.21 [327]~P7(x3271)+P11(x3271)+P7(a36)+P11(a39)+~P16(a5000) % 16.12/16.21 [328]~P9(x3281)+P11(x3281)+P9(a40)+P9(a41)+~P17(a5000) % 16.12/16.21 [329]~P9(x3291)+P11(x3291)+P9(a43)+P9(a41)+~P17(a5000) % 16.12/16.21 [330]~P9(x3301)+P11(x3301)+P9(a41)+P11(a40)+~P17(a5000) % 16.12/16.21 [331]~P9(x3311)+P11(x3311)+P9(a41)+P11(a44)+~P17(a5000) % 16.12/16.21 [332]~P10(x3321)+P2(x3321)+P2(a18)+~P12(a5000)+~P2(a28) % 16.12/16.21 [333]~P10(x3331)+P2(x3331)+P2(a26)+~P12(a5000)+~P2(a28) % 16.12/16.21 [334]~P8(x3341)+P2(x3341)+P2(a29)+~P14(a5000)+~P2(a33) % 16.12/16.21 [335]~P8(x3351)+P2(x3351)+P2(a31)+~P14(a5000)+~P2(a33) % 16.12/16.21 [336]~P8(x3361)+P2(x3361)+P8(a29)+~P14(a5000)+~P2(a33) % 16.12/16.21 [337]~P8(x3371)+P2(x3371)+P8(a32)+~P14(a5000)+~P2(a33) % 16.12/16.21 [338]~P8(x3381)+P2(x3381)+P8(a33)+~P14(a5000)+~P2(a32) % 16.12/16.21 [339]~P8(x3391)+P2(x3391)+P8(a33)+~P14(a5000)+~P8(a31) % 16.12/16.21 [340]~P10(x3401)+P2(x3401)+P10(a18)+~P12(a5000)+~P2(a28) % 16.12/16.21 [341]~P10(x3411)+P2(x3411)+P10(a27)+~P12(a5000)+~P2(a28) % 16.12/16.21 [342]~P10(x3421)+P2(x3421)+P10(a28)+~P12(a5000)+~P2(a27) % 16.12/16.21 [343]~P10(x3431)+P2(x3431)+P10(a28)+~P12(a5000)+~P10(a26) % 16.12/16.21 [344]~P11(x3441)+P3(x3441)+P3(a35)+~P15(a5000)+~P3(a47) % 16.12/16.21 [345]~P11(x3451)+P3(x3451)+P3(a48)+~P15(a5000)+~P3(a47) % 16.12/16.21 [346]~P11(x3461)+P3(x3461)+P11(a35)+~P15(a5000)+~P3(a47) % 16.12/16.21 [347]~P11(x3471)+P3(x3471)+P11(a49)+~P15(a5000)+~P3(a47) % 16.12/16.21 [348]~P11(x3481)+P3(x3481)+P11(a47)+~P15(a5000)+~P3(a49) % 16.12/16.21 [349]~P11(x3491)+P3(x3491)+P11(a47)+~P15(a5000)+~P11(a48) % 16.12/16.21 [350]~P11(x3501)+P5(x3501)+P5(a19)+~P13(a5000)+~P5(a21) % 16.12/16.21 [351]~P11(x3511)+P5(x3511)+P5(a22)+~P13(a5000)+~P5(a21) % 16.12/16.21 [352]~P11(x3521)+P5(x3521)+P11(a19)+~P13(a5000)+~P5(a21) % 16.12/16.21 [353]~P11(x3531)+P5(x3531)+P11(a23)+~P13(a5000)+~P5(a21) % 16.12/16.21 [354]~P11(x3541)+P5(x3541)+P11(a21)+~P13(a5000)+~P5(a23) % 16.12/16.21 [355]~P11(x3551)+P5(x3551)+P11(a21)+~P13(a5000)+~P11(a22) % 16.12/16.21 [356]~P11(x3561)+P6(x3561)+P6(a50)+~P18(a5000)+~P6(a52) % 16.12/16.21 [357]~P11(x3571)+P6(x3571)+P6(a53)+~P18(a5000)+~P6(a52) % 16.12/16.21 [358]~P11(x3581)+P6(x3581)+P11(a50)+~P18(a5000)+~P6(a52) % 16.12/16.21 [359]~P11(x3591)+P6(x3591)+P11(a54)+~P18(a5000)+~P6(a52) % 16.12/16.21 [360]~P11(x3601)+P6(x3601)+P11(a52)+~P18(a5000)+~P6(a54) % 16.12/16.21 [361]~P11(x3611)+P6(x3611)+P11(a52)+~P18(a5000)+~P11(a53) % 16.12/16.21 [362]~P11(x3621)+P7(x3621)+P7(a34)+~P16(a5000)+~P7(a37) % 16.12/16.21 [363]~P11(x3631)+P7(x3631)+P7(a38)+~P16(a5000)+~P7(a37) % 16.12/16.21 [364]~P11(x3641)+P7(x3641)+P11(a34)+~P16(a5000)+~P7(a37) % 16.12/16.21 [365]~P11(x3651)+P7(x3651)+P11(a39)+~P16(a5000)+~P7(a37) % 16.12/16.21 [366]~P11(x3661)+P7(x3661)+P11(a37)+~P16(a5000)+~P7(a39) % 16.12/16.21 [367]~P11(x3671)+P7(x3671)+P11(a37)+~P16(a5000)+~P11(a38) % 16.12/16.21 [368]~P2(x3681)+P8(x3681)+P2(a29)+~P14(a5000)+~P8(a30) % 16.12/16.21 [369]~P2(x3691)+P8(x3691)+P2(a31)+~P14(a5000)+~P8(a30) % 16.12/16.21 [370]~P2(x3701)+P8(x3701)+P2(a30)+~P14(a5000)+~P2(a32) % 16.12/16.21 [371]~P2(x3711)+P8(x3711)+P2(a30)+~P14(a5000)+~P8(a31) % 16.12/16.21 [372]~P2(x3721)+P8(x3721)+P8(a29)+~P14(a5000)+~P8(a30) % 16.12/16.21 [373]~P2(x3731)+P8(x3731)+P8(a32)+~P14(a5000)+~P8(a30) % 16.12/16.21 [374]~P11(x3741)+P9(x3741)+P9(a40)+~P17(a5000)+~P9(a42) % 16.12/16.21 [375]~P11(x3751)+P9(x3751)+P9(a43)+~P17(a5000)+~P9(a42) % 16.12/16.21 [376]~P11(x3761)+P9(x3761)+P11(a40)+~P17(a5000)+~P9(a42) % 16.12/16.21 [377]~P11(x3771)+P9(x3771)+P11(a44)+~P17(a5000)+~P9(a42) % 16.12/16.21 [378]~P11(x3781)+P9(x3781)+P11(a42)+~P17(a5000)+~P9(a44) % 16.12/16.21 [379]~P11(x3791)+P9(x3791)+P11(a42)+~P17(a5000)+~P11(a43) % 16.12/16.21 [380]~P2(x3801)+P10(x3801)+P2(a18)+~P12(a5000)+~P10(a25) % 16.12/16.21 [381]~P2(x3811)+P10(x3811)+P2(a26)+~P12(a5000)+~P10(a25) % 16.12/16.21 [382]~P2(x3821)+P10(x3821)+P2(a25)+~P12(a5000)+~P2(a27) % 16.12/16.21 [383]~P2(x3831)+P10(x3831)+P2(a25)+~P12(a5000)+~P10(a26) % 16.12/16.21 [384]~P2(x3841)+P10(x3841)+P10(a18)+~P12(a5000)+~P10(a25) % 16.12/16.21 [385]~P2(x3851)+P10(x3851)+P10(a27)+~P12(a5000)+~P10(a25) % 16.12/16.21 [386]~P3(x3861)+P11(x3861)+P3(a35)+~P15(a5000)+~P11(a46) % 16.12/16.21 [387]~P3(x3871)+P11(x3871)+P3(a48)+~P15(a5000)+~P11(a46) % 16.12/16.21 [388]~P3(x3881)+P11(x3881)+P3(a46)+~P15(a5000)+~P3(a49) % 16.12/16.21 [389]~P3(x3891)+P11(x3891)+P3(a46)+~P15(a5000)+~P11(a48) % 16.12/16.21 [390]~P5(x3901)+P11(x3901)+P5(a19)+~P13(a5000)+~P11(a20) % 16.12/16.21 [391]~P5(x3911)+P11(x3911)+P5(a22)+~P13(a5000)+~P11(a20) % 16.12/16.21 [392]~P5(x3921)+P11(x3921)+P5(a20)+~P13(a5000)+~P5(a23) % 16.12/16.21 [393]~P5(x3931)+P11(x3931)+P5(a20)+~P13(a5000)+~P11(a22) % 16.12/16.21 [394]~P6(x3941)+P11(x3941)+P6(a50)+~P18(a5000)+~P11(a51) % 16.12/16.21 [395]~P6(x3951)+P11(x3951)+P6(a53)+~P18(a5000)+~P11(a51) % 16.12/16.21 [396]~P6(x3961)+P11(x3961)+P6(a51)+~P18(a5000)+~P6(a54) % 16.12/16.21 [397]~P6(x3971)+P11(x3971)+P6(a51)+~P18(a5000)+~P11(a53) % 16.12/16.21 [398]~P7(x3981)+P11(x3981)+P7(a34)+~P16(a5000)+~P11(a36) % 16.12/16.21 [399]~P7(x3991)+P11(x3991)+P7(a38)+~P16(a5000)+~P11(a36) % 16.12/16.21 [400]~P7(x4001)+P11(x4001)+P7(a36)+~P16(a5000)+~P7(a39) % 16.12/16.21 [401]~P7(x4011)+P11(x4011)+P7(a36)+~P16(a5000)+~P11(a38) % 16.12/16.21 [402]~P9(x4021)+P11(x4021)+P9(a40)+~P17(a5000)+~P11(a41) % 16.12/16.21 [403]~P9(x4031)+P11(x4031)+P9(a43)+~P17(a5000)+~P11(a41) % 16.12/16.21 [404]~P9(x4041)+P11(x4041)+P9(a41)+~P17(a5000)+~P9(a44) % 16.12/16.21 [405]~P9(x4051)+P11(x4051)+P9(a41)+~P17(a5000)+~P11(a43) % 16.12/16.21 [406]~P5(x4061)+P11(x4061)+P11(a19)+~P13(a5000)+~P11(a20) % 16.12/16.21 [407]~P5(x4071)+P11(x4071)+P11(a23)+~P13(a5000)+~P11(a20) % 16.12/16.21 [408]~P7(x4081)+P11(x4081)+P11(a34)+~P16(a5000)+~P11(a36) % 16.12/16.21 [409]~P7(x4091)+P11(x4091)+P11(a39)+~P16(a5000)+~P11(a36) % 16.12/16.21 [410]~P9(x4101)+P11(x4101)+P11(a40)+~P17(a5000)+~P11(a41) % 16.12/16.21 [411]~P9(x4111)+P11(x4111)+P11(a44)+~P17(a5000)+~P11(a41) % 16.12/16.21 [412]~P3(x4121)+P11(x4121)+P11(a35)+~P15(a5000)+~P11(a46) % 16.12/16.21 [413]~P3(x4131)+P11(x4131)+P11(a49)+~P15(a5000)+~P11(a46) % 16.12/16.21 [414]~P6(x4141)+P11(x4141)+P11(a50)+~P18(a5000)+~P11(a51) % 16.12/16.21 [415]~P6(x4151)+P11(x4151)+P11(a54)+~P18(a5000)+~P11(a51) % 16.12/16.21 [416]~P10(x4161)+P2(x4161)+~P12(a5000)+~P2(a27)+~P2(a28) % 16.12/16.21 [417]~P10(x4171)+P2(x4171)+~P12(a5000)+~P2(a28)+~P10(a26) % 16.12/16.21 [418]~P8(x4181)+P2(x4181)+~P14(a5000)+~P2(a32)+~P2(a33) % 16.12/16.21 [419]~P8(x4191)+P2(x4191)+~P14(a5000)+~P2(a33)+~P8(a31) % 16.12/16.21 [420]~P11(x4201)+P3(x4201)+~P15(a5000)+~P3(a49)+~P3(a47) % 16.12/16.21 [421]~P11(x4211)+P3(x4211)+~P15(a5000)+~P3(a47)+~P11(a48) % 16.12/16.21 [422]~P11(x4221)+P5(x4221)+~P13(a5000)+~P5(a23)+~P5(a21) % 16.12/16.21 [423]~P11(x4231)+P5(x4231)+~P13(a5000)+~P5(a21)+~P11(a22) % 16.12/16.21 [424]~P11(x4241)+P6(x4241)+~P18(a5000)+~P6(a54)+~P6(a52) % 16.12/16.21 [425]~P11(x4251)+P6(x4251)+~P18(a5000)+~P6(a52)+~P11(a53) % 16.12/16.21 [426]~P11(x4261)+P7(x4261)+~P16(a5000)+~P7(a39)+~P7(a37) % 16.12/16.21 [427]~P11(x4271)+P7(x4271)+~P16(a5000)+~P7(a37)+~P11(a38) % 16.12/16.21 [428]~P2(x4281)+P8(x4281)+~P14(a5000)+~P2(a32)+~P8(a30) % 16.12/16.21 [429]~P2(x4291)+P8(x4291)+~P14(a5000)+~P8(a31)+~P8(a30) % 16.12/16.21 [430]~P11(x4301)+P9(x4301)+~P17(a5000)+~P9(a44)+~P9(a42) % 16.12/16.21 [431]~P11(x4311)+P9(x4311)+~P17(a5000)+~P9(a42)+~P11(a43) % 16.12/16.21 [432]~P2(x4321)+P10(x4321)+~P12(a5000)+~P2(a27)+~P10(a25) % 16.12/16.21 [433]~P2(x4331)+P10(x4331)+~P12(a5000)+~P10(a26)+~P10(a25) % 16.12/16.21 [434]~P5(x4341)+P11(x4341)+~P13(a5000)+~P5(a23)+~P11(a20) % 16.12/16.21 [435]~P5(x4351)+P11(x4351)+~P13(a5000)+~P11(a22)+~P11(a20) % 16.12/16.21 [436]~P7(x4361)+P11(x4361)+~P16(a5000)+~P7(a39)+~P11(a36) % 16.12/16.21 [437]~P7(x4371)+P11(x4371)+~P16(a5000)+~P11(a38)+~P11(a36) % 16.12/16.21 [438]~P9(x4381)+P11(x4381)+~P17(a5000)+~P9(a44)+~P11(a41) % 16.12/16.21 [439]~P9(x4391)+P11(x4391)+~P17(a5000)+~P11(a43)+~P11(a41) % 16.12/16.21 [440]~P3(x4401)+P11(x4401)+~P15(a5000)+~P3(a49)+~P11(a46) % 16.12/16.21 [441]~P3(x4411)+P11(x4411)+~P15(a5000)+~P11(a48)+~P11(a46) % 16.12/16.21 [442]~P6(x4421)+P11(x4421)+~P18(a5000)+~P6(a54)+~P11(a51) % 16.12/16.21 [443]~P6(x4431)+P11(x4431)+~P18(a5000)+~P11(a53)+~P11(a51) % 16.12/16.21 [444]~P2(x4442)+~P8(x4441)+P2(x4441)+P8(x4442)+P2(a29)+~P14(a5000) % 16.12/16.21 [445]~P2(x4452)+~P8(x4451)+P2(x4451)+P8(x4452)+P2(a31)+~P14(a5000) % 16.12/16.21 [446]~P2(x4462)+~P8(x4461)+P2(x4461)+P8(x4462)+P8(a29)+~P14(a5000) % 16.12/16.21 [447]~P2(x4472)+~P8(x4471)+P2(x4471)+P8(x4472)+P8(a32)+~P14(a5000) % 16.12/16.21 [448]~P2(x4482)+~P10(x4481)+P2(x4481)+P10(x4482)+P2(a18)+~P12(a5000) % 16.12/16.21 [449]~P2(x4492)+~P10(x4491)+P2(x4491)+P10(x4492)+P2(a26)+~P12(a5000) % 16.12/16.21 [450]~P2(x4502)+~P10(x4501)+P2(x4501)+P10(x4502)+P10(a18)+~P12(a5000) % 16.12/16.21 [451]~P2(x4512)+~P10(x4511)+P2(x4511)+P10(x4512)+P10(a27)+~P12(a5000) % 16.12/16.21 [452]~P3(x4522)+~P11(x4521)+P3(x4521)+P11(x4522)+P3(a35)+~P15(a5000) % 16.12/16.21 [453]~P3(x4532)+~P11(x4531)+P3(x4531)+P11(x4532)+P3(a48)+~P15(a5000) % 16.12/16.21 [454]~P3(x4542)+~P11(x4541)+P3(x4541)+P11(x4542)+P11(a35)+~P15(a5000) % 16.12/16.21 [455]~P3(x4552)+~P11(x4551)+P3(x4551)+P11(x4552)+P11(a49)+~P15(a5000) % 16.12/16.21 [456]~P5(x4562)+~P11(x4561)+P5(x4561)+P11(x4562)+P5(a19)+~P13(a5000) % 16.12/16.21 [457]~P5(x4572)+~P11(x4571)+P5(x4571)+P11(x4572)+P5(a22)+~P13(a5000) % 16.12/16.21 [458]~P5(x4582)+~P11(x4581)+P5(x4581)+P11(x4582)+P11(a19)+~P13(a5000) % 16.12/16.21 [459]~P5(x4592)+~P11(x4591)+P5(x4591)+P11(x4592)+P11(a23)+~P13(a5000) % 16.12/16.21 [460]~P6(x4602)+~P11(x4601)+P6(x4601)+P11(x4602)+P6(a50)+~P18(a5000) % 16.12/16.21 [461]~P6(x4612)+~P11(x4611)+P6(x4611)+P11(x4612)+P6(a53)+~P18(a5000) % 16.12/16.21 [462]~P6(x4622)+~P11(x4621)+P6(x4621)+P11(x4622)+P11(a50)+~P18(a5000) % 16.12/16.21 [463]~P6(x4632)+~P11(x4631)+P6(x4631)+P11(x4632)+P11(a54)+~P18(a5000) % 16.12/16.21 [464]~P7(x4642)+~P11(x4641)+P7(x4641)+P11(x4642)+P7(a34)+~P16(a5000) % 16.12/16.21 [465]~P7(x4652)+~P11(x4651)+P7(x4651)+P11(x4652)+P7(a38)+~P16(a5000) % 16.12/16.21 [466]~P7(x4662)+~P11(x4661)+P7(x4661)+P11(x4662)+P11(a34)+~P16(a5000) % 16.12/16.21 [467]~P7(x4672)+~P11(x4671)+P7(x4671)+P11(x4672)+P11(a39)+~P16(a5000) % 16.12/16.21 [468]~P9(x4682)+~P11(x4681)+P9(x4681)+P11(x4682)+P9(a40)+~P17(a5000) % 16.12/16.21 [469]~P9(x4692)+~P11(x4691)+P9(x4691)+P11(x4692)+P9(a43)+~P17(a5000) % 16.12/16.21 [470]~P9(x4702)+~P11(x4701)+P9(x4701)+P11(x4702)+P11(a40)+~P17(a5000) % 16.12/16.21 [471]~P9(x4712)+~P11(x4711)+P9(x4711)+P11(x4712)+P11(a44)+~P17(a5000) % 16.12/16.21 [472]~P2(x4722)+~P8(x4721)+P2(x4721)+P8(x4722)+~P14(a5000)+~P2(a32) % 16.12/16.21 [473]~P2(x4732)+~P8(x4731)+P2(x4731)+P8(x4732)+~P14(a5000)+~P8(a31) % 16.12/16.21 [474]~P2(x4742)+~P10(x4741)+P2(x4741)+P10(x4742)+~P12(a5000)+~P2(a27) % 16.12/16.21 [475]~P2(x4752)+~P10(x4751)+P2(x4751)+P10(x4752)+~P12(a5000)+~P10(a26) % 16.12/16.21 [476]~P3(x4762)+~P11(x4761)+P3(x4761)+P11(x4762)+~P15(a5000)+~P3(a49) % 16.12/16.21 [477]~P3(x4772)+~P11(x4771)+P3(x4771)+P11(x4772)+~P15(a5000)+~P11(a48) % 16.12/16.21 [478]~P5(x4782)+~P11(x4781)+P5(x4781)+P11(x4782)+~P13(a5000)+~P5(a23) % 16.12/16.21 [479]~P5(x4792)+~P11(x4791)+P5(x4791)+P11(x4792)+~P13(a5000)+~P11(a22) % 16.12/16.21 [480]~P6(x4802)+~P11(x4801)+P6(x4801)+P11(x4802)+~P18(a5000)+~P6(a54) % 16.12/16.21 [481]~P6(x4812)+~P11(x4811)+P6(x4811)+P11(x4812)+~P18(a5000)+~P11(a53) % 16.12/16.21 [482]~P7(x4822)+~P11(x4821)+P7(x4821)+P11(x4822)+~P16(a5000)+~P7(a39) % 16.12/16.21 [483]~P7(x4832)+~P11(x4831)+P7(x4831)+P11(x4832)+~P16(a5000)+~P11(a38) % 16.12/16.21 [484]~P9(x4842)+~P11(x4841)+P9(x4841)+P11(x4842)+~P17(a5000)+~P9(a44) % 16.12/16.21 [485]~P9(x4852)+~P11(x4851)+P9(x4851)+P11(x4852)+~P17(a5000)+~P11(a43) % 16.12/16.21 [487]P5(x4871)+P6(x4871)+P7(x4871)+P8(x4871)+P9(x4871)+P10(x4871)+~P4(x4871)+P3(x4871) % 16.12/16.21 %EqnAxiom % 16.12/16.21 % 16.12/16.21 %------------------------------------------- % 16.12/16.21 cnf(488,plain, % 16.12/16.21 (~P11(a2)), % 16.12/16.21 inference(scs_inference,[],[2,207])). % 16.12/16.21 cnf(518,plain, % 16.12/16.21 (~P6(a11)), % 16.12/16.21 inference(scs_inference,[],[30,2,8,13,23,207,60,61,62,63,64,65,76,77,209,211,213,215,217,219,221])). % 16.12/16.21 cnf(550,plain, % 16.12/16.21 (~P19(a1)), % 16.12/16.21 inference(scs_inference,[],[30,2,1,8,13,14,15,16,17,23,207,60,61,62,63,64,65,76,77,209,211,213,215,217,219,221,223,225,227,229,231,233,235,237,239,241,243,245,247,249,75,205])). % 16.12/16.21 cnf(567,plain, % 16.12/16.21 (~P1(a11)), % 16.12/16.21 inference(scs_inference,[],[488,518,550,65,77,63,62,64,75])). % 16.12/16.21 cnf(590,plain, % 16.12/16.21 (P11(a17)), % 16.12/16.21 inference(scs_inference,[],[2,488,66,251])). % 16.12/16.21 cnf(638,plain, % 16.12/16.21 (P11(a12)+~P4(a17)), % 16.12/16.21 inference(scs_inference,[],[14,69,275])). % 16.12/16.21 cnf(718,plain, % 16.12/16.21 (P11(a12)), % 16.12/16.21 inference(scs_inference,[],[590,74,638])). % 16.12/16.21 cnf(4121,plain, % 16.12/16.21 (P1(a12)), % 16.12/16.21 inference(scs_inference,[],[14,1,75,237,233,59])). % 16.12/16.21 cnf(4140,plain, % 16.12/16.21 (P19(a13)), % 16.12/16.21 inference(scs_inference,[],[15,16,567,18,76,273,77,64])). % 16.12/16.21 cnf(4151,plain, % 16.12/16.21 ($false), % 16.12/16.21 inference(scs_inference,[],[718,4121,4140,205,60,207]), % 16.12/16.21 ['proof']). % 16.12/16.21 % SZS output end Proof % 16.12/16.21 % Total time :15.470000s %------------------------------------------------------------------------------