%------------------------------------------------------------------------------ % File : lazyCoP---0.1 % Problem : PUZ037-3 : TPTP v8.1.0. Released v2.3.0. % Transfm : none % Format : tptp:raw % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % Computer : n023.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 : 600s % DateTime : Mon Jul 18 18:18:55 EDT 2022 % Result : Unsatisfiable 14.41s 2.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PUZ037-3 : TPTP v8.1.0. Released v2.3.0. % 0.04/0.13 % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % 0.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat May 28 20:05:12 EDT 2022 % 0.12/0.34 % CPUTime : % 14.41/2.19 % SZS status Unsatisfiable % 14.41/2.19 % SZS output begin IncompleteProof % 14.41/2.19 cnf(c0, axiom, % 14.41/2.19 ~state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w)). % 14.41/2.19 cnf(c1, plain, % 14.41/2.19 ~state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w), % 14.41/2.19 inference(start, [], [c0])). % 14.41/2.19 % 14.41/2.19 cnf(c2, axiom, % 14.41/2.19 state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53) | ~state(X44,X1,X2,X32,X4,X5,X20,X7,X8,X33,X21,X9,X0,X13,X14,X15,X16,X17,X18,X19,X51,X34,X22,X10,X3,X25,X26,X27,X28,X29,X30,X31,X48,X35,X23,X11,X6,X37,X38,X39,X40,X41,X42,X43,X45,X12,X46,X47,X24,X49,X50,X36,X52,X53)). % 14.41/2.19 cnf(a0, assumption, % 14.41/2.19 b = X0). % 14.41/2.19 cnf(a1, assumption, % 14.41/2.19 b = X1). % 14.41/2.19 cnf(a2, assumption, % 14.41/2.19 b = X2). % 14.41/2.19 cnf(a3, assumption, % 14.41/2.19 b = X3). % 14.41/2.19 cnf(a4, assumption, % 14.41/2.19 b = X4). % 14.41/2.19 cnf(a5, assumption, % 14.41/2.19 b = X5). % 14.41/2.19 cnf(a6, assumption, % 14.41/2.19 b = X6). % 14.41/2.19 cnf(a7, assumption, % 14.41/2.19 b = X7). % 14.41/2.19 cnf(a8, assumption, % 14.41/2.19 b = X8). % 14.41/2.19 cnf(a9, assumption, % 14.41/2.19 r = X9). % 14.41/2.19 cnf(a10, assumption, % 14.41/2.19 r = X10). % 14.41/2.19 cnf(a11, assumption, % 14.41/2.19 r = X11). % 14.41/2.19 cnf(a12, assumption, % 14.41/2.19 g = X12). % 14.41/2.19 cnf(a13, assumption, % 14.41/2.19 g = X13). % 14.41/2.19 cnf(a14, assumption, % 14.41/2.19 g = X14). % 14.41/2.19 cnf(a15, assumption, % 14.41/2.19 o = X15). % 14.41/2.19 cnf(a16, assumption, % 14.41/2.19 o = X16). % 14.41/2.19 cnf(a17, assumption, % 14.41/2.19 o = X17). % 14.41/2.19 cnf(a18, assumption, % 14.41/2.19 y = X18). % 14.41/2.19 cnf(a19, assumption, % 14.41/2.19 y = X19). % 14.41/2.19 cnf(a20, assumption, % 14.41/2.19 y = X20). % 14.41/2.19 cnf(a21, assumption, % 14.41/2.19 r = X21). % 14.41/2.19 cnf(a22, assumption, % 14.41/2.19 r = X22). % 14.41/2.19 cnf(a23, assumption, % 14.41/2.19 r = X23). % 14.41/2.19 cnf(a24, assumption, % 14.41/2.19 g = X24). % 14.41/2.19 cnf(a25, assumption, % 14.41/2.19 g = X25). % 14.41/2.19 cnf(a26, assumption, % 14.41/2.19 g = X26). % 14.41/2.19 cnf(a27, assumption, % 14.41/2.19 o = X27). % 14.41/2.19 cnf(a28, assumption, % 14.41/2.19 o = X28). % 14.41/2.19 cnf(a29, assumption, % 14.41/2.19 o = X29). % 14.41/2.19 cnf(a30, assumption, % 14.41/2.19 y = X30). % 14.41/2.19 cnf(a31, assumption, % 14.41/2.19 y = X31). % 14.41/2.19 cnf(a32, assumption, % 14.41/2.19 y = X32). % 14.41/2.19 cnf(a33, assumption, % 14.41/2.19 r = X33). % 14.41/2.19 cnf(a34, assumption, % 14.41/2.19 r = X34). % 14.41/2.19 cnf(a35, assumption, % 14.41/2.19 r = X35). % 14.41/2.19 cnf(a36, assumption, % 14.41/2.19 g = X36). % 14.41/2.19 cnf(a37, assumption, % 14.41/2.19 g = X37). % 14.41/2.19 cnf(a38, assumption, % 14.41/2.19 g = X38). % 14.41/2.19 cnf(a39, assumption, % 14.41/2.19 o = X39). % 14.41/2.19 cnf(a40, assumption, % 14.41/2.19 o = X40). % 14.41/2.19 cnf(a41, assumption, % 14.41/2.19 o = X41). % 14.41/2.19 cnf(a42, assumption, % 14.41/2.19 y = X42). % 14.41/2.19 cnf(a43, assumption, % 14.41/2.19 y = X43). % 14.41/2.19 cnf(a44, assumption, % 14.41/2.19 y = X44). % 14.41/2.19 cnf(a45, assumption, % 14.41/2.19 w = X45). % 14.41/2.19 cnf(a46, assumption, % 14.41/2.19 w = X46). % 14.41/2.19 cnf(a47, assumption, % 14.41/2.19 w = X47). % 14.41/2.19 cnf(a48, assumption, % 14.41/2.19 w = X48). % 14.41/2.19 cnf(a49, assumption, % 14.41/2.19 w = X49). % 14.41/2.19 cnf(a50, assumption, % 14.41/2.19 w = X50). % 14.41/2.19 cnf(a51, assumption, % 14.41/2.19 w = X51). % 14.41/2.19 cnf(a52, assumption, % 14.41/2.19 w = X52). % 14.41/2.19 cnf(a53, assumption, % 14.41/2.19 w = X53). % 14.41/2.19 cnf(c3, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53])], [c1, c2])). % 14.41/2.19 cnf(c4, plain, % 14.41/2.19 ~state(X44,X1,X2,X32,X4,X5,X20,X7,X8,X33,X21,X9,X0,X13,X14,X15,X16,X17,X18,X19,X51,X34,X22,X10,X3,X25,X26,X27,X28,X29,X30,X31,X48,X35,X23,X11,X6,X37,X38,X39,X40,X41,X42,X43,X45,X12,X46,X47,X24,X49,X50,X36,X52,X53), % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53])], [c1, c2])). % 14.41/2.19 % 14.41/2.19 cnf(c5, axiom, % 14.41/2.19 state(X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100,X101,X102,X103,X104,X105,X106,X107) | ~state(X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X90,X91,X92,X93,X94,X95,X96,X97,X98,X87,X88,X89,X101,X104,X107,X100,X103,X106,X99,X102,X105)). % 14.41/2.19 cnf(a54, assumption, % 14.41/2.19 X44 = X54). % 14.41/2.19 cnf(a55, assumption, % 14.41/2.19 X1 = X55). % 14.41/2.19 cnf(a56, assumption, % 14.41/2.19 X2 = X56). % 14.41/2.19 cnf(a57, assumption, % 14.41/2.19 X32 = X57). % 14.41/2.19 cnf(a58, assumption, % 14.41/2.19 X4 = X58). % 14.41/2.19 cnf(a59, assumption, % 14.41/2.19 X5 = X59). % 14.41/2.19 cnf(a60, assumption, % 14.41/2.19 X20 = X60). % 14.41/2.19 cnf(a61, assumption, % 14.41/2.19 X7 = X61). % 14.41/2.19 cnf(a62, assumption, % 14.41/2.19 X8 = X62). % 14.41/2.19 cnf(a63, assumption, % 14.41/2.19 X33 = X63). % 14.41/2.19 cnf(a64, assumption, % 14.41/2.19 X21 = X64). % 14.41/2.19 cnf(a65, assumption, % 14.41/2.19 X9 = X65). % 14.41/2.19 cnf(a66, assumption, % 14.41/2.19 X0 = X66). % 14.41/2.19 cnf(a67, assumption, % 14.41/2.19 X13 = X67). % 14.41/2.19 cnf(a68, assumption, % 14.41/2.19 X14 = X68). % 14.41/2.19 cnf(a69, assumption, % 14.41/2.19 X15 = X69). % 14.41/2.19 cnf(a70, assumption, % 14.41/2.19 X16 = X70). % 14.41/2.19 cnf(a71, assumption, % 14.41/2.19 X17 = X71). % 14.41/2.19 cnf(a72, assumption, % 14.41/2.19 X18 = X72). % 14.41/2.19 cnf(a73, assumption, % 14.41/2.19 X19 = X73). % 14.41/2.19 cnf(a74, assumption, % 14.41/2.19 X51 = X74). % 14.41/2.19 cnf(a75, assumption, % 14.41/2.19 X34 = X75). % 14.41/2.19 cnf(a76, assumption, % 14.41/2.19 X22 = X76). % 14.41/2.19 cnf(a77, assumption, % 14.41/2.19 X10 = X77). % 14.41/2.19 cnf(a78, assumption, % 14.41/2.19 X3 = X78). % 14.41/2.19 cnf(a79, assumption, % 14.41/2.19 X25 = X79). % 14.41/2.19 cnf(a80, assumption, % 14.41/2.19 X26 = X80). % 14.41/2.19 cnf(a81, assumption, % 14.41/2.19 X27 = X81). % 14.41/2.19 cnf(a82, assumption, % 14.41/2.19 X28 = X82). % 14.41/2.19 cnf(a83, assumption, % 14.41/2.19 X29 = X83). % 14.41/2.19 cnf(a84, assumption, % 14.41/2.19 X30 = X84). % 14.41/2.19 cnf(a85, assumption, % 14.41/2.19 X31 = X85). % 14.41/2.19 cnf(a86, assumption, % 14.41/2.19 X48 = X86). % 14.41/2.19 cnf(a87, assumption, % 14.41/2.19 X35 = X87). % 14.41/2.19 cnf(a88, assumption, % 14.41/2.19 X23 = X88). % 14.41/2.19 cnf(a89, assumption, % 14.41/2.19 X11 = X89). % 14.41/2.19 cnf(a90, assumption, % 14.41/2.19 X6 = X90). % 14.41/2.19 cnf(a91, assumption, % 14.41/2.19 X37 = X91). % 14.41/2.19 cnf(a92, assumption, % 14.41/2.19 X38 = X92). % 14.41/2.19 cnf(a93, assumption, % 14.41/2.19 X39 = X93). % 14.41/2.19 cnf(a94, assumption, % 14.41/2.19 X40 = X94). % 14.41/2.19 cnf(a95, assumption, % 14.41/2.19 X41 = X95). % 14.41/2.19 cnf(a96, assumption, % 14.41/2.19 X42 = X96). % 14.41/2.19 cnf(a97, assumption, % 14.41/2.19 X43 = X97). % 14.41/2.19 cnf(a98, assumption, % 14.41/2.19 X45 = X98). % 14.41/2.19 cnf(a99, assumption, % 14.41/2.19 X12 = X99). % 14.41/2.19 cnf(a100, assumption, % 14.41/2.19 X46 = X100). % 14.41/2.19 cnf(a101, assumption, % 14.41/2.19 X47 = X101). % 14.41/2.19 cnf(a102, assumption, % 14.41/2.19 X24 = X102). % 14.41/2.19 cnf(a103, assumption, % 14.41/2.19 X49 = X103). % 14.41/2.19 cnf(a104, assumption, % 14.41/2.19 X50 = X104). % 14.41/2.19 cnf(a105, assumption, % 14.41/2.19 X36 = X105). % 14.41/2.19 cnf(a106, assumption, % 14.41/2.19 X52 = X106). % 14.41/2.19 cnf(a107, assumption, % 14.41/2.19 X53 = X107). % 14.41/2.19 cnf(c6, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a54, a55, a56, a57, a58, a59, a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99, a100, a101, a102, a103, a104, a105, a106, a107])], [c4, c5])). % 14.41/2.19 cnf(c7, plain, % 14.41/2.19 ~state(X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X90,X91,X92,X93,X94,X95,X96,X97,X98,X87,X88,X89,X101,X104,X107,X100,X103,X106,X99,X102,X105), % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a54, a55, a56, a57, a58, a59, a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99, a100, a101, a102, a103, a104, a105, a106, a107])], [c4, c5])). % 14.41/2.19 % 14.41/2.19 cnf(c8, axiom, % 14.41/2.19 state(X108,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119,X120,X121,X122,X123,X124,X125,X126,X127,X128,X129,X130,X131,X132,X133,X134,X135,X136,X137,X138,X139,X140,X141,X142,X143,X144,X145,X146,X147,X148,X149,X150,X151,X152,X153,X154,X155,X156,X157,X158,X159,X160,X161) | ~state(X141,X129,X117,X111,X112,X113,X114,X115,X116,X159,X118,X119,X120,X121,X122,X123,X124,X108,X128,X140,X152,X160,X130,X131,X132,X133,X134,X135,X136,X109,X127,X139,X151,X161,X142,X143,X144,X145,X146,X147,X148,X110,X126,X138,X150,X153,X154,X155,X156,X157,X158,X149,X137,X125)). % 14.41/2.19 cnf(a108, assumption, % 14.41/2.19 X54 = X108). % 14.41/2.19 cnf(a109, assumption, % 14.41/2.19 X55 = X109). % 14.41/2.19 cnf(a110, assumption, % 14.41/2.19 X56 = X110). % 14.41/2.19 cnf(a111, assumption, % 14.41/2.19 X57 = X111). % 14.41/2.19 cnf(a112, assumption, % 14.41/2.19 X58 = X112). % 14.41/2.19 cnf(a113, assumption, % 14.41/2.19 X59 = X113). % 14.41/2.19 cnf(a114, assumption, % 14.41/2.19 X60 = X114). % 14.41/2.19 cnf(a115, assumption, % 14.41/2.19 X61 = X115). % 14.41/2.19 cnf(a116, assumption, % 14.41/2.19 X62 = X116). % 14.41/2.19 cnf(a117, assumption, % 14.41/2.19 X63 = X117). % 14.41/2.19 cnf(a118, assumption, % 14.41/2.19 X64 = X118). % 14.41/2.19 cnf(a119, assumption, % 14.41/2.19 X65 = X119). % 14.41/2.19 cnf(a120, assumption, % 14.41/2.19 X66 = X120). % 14.41/2.19 cnf(a121, assumption, % 14.41/2.19 X67 = X121). % 14.41/2.19 cnf(a122, assumption, % 14.41/2.19 X68 = X122). % 14.41/2.19 cnf(a123, assumption, % 14.41/2.19 X69 = X123). % 14.41/2.19 cnf(a124, assumption, % 14.41/2.19 X70 = X124). % 14.41/2.19 cnf(a125, assumption, % 14.41/2.19 X71 = X125). % 14.41/2.19 cnf(a126, assumption, % 14.41/2.19 X72 = X126). % 14.41/2.19 cnf(a127, assumption, % 14.41/2.19 X73 = X127). % 14.41/2.19 cnf(a128, assumption, % 14.41/2.19 X74 = X128). % 14.41/2.19 cnf(a129, assumption, % 14.41/2.19 X75 = X129). % 14.41/2.19 cnf(a130, assumption, % 14.41/2.19 X76 = X130). % 14.41/2.19 cnf(a131, assumption, % 14.41/2.19 X77 = X131). % 14.41/2.19 cnf(a132, assumption, % 14.41/2.19 X78 = X132). % 14.41/2.19 cnf(a133, assumption, % 14.41/2.19 X79 = X133). % 14.41/2.19 cnf(a134, assumption, % 14.41/2.19 X80 = X134). % 14.41/2.19 cnf(a135, assumption, % 14.41/2.19 X81 = X135). % 14.41/2.19 cnf(a136, assumption, % 14.41/2.19 X82 = X136). % 14.41/2.19 cnf(a137, assumption, % 14.41/2.19 X83 = X137). % 14.41/2.19 cnf(a138, assumption, % 14.41/2.19 X84 = X138). % 14.41/2.19 cnf(a139, assumption, % 14.41/2.19 X85 = X139). % 14.41/2.19 cnf(a140, assumption, % 14.41/2.19 X86 = X140). % 14.41/2.19 cnf(a141, assumption, % 14.41/2.19 X90 = X141). % 14.41/2.19 cnf(a142, assumption, % 14.41/2.19 X91 = X142). % 14.41/2.19 cnf(a143, assumption, % 14.41/2.19 X92 = X143). % 14.41/2.19 cnf(a144, assumption, % 14.41/2.19 X93 = X144). % 14.41/2.19 cnf(a145, assumption, % 14.41/2.19 X94 = X145). % 14.41/2.19 cnf(a146, assumption, % 14.41/2.19 X95 = X146). % 14.41/2.19 cnf(a147, assumption, % 14.41/2.19 X96 = X147). % 14.41/2.19 cnf(a148, assumption, % 14.41/2.19 X97 = X148). % 14.41/2.19 cnf(a149, assumption, % 14.41/2.19 X98 = X149). % 14.41/2.19 cnf(a150, assumption, % 14.41/2.19 X87 = X150). % 14.41/2.19 cnf(a151, assumption, % 14.41/2.19 X88 = X151). % 14.41/2.19 cnf(a152, assumption, % 14.41/2.19 X89 = X152). % 14.41/2.19 cnf(a153, assumption, % 14.41/2.19 X101 = X153). % 14.41/2.19 cnf(a154, assumption, % 14.41/2.19 X104 = X154). % 14.41/2.19 cnf(a155, assumption, % 14.41/2.19 X107 = X155). % 14.41/2.19 cnf(a156, assumption, % 14.41/2.19 X100 = X156). % 14.41/2.19 cnf(a157, assumption, % 14.41/2.19 X103 = X157). % 14.41/2.19 cnf(a158, assumption, % 14.41/2.19 X106 = X158). % 14.41/2.19 cnf(a159, assumption, % 14.41/2.19 X99 = X159). % 14.41/2.19 cnf(a160, assumption, % 14.41/2.19 X102 = X160). % 14.41/2.19 cnf(a161, assumption, % 14.41/2.19 X105 = X161). % 14.41/2.19 cnf(c9, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119, a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139, a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159, a160, a161])], [c7, c8])). % 14.41/2.19 cnf(c10, plain, % 14.41/2.19 ~state(X141,X129,X117,X111,X112,X113,X114,X115,X116,X159,X118,X119,X120,X121,X122,X123,X124,X108,X128,X140,X152,X160,X130,X131,X132,X133,X134,X135,X136,X109,X127,X139,X151,X161,X142,X143,X144,X145,X146,X147,X148,X110,X126,X138,X150,X153,X154,X155,X156,X157,X158,X149,X137,X125), % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119, a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139, a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159, a160, a161])], [c7, c8])). % 14.41/2.19 % 14.41/2.19 cnf(c11, axiom, % 14.41/2.19 state(X162,X163,X164,X165,X166,X167,X168,X169,X170,X171,X172,X173,X174,X175,X176,X177,X178,X179,X180,X181,X182,X183,X184,X185,X186,X187,X188,X189,X190,X191,X192,X193,X194,X195,X196,X197,X198,X199,X200,X201,X202,X203,X204,X205,X206,X207,X208,X209,X210,X211,X212,X213,X214,X215) | ~state(X162,X163,X164,X196,X184,X172,X168,X169,X170,X171,X210,X173,X174,X175,X176,X177,X165,X179,X180,X181,X182,X183,X211,X185,X186,X187,X188,X189,X166,X191,X192,X193,X194,X195,X212,X197,X198,X199,X200,X201,X167,X203,X204,X205,X206,X207,X208,X209,X202,X190,X178,X213,X214,X215)). % 14.41/2.19 cnf(a162, assumption, % 14.41/2.19 X141 = X162). % 14.41/2.19 cnf(a163, assumption, % 14.41/2.19 X129 = X163). % 14.41/2.19 cnf(a164, assumption, % 14.41/2.19 X117 = X164). % 14.41/2.19 cnf(a165, assumption, % 14.41/2.19 X111 = X165). % 14.41/2.19 cnf(a166, assumption, % 14.41/2.19 X112 = X166). % 14.41/2.19 cnf(a167, assumption, % 14.41/2.19 X113 = X167). % 14.41/2.19 cnf(a168, assumption, % 14.41/2.19 X114 = X168). % 14.41/2.19 cnf(a169, assumption, % 14.41/2.19 X115 = X169). % 14.41/2.19 cnf(a170, assumption, % 14.41/2.19 X116 = X170). % 14.41/2.19 cnf(a171, assumption, % 14.41/2.19 X159 = X171). % 14.41/2.19 cnf(a172, assumption, % 14.41/2.19 X118 = X172). % 14.41/2.19 cnf(a173, assumption, % 14.41/2.19 X119 = X173). % 14.41/2.19 cnf(a174, assumption, % 14.41/2.19 X120 = X174). % 14.41/2.19 cnf(a175, assumption, % 14.41/2.19 X121 = X175). % 14.41/2.19 cnf(a176, assumption, % 14.41/2.19 X122 = X176). % 14.41/2.19 cnf(a177, assumption, % 14.41/2.19 X123 = X177). % 14.41/2.19 cnf(a178, assumption, % 14.41/2.19 X124 = X178). % 14.41/2.19 cnf(a179, assumption, % 14.41/2.19 X108 = X179). % 14.41/2.19 cnf(a180, assumption, % 14.41/2.19 X128 = X180). % 14.41/2.19 cnf(a181, assumption, % 14.41/2.19 X140 = X181). % 14.41/2.19 cnf(a182, assumption, % 14.41/2.19 X152 = X182). % 14.41/2.19 cnf(a183, assumption, % 14.41/2.19 X160 = X183). % 14.41/2.19 cnf(a184, assumption, % 14.41/2.19 X130 = X184). % 14.41/2.19 cnf(a185, assumption, % 14.41/2.19 X131 = X185). % 14.41/2.19 cnf(a186, assumption, % 14.41/2.19 X132 = X186). % 14.41/2.19 cnf(a187, assumption, % 14.41/2.19 X133 = X187). % 14.41/2.19 cnf(a188, assumption, % 14.41/2.19 X134 = X188). % 14.41/2.19 cnf(a189, assumption, % 14.41/2.19 X135 = X189). % 14.41/2.19 cnf(a190, assumption, % 14.41/2.19 X136 = X190). % 14.41/2.19 cnf(a191, assumption, % 14.41/2.19 X109 = X191). % 14.41/2.19 cnf(a192, assumption, % 14.41/2.19 X127 = X192). % 14.41/2.19 cnf(a193, assumption, % 14.41/2.19 X139 = X193). % 14.41/2.19 cnf(a194, assumption, % 14.41/2.19 X151 = X194). % 14.41/2.19 cnf(a195, assumption, % 14.41/2.19 X161 = X195). % 14.41/2.19 cnf(a196, assumption, % 14.41/2.19 X142 = X196). % 14.41/2.19 cnf(a197, assumption, % 14.41/2.19 X143 = X197). % 14.41/2.19 cnf(a198, assumption, % 14.41/2.19 X144 = X198). % 14.41/2.19 cnf(a199, assumption, % 14.41/2.19 X145 = X199). % 14.41/2.19 cnf(a200, assumption, % 14.41/2.19 X146 = X200). % 14.41/2.19 cnf(a201, assumption, % 14.41/2.19 X147 = X201). % 14.41/2.19 cnf(a202, assumption, % 14.41/2.19 X148 = X202). % 14.41/2.19 cnf(a203, assumption, % 14.41/2.19 X110 = X203). % 14.41/2.19 cnf(a204, assumption, % 14.41/2.19 X126 = X204). % 14.41/2.19 cnf(a205, assumption, % 14.41/2.19 X138 = X205). % 14.41/2.19 cnf(a206, assumption, % 14.41/2.19 X150 = X206). % 14.41/2.19 cnf(a207, assumption, % 14.41/2.19 X153 = X207). % 14.41/2.19 cnf(a208, assumption, % 14.41/2.19 X154 = X208). % 14.41/2.19 cnf(a209, assumption, % 14.41/2.19 X155 = X209). % 14.41/2.19 cnf(a210, assumption, % 14.41/2.19 X156 = X210). % 14.41/2.19 cnf(a211, assumption, % 14.41/2.19 X157 = X211). % 14.41/2.19 cnf(a212, assumption, % 14.41/2.19 X158 = X212). % 14.41/2.19 cnf(a213, assumption, % 14.41/2.19 X149 = X213). % 14.41/2.19 cnf(a214, assumption, % 14.41/2.19 X137 = X214). % 14.41/2.19 cnf(a215, assumption, % 14.41/2.19 X125 = X215). % 14.41/2.19 cnf(c12, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179, a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199, a200, a201, a202, a203, a204, a205, a206, a207, a208, a209, a210, a211, a212, a213, a214, a215])], [c10, c11])). % 14.41/2.19 cnf(c13, plain, % 14.41/2.19 ~state(X162,X163,X164,X196,X184,X172,X168,X169,X170,X171,X210,X173,X174,X175,X176,X177,X165,X179,X180,X181,X182,X183,X211,X185,X186,X187,X188,X189,X166,X191,X192,X193,X194,X195,X212,X197,X198,X199,X200,X201,X167,X203,X204,X205,X206,X207,X208,X209,X202,X190,X178,X213,X214,X215), % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179, a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199, a200, a201, a202, a203, a204, a205, a206, a207, a208, a209, a210, a211, a212, a213, a214, a215])], [c10, c11])). % 14.41/2.19 % 14.41/2.19 cnf(c14, axiom, % 14.41/2.19 state(X216,X217,X218,X219,X220,X221,X222,X223,X224,X225,X226,X227,X228,X229,X230,X231,X232,X233,X234,X235,X236,X237,X238,X239,X240,X241,X242,X243,X244,X245,X246,X247,X248,X249,X250,X251,X252,X253,X254,X255,X256,X257,X258,X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269) | ~state(X216,X217,X218,X250,X238,X226,X222,X223,X224,X225,X264,X227,X228,X229,X230,X231,X219,X233,X234,X235,X236,X237,X265,X239,X240,X241,X242,X243,X220,X245,X246,X247,X248,X249,X266,X251,X252,X253,X254,X255,X221,X257,X258,X259,X260,X261,X262,X263,X256,X244,X232,X267,X268,X269)). % 14.41/2.19 cnf(a216, assumption, % 14.41/2.19 X162 = X216). % 14.41/2.19 cnf(a217, assumption, % 14.41/2.19 X163 = X217). % 14.41/2.19 cnf(a218, assumption, % 14.41/2.19 X164 = X218). % 14.41/2.19 cnf(a219, assumption, % 14.41/2.19 X196 = X219). % 14.41/2.19 cnf(a220, assumption, % 14.41/2.19 X184 = X220). % 14.41/2.19 cnf(a221, assumption, % 14.41/2.19 X172 = X221). % 14.41/2.19 cnf(a222, assumption, % 14.41/2.19 X168 = X222). % 14.41/2.19 cnf(a223, assumption, % 14.41/2.19 X169 = X223). % 14.41/2.19 cnf(a224, assumption, % 14.41/2.19 X170 = X224). % 14.41/2.19 cnf(a225, assumption, % 14.41/2.19 X171 = X225). % 14.41/2.19 cnf(a226, assumption, % 14.41/2.19 X210 = X226). % 14.41/2.19 cnf(a227, assumption, % 14.41/2.19 X173 = X227). % 14.41/2.19 cnf(a228, assumption, % 14.41/2.19 X174 = X228). % 14.41/2.19 cnf(a229, assumption, % 14.41/2.19 X175 = X229). % 14.41/2.19 cnf(a230, assumption, % 14.41/2.19 X176 = X230). % 14.41/2.19 cnf(a231, assumption, % 14.41/2.19 X177 = X231). % 14.41/2.19 cnf(a232, assumption, % 14.41/2.19 X165 = X232). % 14.41/2.19 cnf(a233, assumption, % 14.41/2.19 X179 = X233). % 14.41/2.19 cnf(a234, assumption, % 14.41/2.19 X180 = X234). % 14.41/2.19 cnf(a235, assumption, % 14.41/2.19 X181 = X235). % 14.41/2.19 cnf(a236, assumption, % 14.41/2.19 X182 = X236). % 14.41/2.19 cnf(a237, assumption, % 14.41/2.19 X183 = X237). % 14.41/2.19 cnf(a238, assumption, % 14.41/2.19 X211 = X238). % 14.41/2.19 cnf(a239, assumption, % 14.41/2.19 X185 = X239). % 14.41/2.19 cnf(a240, assumption, % 14.41/2.19 X186 = X240). % 14.41/2.19 cnf(a241, assumption, % 14.41/2.19 X187 = X241). % 14.41/2.19 cnf(a242, assumption, % 14.41/2.19 X188 = X242). % 14.41/2.19 cnf(a243, assumption, % 14.41/2.19 X189 = X243). % 14.41/2.19 cnf(a244, assumption, % 14.41/2.19 X166 = X244). % 14.41/2.19 cnf(a245, assumption, % 14.41/2.19 X191 = X245). % 14.41/2.19 cnf(a246, assumption, % 14.41/2.19 X192 = X246). % 14.41/2.19 cnf(a247, assumption, % 14.41/2.19 X193 = X247). % 14.41/2.19 cnf(a248, assumption, % 14.41/2.19 X194 = X248). % 14.41/2.19 cnf(a249, assumption, % 14.41/2.19 X195 = X249). % 14.41/2.19 cnf(a250, assumption, % 14.41/2.19 X212 = X250). % 14.41/2.19 cnf(a251, assumption, % 14.41/2.19 X197 = X251). % 14.41/2.19 cnf(a252, assumption, % 14.41/2.19 X198 = X252). % 14.41/2.19 cnf(a253, assumption, % 14.41/2.19 X199 = X253). % 14.41/2.19 cnf(a254, assumption, % 14.41/2.19 X200 = X254). % 14.41/2.19 cnf(a255, assumption, % 14.41/2.19 X201 = X255). % 14.41/2.19 cnf(a256, assumption, % 14.41/2.19 X167 = X256). % 14.41/2.19 cnf(a257, assumption, % 14.41/2.19 X203 = X257). % 14.41/2.19 cnf(a258, assumption, % 14.41/2.19 X204 = X258). % 14.41/2.19 cnf(a259, assumption, % 14.41/2.19 X205 = X259). % 14.41/2.19 cnf(a260, assumption, % 14.41/2.19 X206 = X260). % 14.41/2.19 cnf(a261, assumption, % 14.41/2.19 X207 = X261). % 14.41/2.19 cnf(a262, assumption, % 14.41/2.19 X208 = X262). % 14.41/2.19 cnf(a263, assumption, % 14.41/2.19 X209 = X263). % 14.41/2.19 cnf(a264, assumption, % 14.41/2.19 X202 = X264). % 14.41/2.19 cnf(a265, assumption, % 14.41/2.19 X190 = X265). % 14.41/2.19 cnf(a266, assumption, % 14.41/2.19 X178 = X266). % 14.41/2.19 cnf(a267, assumption, % 14.41/2.19 X213 = X267). % 14.41/2.19 cnf(a268, assumption, % 14.41/2.19 X214 = X268). % 14.41/2.19 cnf(a269, assumption, % 14.41/2.19 X215 = X269). % 14.41/2.19 cnf(c15, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a216, a217, a218, a219, a220, a221, a222, a223, a224, a225, a226, a227, a228, a229, a230, a231, a232, a233, a234, a235, a236, a237, a238, a239, a240, a241, a242, a243, a244, a245, a246, a247, a248, a249, a250, a251, a252, a253, a254, a255, a256, a257, a258, a259, a260, a261, a262, a263, a264, a265, a266, a267, a268, a269])], [c13, c14])). % 14.41/2.19 cnf(c16, plain, % 14.41/2.19 ~state(X216,X217,X218,X250,X238,X226,X222,X223,X224,X225,X264,X227,X228,X229,X230,X231,X219,X233,X234,X235,X236,X237,X265,X239,X240,X241,X242,X243,X220,X245,X246,X247,X248,X249,X266,X251,X252,X253,X254,X255,X221,X257,X258,X259,X260,X261,X262,X263,X256,X244,X232,X267,X268,X269), % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a216, a217, a218, a219, a220, a221, a222, a223, a224, a225, a226, a227, a228, a229, a230, a231, a232, a233, a234, a235, a236, a237, a238, a239, a240, a241, a242, a243, a244, a245, a246, a247, a248, a249, a250, a251, a252, a253, a254, a255, a256, a257, a258, a259, a260, a261, a262, a263, a264, a265, a266, a267, a268, a269])], [c13, c14])). % 14.41/2.19 % 14.41/2.19 cnf(c17, axiom, % 14.41/2.19 state(b,r,r,w,w,w,y,b,b,g,y,r,b,g,g,o,g,y,w,w,r,g,o,r,b,g,g,o,r,b,y,y,r,g,o,g,o,o,o,y,r,b,y,y,r,w,w,w,b,b,y,w,o,o)). % 14.41/2.19 cnf(a270, assumption, % 14.41/2.19 X216 = b). % 14.41/2.19 cnf(a271, assumption, % 14.41/2.19 X217 = r). % 14.41/2.19 cnf(a272, assumption, % 14.41/2.19 X218 = r). % 14.41/2.19 cnf(a273, assumption, % 14.41/2.19 X250 = w). % 14.41/2.19 cnf(a274, assumption, % 14.41/2.19 X238 = w). % 14.41/2.19 cnf(a275, assumption, % 14.41/2.19 X226 = w). % 14.41/2.19 cnf(a276, assumption, % 14.41/2.19 X222 = y). % 14.41/2.19 cnf(a277, assumption, % 14.41/2.19 X223 = b). % 14.41/2.19 cnf(a278, assumption, % 14.41/2.19 X224 = b). % 14.41/2.19 cnf(a279, assumption, % 14.41/2.19 X225 = g). % 14.41/2.19 cnf(a280, assumption, % 14.41/2.19 X264 = y). % 14.41/2.19 cnf(a281, assumption, % 14.41/2.19 X227 = r). % 14.41/2.19 cnf(a282, assumption, % 14.41/2.19 X228 = b). % 14.41/2.19 cnf(a283, assumption, % 14.41/2.19 X229 = g). % 14.41/2.19 cnf(a284, assumption, % 14.41/2.19 X230 = g). % 14.41/2.19 cnf(a285, assumption, % 14.41/2.19 X231 = o). % 14.41/2.19 cnf(a286, assumption, % 14.41/2.19 X219 = g). % 14.41/2.19 cnf(a287, assumption, % 14.41/2.19 X233 = y). % 14.41/2.19 cnf(a288, assumption, % 14.41/2.19 X234 = w). % 14.41/2.19 cnf(a289, assumption, % 14.41/2.19 X235 = w). % 14.41/2.19 cnf(a290, assumption, % 14.41/2.19 X236 = r). % 14.41/2.19 cnf(a291, assumption, % 14.41/2.19 X237 = g). % 14.41/2.19 cnf(a292, assumption, % 14.41/2.19 X265 = o). % 14.41/2.19 cnf(a293, assumption, % 14.41/2.19 X239 = r). % 14.41/2.19 cnf(a294, assumption, % 14.41/2.19 X240 = b). % 14.41/2.19 cnf(a295, assumption, % 14.41/2.19 X241 = g). % 14.41/2.19 cnf(a296, assumption, % 14.41/2.19 X242 = g). % 14.41/2.19 cnf(a297, assumption, % 14.41/2.19 X243 = o). % 14.41/2.19 cnf(a298, assumption, % 14.41/2.19 X220 = r). % 14.41/2.19 cnf(a299, assumption, % 14.41/2.19 X245 = b). % 14.41/2.19 cnf(a300, assumption, % 14.41/2.19 X246 = y). % 14.41/2.19 cnf(a301, assumption, % 14.41/2.19 X247 = y). % 14.41/2.19 cnf(a302, assumption, % 14.41/2.19 X248 = r). % 14.41/2.19 cnf(a303, assumption, % 14.41/2.19 X249 = g). % 14.41/2.19 cnf(a304, assumption, % 14.41/2.19 X266 = o). % 14.41/2.19 cnf(a305, assumption, % 14.41/2.19 X251 = g). % 14.41/2.19 cnf(a306, assumption, % 14.41/2.19 X252 = o). % 14.41/2.19 cnf(a307, assumption, % 14.41/2.19 X253 = o). % 14.41/2.19 cnf(a308, assumption, % 14.41/2.19 X254 = o). % 14.41/2.19 cnf(a309, assumption, % 14.41/2.19 X255 = y). % 14.41/2.19 cnf(a310, assumption, % 14.41/2.19 X221 = r). % 14.41/2.19 cnf(a311, assumption, % 14.41/2.19 X257 = b). % 14.41/2.19 cnf(a312, assumption, % 14.41/2.19 X258 = y). % 14.41/2.19 cnf(a313, assumption, % 14.41/2.19 X259 = y). % 14.41/2.19 cnf(a314, assumption, % 14.41/2.19 X260 = r). % 14.41/2.19 cnf(a315, assumption, % 14.41/2.19 X261 = w). % 14.41/2.19 cnf(a316, assumption, % 14.41/2.19 X262 = w). % 14.41/2.19 cnf(a317, assumption, % 14.41/2.19 X263 = w). % 14.41/2.19 cnf(a318, assumption, % 14.41/2.19 X256 = b). % 14.41/2.19 cnf(a319, assumption, % 14.41/2.19 X244 = b). % 14.41/2.19 cnf(a320, assumption, % 14.41/2.19 X232 = y). % 14.41/2.19 cnf(a321, assumption, % 14.41/2.19 X267 = w). % 14.41/2.19 cnf(a322, assumption, % 14.41/2.19 X268 = o). % 14.41/2.19 cnf(a323, assumption, % 14.41/2.19 X269 = o). % 14.41/2.19 cnf(c18, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a270, a271, a272, a273, a274, a275, a276, a277, a278, a279, a280, a281, a282, a283, a284, a285, a286, a287, a288, a289, a290, a291, a292, a293, a294, a295, a296, a297, a298, a299, a300, a301, a302, a303, a304, a305, a306, a307, a308, a309, a310, a311, a312, a313, a314, a315, a316, a317, a318, a319, a320, a321, a322, a323])], [c16, c17])). % 14.41/2.19 cnf(c19, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(strict_predicate_extension, [assumptions([a270, a271, a272, a273, a274, a275, a276, a277, a278, a279, a280, a281, a282, a283, a284, a285, a286, a287, a288, a289, a290, a291, a292, a293, a294, a295, a296, a297, a298, a299, a300, a301, a302, a303, a304, a305, a306, a307, a308, a309, a310, a311, a312, a313, a314, a315, a316, a317, a318, a319, a320, a321, a322, a323])], [c16, c17])). % 14.41/2.19 % 14.41/2.19 cnf(c20, plain, % 14.41/2.19 $false, % 14.41/2.19 inference(constraint_solving, [ % 14.41/2.19 bind(X0, b), % 14.41/2.19 bind(X1, b), % 14.41/2.19 bind(X2, b), % 14.41/2.19 bind(X3, b), % 14.41/2.19 bind(X4, b), % 14.41/2.19 bind(X5, b), % 14.41/2.19 bind(X6, b), % 14.41/2.19 bind(X7, b), % 14.41/2.19 bind(X8, b), % 14.41/2.19 bind(X9, r), % 14.41/2.19 bind(X10, r), % 14.41/2.19 bind(X11, r), % 14.41/2.19 bind(X12, g), % 14.41/2.19 bind(X13, g), % 14.41/2.19 bind(X14, g), % 14.41/2.19 bind(X15, o), % 14.41/2.19 bind(X16, o), % 14.41/2.19 bind(X17, o), % 14.41/2.19 bind(X18, y), % 14.41/2.19 bind(X19, y), % 14.41/2.19 bind(X20, y), % 14.41/2.19 bind(X21, r), % 14.41/2.19 bind(X22, r), % 14.41/2.19 bind(X23, r), % 14.41/2.19 bind(X24, g), % 14.41/2.19 bind(X25, g), % 14.41/2.19 bind(X26, g), % 14.41/2.19 bind(X27, o), % 14.41/2.19 bind(X28, o), % 14.41/2.19 bind(X29, o), % 14.41/2.19 bind(X30, y), % 14.41/2.19 bind(X31, y), % 14.41/2.19 bind(X32, y), % 14.41/2.19 bind(X33, r), % 14.41/2.19 bind(X34, r), % 14.41/2.19 bind(X35, r), % 14.41/2.19 bind(X36, g), % 14.41/2.19 bind(X37, g), % 14.41/2.19 bind(X38, g), % 14.41/2.19 bind(X39, o), % 14.41/2.19 bind(X40, o), % 14.41/2.19 bind(X41, o), % 14.41/2.19 bind(X42, y), % 14.41/2.19 bind(X43, y), % 14.41/2.19 bind(X44, y), % 14.41/2.19 bind(X45, w), % 14.41/2.19 bind(X46, w), % 14.41/2.19 bind(X47, w), % 14.41/2.19 bind(X48, w), % 14.41/2.19 bind(X49, w), % 14.41/2.19 bind(X50, w), % 14.41/2.19 bind(X51, w), % 14.41/2.19 bind(X52, w), % 14.41/2.19 bind(X53, w), % 14.41/2.19 bind(X54, y), % 14.41/2.19 bind(X55, b), % 14.41/2.19 bind(X56, b), % 14.41/2.19 bind(X57, y), % 14.41/2.19 bind(X58, b), % 14.41/2.19 bind(X59, b), % 14.41/2.19 bind(X60, y), % 14.41/2.19 bind(X61, b), % 14.41/2.19 bind(X62, b), % 14.41/2.19 bind(X63, r), % 14.41/2.19 bind(X64, r), % 14.41/2.19 bind(X65, r), % 14.41/2.19 bind(X66, b), % 14.41/2.19 bind(X67, g), % 14.41/2.19 bind(X68, g), % 14.41/2.19 bind(X69, o), % 14.41/2.19 bind(X70, o), % 14.41/2.19 bind(X71, o), % 14.41/2.19 bind(X72, y), % 14.41/2.19 bind(X73, y), % 14.41/2.19 bind(X74, w), % 14.41/2.19 bind(X75, r), % 14.41/2.19 bind(X76, r), % 14.41/2.19 bind(X77, r), % 14.41/2.19 bind(X78, b), % 14.41/2.19 bind(X79, g), % 14.41/2.19 bind(X80, g), % 14.41/2.19 bind(X81, o), % 14.41/2.19 bind(X82, o), % 14.41/2.19 bind(X83, o), % 14.41/2.19 bind(X84, y), % 14.41/2.19 bind(X85, y), % 14.41/2.19 bind(X86, w), % 14.41/2.19 bind(X87, r), % 14.41/2.19 bind(X88, r), % 14.41/2.19 bind(X89, r), % 14.41/2.19 bind(X90, b), % 14.41/2.19 bind(X91, g), % 14.41/2.19 bind(X92, g), % 14.41/2.19 bind(X93, o), % 14.41/2.19 bind(X94, o), % 14.41/2.19 bind(X95, o), % 14.41/2.19 bind(X96, y), % 14.41/2.19 bind(X97, y), % 14.41/2.19 bind(X98, w), % 14.41/2.19 bind(X99, g), % 14.41/2.19 bind(X100, w), % 14.41/2.19 bind(X101, w), % 14.41/2.19 bind(X102, g), % 14.41/2.19 bind(X103, w), % 14.41/2.19 bind(X104, w), % 14.41/2.19 bind(X105, g), % 14.41/2.19 bind(X106, w), % 14.41/2.19 bind(X107, w), % 14.41/2.19 bind(X108, y), % 14.41/2.19 bind(X109, b), % 14.41/2.19 bind(X110, b), % 14.41/2.19 bind(X111, y), % 14.41/2.19 bind(X112, b), % 14.41/2.19 bind(X113, b), % 14.41/2.19 bind(X114, y), % 14.41/2.19 bind(X115, b), % 14.41/2.19 bind(X116, b), % 14.41/2.19 bind(X117, r), % 14.41/2.19 bind(X118, r), % 14.41/2.19 bind(X119, r), % 14.41/2.19 bind(X120, b), % 14.41/2.19 bind(X121, g), % 14.41/2.19 bind(X122, g), % 14.41/2.19 bind(X123, o), % 14.41/2.19 bind(X124, o), % 14.41/2.19 bind(X125, o), % 14.41/2.19 bind(X126, y), % 14.41/2.19 bind(X127, y), % 14.41/2.19 bind(X128, w), % 14.41/2.19 bind(X129, r), % 14.41/2.19 bind(X130, r), % 14.41/2.19 bind(X131, r), % 14.41/2.19 bind(X132, b), % 14.41/2.19 bind(X133, g), % 14.41/2.19 bind(X134, g), % 14.41/2.19 bind(X135, o), % 14.41/2.19 bind(X136, o), % 14.41/2.19 bind(X137, o), % 14.41/2.19 bind(X138, y), % 14.41/2.19 bind(X139, y), % 14.41/2.19 bind(X140, w), % 14.41/2.19 bind(X141, b), % 14.41/2.19 bind(X142, g), % 14.41/2.19 bind(X143, g), % 14.41/2.19 bind(X144, o), % 14.41/2.19 bind(X145, o), % 14.41/2.19 bind(X146, o), % 14.41/2.19 bind(X147, y), % 14.41/2.19 bind(X148, y), % 14.41/2.19 bind(X149, w), % 14.41/2.19 bind(X150, r), % 14.41/2.19 bind(X151, r), % 14.41/2.19 bind(X152, r), % 14.41/2.19 bind(X153, w), % 14.41/2.19 bind(X154, w), % 14.41/2.19 bind(X155, w), % 14.41/2.19 bind(X156, w), % 14.41/2.19 bind(X157, w), % 14.41/2.19 bind(X158, w), % 14.41/2.19 bind(X159, g), % 14.41/2.19 bind(X160, g), % 14.41/2.19 bind(X161, g), % 14.41/2.19 bind(X162, b), % 14.41/2.19 bind(X163, r), % 14.41/2.19 bind(X164, r), % 14.41/2.19 bind(X165, y), % 14.41/2.19 bind(X166, b), % 14.41/2.19 bind(X167, b), % 14.41/2.19 bind(X168, y), % 14.41/2.19 bind(X169, b), % 14.41/2.19 bind(X170, b), % 14.41/2.19 bind(X171, g), % 14.41/2.19 bind(X172, r), % 14.41/2.19 bind(X173, r), % 14.41/2.19 bind(X174, b), % 14.41/2.19 bind(X175, g), % 14.41/2.19 bind(X176, g), % 14.41/2.19 bind(X177, o), % 14.41/2.19 bind(X178, o), % 14.41/2.19 bind(X179, y), % 14.41/2.19 bind(X180, w), % 14.41/2.19 bind(X181, w), % 14.41/2.19 bind(X182, r), % 14.41/2.19 bind(X183, g), % 14.41/2.19 bind(X184, r), % 14.41/2.19 bind(X185, r), % 14.41/2.19 bind(X186, b), % 14.41/2.19 bind(X187, g), % 14.41/2.19 bind(X188, g), % 14.41/2.19 bind(X189, o), % 14.41/2.19 bind(X190, o), % 14.41/2.19 bind(X191, b), % 14.41/2.19 bind(X192, y), % 14.41/2.19 bind(X193, y), % 14.41/2.19 bind(X194, r), % 14.41/2.19 bind(X195, g), % 14.41/2.19 bind(X196, g), % 14.41/2.19 bind(X197, g), % 14.41/2.19 bind(X198, o), % 14.41/2.19 bind(X199, o), % 14.41/2.19 bind(X200, o), % 14.41/2.19 bind(X201, y), % 14.41/2.19 bind(X202, y), % 14.41/2.19 bind(X203, b), % 14.41/2.19 bind(X204, y), % 14.41/2.19 bind(X205, y), % 14.41/2.19 bind(X206, r), % 14.41/2.19 bind(X207, w), % 14.41/2.19 bind(X208, w), % 14.41/2.19 bind(X209, w), % 14.41/2.19 bind(X210, w), % 14.41/2.19 bind(X211, w), % 14.41/2.19 bind(X212, w), % 14.41/2.19 bind(X213, w), % 14.41/2.19 bind(X214, o), % 14.41/2.19 bind(X215, o), % 14.41/2.19 bind(X216, b), % 14.41/2.19 bind(X217, r), % 14.41/2.19 bind(X218, r), % 14.41/2.19 bind(X219, g), % 14.41/2.19 bind(X220, r), % 14.41/2.19 bind(X221, r), % 14.41/2.19 bind(X222, y), % 14.41/2.19 bind(X223, b), % 14.41/2.19 bind(X224, b), % 14.41/2.19 bind(X225, g), % 14.41/2.19 bind(X226, w), % 14.41/2.19 bind(X227, r), % 14.41/2.19 bind(X228, b), % 14.41/2.19 bind(X229, g), % 14.41/2.19 bind(X230, g), % 14.41/2.19 bind(X231, o), % 14.41/2.19 bind(X232, y), % 14.41/2.19 bind(X233, y), % 14.41/2.19 bind(X234, w), % 14.41/2.19 bind(X235, w), % 14.41/2.19 bind(X236, r), % 14.41/2.19 bind(X237, g), % 14.41/2.19 bind(X238, w), % 14.41/2.19 bind(X239, r), % 14.41/2.19 bind(X240, b), % 14.41/2.19 bind(X241, g), % 14.41/2.19 bind(X242, g), % 14.41/2.19 bind(X243, o), % 14.41/2.19 bind(X244, b), % 14.41/2.19 bind(X245, b), % 14.41/2.19 bind(X246, y), % 14.41/2.19 bind(X247, y), % 14.41/2.19 bind(X248, r), % 14.41/2.19 bind(X249, g), % 14.41/2.19 bind(X250, w), % 14.41/2.19 bind(X251, g), % 14.41/2.19 bind(X252, o), % 14.41/2.19 bind(X253, o), % 14.41/2.19 bind(X254, o), % 14.41/2.19 bind(X255, y), % 14.41/2.19 bind(X256, b), % 14.41/2.19 bind(X257, b), % 14.41/2.19 bind(X258, y), % 14.41/2.19 bind(X259, y), % 14.41/2.19 bind(X260, r), % 14.41/2.19 bind(X261, w), % 14.41/2.19 bind(X262, w), % 14.41/2.19 bind(X263, w), % 14.41/2.19 bind(X264, y), % 14.41/2.19 bind(X265, o), % 14.41/2.19 bind(X266, o), % 14.41/2.19 bind(X267, w), % 14.41/2.19 bind(X268, o), % 14.41/2.19 bind(X269, o) % 14.41/2.19 ], % 14.41/2.19 [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59, a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99, a100, a101, a102, a103, a104, a105, a106, a107, a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119, a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139, a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159, a160, a161, a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179, a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199, a200, a201, a202, a203, a204, a205, a206, a207, a208, a209, a210, a211, a212, a213, a214, a215, a216, a217, a218, a219, a220, a221, a222, a223, a224, a225, a226, a227, a228, a229, a230, a231, a232, a233, a234, a235, a236, a237, a238, a239, a240, a241, a242, a243, a244, a245, a246, a247, a248, a249, a250, a251, a252, a253, a254, a255, a256, a257, a258, a259, a260, a261, a262, a263, a264, a265, a266, a267, a268, a269, a270, a271, a272, a273, a274, a275, a276, a277, a278, a279, a280, a281, a282, a283, a284, a285, a286, a287, a288, a289, a290, a291, a292, a293, a294, a295, a296, a297, a298, a299, a300, a301, a302, a303, a304, a305, a306, a307, a308, a309, a310, a311, a312, a313, a314, a315, a316, a317, a318, a319, a320, a321, a322, a323])). % 14.41/2.19 % 14.41/2.19 % SZS output end IncompleteProof %------------------------------------------------------------------------------