%------------------------------------------------------------------------------ % File : lazyCoP---0.1 % Problem : PUZ036-1.005 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % Computer : n025.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 0.13s 0.35s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ036-1.005 : TPTP v8.1.0. Released v2.0.0. % 0.11/0.13 % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sat May 28 21:34:26 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 % SZS status Unsatisfiable % 0.13/0.35 % SZS output begin IncompleteProof % 0.13/0.35 cnf(c0, axiom, % 0.13/0.35 ~state(p_1,p_2,p_3,p_4,p_5,p_6,p_7,p_8,p_9,p_10,p_11,p_12,p_13,p_14,p_15,p_16,p_17,p_18,p_19,p_20)). % 0.13/0.35 cnf(c1, plain, % 0.13/0.35 ~state(p_1,p_2,p_3,p_4,p_5,p_6,p_7,p_8,p_9,p_10,p_11,p_12,p_13,p_14,p_15,p_16,p_17,p_18,p_19,p_20), % 0.13/0.35 inference(start, [], [c0])). % 0.13/0.35 % 0.13/0.35 cnf(c2, axiom, % 0.13/0.35 state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) | ~state(X3,X2,X1,X0,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)). % 0.13/0.35 cnf(a0, assumption, % 0.13/0.35 p_1 = X0). % 0.13/0.35 cnf(a1, assumption, % 0.13/0.35 p_2 = X1). % 0.13/0.35 cnf(a2, assumption, % 0.13/0.35 p_3 = X2). % 0.13/0.35 cnf(a3, assumption, % 0.13/0.35 p_4 = X3). % 0.13/0.35 cnf(a4, assumption, % 0.13/0.35 p_5 = X4). % 0.13/0.35 cnf(a5, assumption, % 0.13/0.35 p_6 = X5). % 0.13/0.35 cnf(a6, assumption, % 0.13/0.35 p_7 = X6). % 0.13/0.35 cnf(a7, assumption, % 0.13/0.35 p_8 = X7). % 0.13/0.35 cnf(a8, assumption, % 0.13/0.35 p_9 = X8). % 0.13/0.35 cnf(a9, assumption, % 0.13/0.35 p_10 = X9). % 0.13/0.35 cnf(a10, assumption, % 0.13/0.35 p_11 = X10). % 0.13/0.35 cnf(a11, assumption, % 0.13/0.35 p_12 = X11). % 0.13/0.35 cnf(a12, assumption, % 0.13/0.35 p_13 = X12). % 0.13/0.35 cnf(a13, assumption, % 0.13/0.35 p_14 = X13). % 0.13/0.35 cnf(a14, assumption, % 0.13/0.35 p_15 = X14). % 0.13/0.35 cnf(a15, assumption, % 0.13/0.35 p_16 = X15). % 0.13/0.35 cnf(a16, assumption, % 0.13/0.35 p_17 = X16). % 0.13/0.35 cnf(a17, assumption, % 0.13/0.35 p_18 = X17). % 0.13/0.35 cnf(a18, assumption, % 0.13/0.35 p_19 = X18). % 0.13/0.35 cnf(a19, assumption, % 0.13/0.35 p_20 = X19). % 0.13/0.35 cnf(c3, plain, % 0.13/0.35 $false, % 0.13/0.35 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])], [c1, c2])). % 0.13/0.35 cnf(c4, plain, % 0.13/0.35 ~state(X3,X2,X1,X0,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19), % 0.13/0.35 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])], [c1, c2])). % 0.13/0.35 % 0.13/0.35 cnf(c5, axiom, % 0.13/0.35 state(X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39) | ~state(X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X20)). % 0.13/0.35 cnf(a20, assumption, % 0.13/0.35 X3 = X20). % 0.13/0.35 cnf(a21, assumption, % 0.13/0.35 X2 = X21). % 0.13/0.35 cnf(a22, assumption, % 0.13/0.35 X1 = X22). % 0.13/0.35 cnf(a23, assumption, % 0.13/0.35 X0 = X23). % 0.13/0.35 cnf(a24, assumption, % 0.13/0.35 X4 = X24). % 0.13/0.35 cnf(a25, assumption, % 0.13/0.35 X5 = X25). % 0.13/0.35 cnf(a26, assumption, % 0.13/0.35 X6 = X26). % 0.13/0.35 cnf(a27, assumption, % 0.13/0.35 X7 = X27). % 0.13/0.35 cnf(a28, assumption, % 0.13/0.35 X8 = X28). % 0.13/0.35 cnf(a29, assumption, % 0.13/0.35 X9 = X29). % 0.13/0.35 cnf(a30, assumption, % 0.13/0.35 X10 = X30). % 0.13/0.35 cnf(a31, assumption, % 0.13/0.35 X11 = X31). % 0.13/0.35 cnf(a32, assumption, % 0.13/0.35 X12 = X32). % 0.13/0.35 cnf(a33, assumption, % 0.13/0.35 X13 = X33). % 0.13/0.35 cnf(a34, assumption, % 0.13/0.35 X14 = X34). % 0.13/0.35 cnf(a35, assumption, % 0.13/0.35 X15 = X35). % 0.13/0.35 cnf(a36, assumption, % 0.13/0.35 X16 = X36). % 0.13/0.35 cnf(a37, assumption, % 0.13/0.35 X17 = X37). % 0.13/0.35 cnf(a38, assumption, % 0.13/0.35 X18 = X38). % 0.13/0.35 cnf(a39, assumption, % 0.13/0.35 X19 = X39). % 0.13/0.35 cnf(c6, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39])], [c4, c5])). % 0.13/0.35 cnf(c7, plain, % 0.13/0.35 ~state(X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X20), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39])], [c4, c5])). % 0.13/0.35 % 0.13/0.35 cnf(c8, axiom, % 0.13/0.35 state(X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59) | ~state(X43,X42,X41,X40,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59)). % 0.13/0.35 cnf(a40, assumption, % 0.13/0.35 X21 = X40). % 0.13/0.35 cnf(a41, assumption, % 0.13/0.35 X22 = X41). % 0.13/0.35 cnf(a42, assumption, % 0.13/0.35 X23 = X42). % 0.13/0.35 cnf(a43, assumption, % 0.13/0.35 X24 = X43). % 0.13/0.35 cnf(a44, assumption, % 0.13/0.35 X25 = X44). % 0.13/0.35 cnf(a45, assumption, % 0.13/0.35 X26 = X45). % 0.13/0.35 cnf(a46, assumption, % 0.13/0.35 X27 = X46). % 0.13/0.35 cnf(a47, assumption, % 0.13/0.35 X28 = X47). % 0.13/0.35 cnf(a48, assumption, % 0.13/0.35 X29 = X48). % 0.13/0.35 cnf(a49, assumption, % 0.13/0.35 X30 = X49). % 0.13/0.35 cnf(a50, assumption, % 0.13/0.35 X31 = X50). % 0.13/0.35 cnf(a51, assumption, % 0.13/0.35 X32 = X51). % 0.13/0.35 cnf(a52, assumption, % 0.13/0.35 X33 = X52). % 0.13/0.35 cnf(a53, assumption, % 0.13/0.35 X34 = X53). % 0.13/0.35 cnf(a54, assumption, % 0.13/0.35 X35 = X54). % 0.13/0.35 cnf(a55, assumption, % 0.13/0.35 X36 = X55). % 0.13/0.35 cnf(a56, assumption, % 0.13/0.35 X37 = X56). % 0.13/0.35 cnf(a57, assumption, % 0.13/0.35 X38 = X57). % 0.13/0.35 cnf(a58, assumption, % 0.13/0.35 X39 = X58). % 0.13/0.35 cnf(a59, assumption, % 0.13/0.35 X20 = X59). % 0.13/0.35 cnf(c9, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59])], [c7, c8])). % 0.13/0.35 cnf(c10, plain, % 0.13/0.35 ~state(X43,X42,X41,X40,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59])], [c7, c8])). % 0.13/0.35 % 0.13/0.35 cnf(c11, axiom, % 0.13/0.35 state(X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79) | ~state(X79,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78)). % 0.13/0.35 cnf(a60, assumption, % 0.13/0.35 X43 = X60). % 0.13/0.35 cnf(a61, assumption, % 0.13/0.35 X42 = X61). % 0.13/0.35 cnf(a62, assumption, % 0.13/0.35 X41 = X62). % 0.13/0.35 cnf(a63, assumption, % 0.13/0.35 X40 = X63). % 0.13/0.35 cnf(a64, assumption, % 0.13/0.35 X44 = X64). % 0.13/0.35 cnf(a65, assumption, % 0.13/0.35 X45 = X65). % 0.13/0.35 cnf(a66, assumption, % 0.13/0.35 X46 = X66). % 0.13/0.35 cnf(a67, assumption, % 0.13/0.35 X47 = X67). % 0.13/0.35 cnf(a68, assumption, % 0.13/0.35 X48 = X68). % 0.13/0.35 cnf(a69, assumption, % 0.13/0.35 X49 = X69). % 0.13/0.35 cnf(a70, assumption, % 0.13/0.35 X50 = X70). % 0.13/0.35 cnf(a71, assumption, % 0.13/0.35 X51 = X71). % 0.13/0.35 cnf(a72, assumption, % 0.13/0.35 X52 = X72). % 0.13/0.35 cnf(a73, assumption, % 0.13/0.35 X53 = X73). % 0.13/0.35 cnf(a74, assumption, % 0.13/0.35 X54 = X74). % 0.13/0.35 cnf(a75, assumption, % 0.13/0.35 X55 = X75). % 0.13/0.35 cnf(a76, assumption, % 0.13/0.35 X56 = X76). % 0.13/0.35 cnf(a77, assumption, % 0.13/0.35 X57 = X77). % 0.13/0.35 cnf(a78, assumption, % 0.13/0.35 X58 = X78). % 0.13/0.35 cnf(a79, assumption, % 0.13/0.35 X59 = X79). % 0.13/0.35 cnf(c12, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79])], [c10, c11])). % 0.13/0.35 cnf(c13, plain, % 0.13/0.35 ~state(X79,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79])], [c10, c11])). % 0.13/0.35 % 0.13/0.35 cnf(c14, axiom, % 0.13/0.35 state(X80,X81,X82,X83,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99) | ~state(X83,X82,X81,X80,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99)). % 0.13/0.35 cnf(a80, assumption, % 0.13/0.35 X79 = X80). % 0.13/0.35 cnf(a81, assumption, % 0.13/0.35 X60 = X81). % 0.13/0.35 cnf(a82, assumption, % 0.13/0.35 X61 = X82). % 0.13/0.35 cnf(a83, assumption, % 0.13/0.35 X62 = X83). % 0.13/0.35 cnf(a84, assumption, % 0.13/0.35 X63 = X84). % 0.13/0.35 cnf(a85, assumption, % 0.13/0.35 X64 = X85). % 0.13/0.35 cnf(a86, assumption, % 0.13/0.35 X65 = X86). % 0.13/0.35 cnf(a87, assumption, % 0.13/0.35 X66 = X87). % 0.13/0.35 cnf(a88, assumption, % 0.13/0.35 X67 = X88). % 0.13/0.35 cnf(a89, assumption, % 0.13/0.35 X68 = X89). % 0.13/0.35 cnf(a90, assumption, % 0.13/0.35 X69 = X90). % 0.13/0.35 cnf(a91, assumption, % 0.13/0.35 X70 = X91). % 0.13/0.35 cnf(a92, assumption, % 0.13/0.35 X71 = X92). % 0.13/0.35 cnf(a93, assumption, % 0.13/0.35 X72 = X93). % 0.13/0.35 cnf(a94, assumption, % 0.13/0.35 X73 = X94). % 0.13/0.35 cnf(a95, assumption, % 0.13/0.35 X74 = X95). % 0.13/0.35 cnf(a96, assumption, % 0.13/0.35 X75 = X96). % 0.13/0.35 cnf(a97, assumption, % 0.13/0.35 X76 = X97). % 0.13/0.35 cnf(a98, assumption, % 0.13/0.35 X77 = X98). % 0.13/0.35 cnf(a99, assumption, % 0.13/0.35 X78 = X99). % 0.13/0.35 cnf(c15, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99])], [c13, c14])). % 0.13/0.35 cnf(c16, plain, % 0.13/0.35 ~state(X83,X82,X81,X80,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99])], [c13, c14])). % 0.13/0.35 % 0.13/0.35 cnf(c17, axiom, % 0.13/0.35 state(X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119) | ~state(X101,X102,X103,X104,X105,X106,X107,X108,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119,X100)). % 0.13/0.35 cnf(a100, assumption, % 0.13/0.35 X83 = X100). % 0.13/0.35 cnf(a101, assumption, % 0.13/0.35 X82 = X101). % 0.13/0.35 cnf(a102, assumption, % 0.13/0.35 X81 = X102). % 0.13/0.35 cnf(a103, assumption, % 0.13/0.35 X80 = X103). % 0.13/0.35 cnf(a104, assumption, % 0.13/0.35 X84 = X104). % 0.13/0.35 cnf(a105, assumption, % 0.13/0.35 X85 = X105). % 0.13/0.35 cnf(a106, assumption, % 0.13/0.35 X86 = X106). % 0.13/0.35 cnf(a107, assumption, % 0.13/0.35 X87 = X107). % 0.13/0.35 cnf(a108, assumption, % 0.13/0.35 X88 = X108). % 0.13/0.35 cnf(a109, assumption, % 0.13/0.35 X89 = X109). % 0.13/0.35 cnf(a110, assumption, % 0.13/0.35 X90 = X110). % 0.13/0.35 cnf(a111, assumption, % 0.13/0.35 X91 = X111). % 0.13/0.35 cnf(a112, assumption, % 0.13/0.35 X92 = X112). % 0.13/0.35 cnf(a113, assumption, % 0.13/0.35 X93 = X113). % 0.13/0.35 cnf(a114, assumption, % 0.13/0.35 X94 = X114). % 0.13/0.35 cnf(a115, assumption, % 0.13/0.35 X95 = X115). % 0.13/0.35 cnf(a116, assumption, % 0.13/0.35 X96 = X116). % 0.13/0.35 cnf(a117, assumption, % 0.13/0.35 X97 = X117). % 0.13/0.35 cnf(a118, assumption, % 0.13/0.35 X98 = X118). % 0.13/0.35 cnf(a119, assumption, % 0.13/0.35 X99 = X119). % 0.13/0.35 cnf(c18, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a100, a101, a102, a103, a104, a105, a106, a107, a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119])], [c16, c17])). % 0.13/0.35 cnf(c19, plain, % 0.13/0.35 ~state(X101,X102,X103,X104,X105,X106,X107,X108,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119,X100), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a100, a101, a102, a103, a104, a105, a106, a107, a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119])], [c16, c17])). % 0.13/0.35 % 0.13/0.35 cnf(c20, axiom, % 0.13/0.35 state(X120,X121,X122,X123,X124,X125,X126,X127,X128,X129,X130,X131,X132,X133,X134,X135,X136,X137,X138,X139) | ~state(X123,X122,X121,X120,X124,X125,X126,X127,X128,X129,X130,X131,X132,X133,X134,X135,X136,X137,X138,X139)). % 0.13/0.35 cnf(a120, assumption, % 0.13/0.35 X101 = X120). % 0.13/0.35 cnf(a121, assumption, % 0.13/0.35 X102 = X121). % 0.13/0.35 cnf(a122, assumption, % 0.13/0.35 X103 = X122). % 0.13/0.35 cnf(a123, assumption, % 0.13/0.35 X104 = X123). % 0.13/0.35 cnf(a124, assumption, % 0.13/0.35 X105 = X124). % 0.13/0.35 cnf(a125, assumption, % 0.13/0.35 X106 = X125). % 0.13/0.35 cnf(a126, assumption, % 0.13/0.35 X107 = X126). % 0.13/0.35 cnf(a127, assumption, % 0.13/0.35 X108 = X127). % 0.13/0.35 cnf(a128, assumption, % 0.13/0.35 X109 = X128). % 0.13/0.35 cnf(a129, assumption, % 0.13/0.35 X110 = X129). % 0.13/0.35 cnf(a130, assumption, % 0.13/0.35 X111 = X130). % 0.13/0.35 cnf(a131, assumption, % 0.13/0.35 X112 = X131). % 0.13/0.35 cnf(a132, assumption, % 0.13/0.35 X113 = X132). % 0.13/0.35 cnf(a133, assumption, % 0.13/0.35 X114 = X133). % 0.13/0.35 cnf(a134, assumption, % 0.13/0.35 X115 = X134). % 0.13/0.35 cnf(a135, assumption, % 0.13/0.35 X116 = X135). % 0.13/0.35 cnf(a136, assumption, % 0.13/0.35 X117 = X136). % 0.13/0.35 cnf(a137, assumption, % 0.13/0.35 X118 = X137). % 0.13/0.35 cnf(a138, assumption, % 0.13/0.35 X119 = X138). % 0.13/0.35 cnf(a139, assumption, % 0.13/0.35 X100 = X139). % 0.13/0.35 cnf(c21, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139])], [c19, c20])). % 0.13/0.35 cnf(c22, plain, % 0.13/0.35 ~state(X123,X122,X121,X120,X124,X125,X126,X127,X128,X129,X130,X131,X132,X133,X134,X135,X136,X137,X138,X139), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139])], [c19, c20])). % 0.13/0.35 % 0.13/0.35 cnf(c23, axiom, % 0.13/0.35 state(X140,X141,X142,X143,X144,X145,X146,X147,X148,X149,X150,X151,X152,X153,X154,X155,X156,X157,X158,X159) | ~state(X159,X140,X141,X142,X143,X144,X145,X146,X147,X148,X149,X150,X151,X152,X153,X154,X155,X156,X157,X158)). % 0.13/0.35 cnf(a140, assumption, % 0.13/0.35 X123 = X140). % 0.13/0.35 cnf(a141, assumption, % 0.13/0.35 X122 = X141). % 0.13/0.35 cnf(a142, assumption, % 0.13/0.35 X121 = X142). % 0.13/0.35 cnf(a143, assumption, % 0.13/0.35 X120 = X143). % 0.13/0.35 cnf(a144, assumption, % 0.13/0.35 X124 = X144). % 0.13/0.35 cnf(a145, assumption, % 0.13/0.35 X125 = X145). % 0.13/0.35 cnf(a146, assumption, % 0.13/0.35 X126 = X146). % 0.13/0.35 cnf(a147, assumption, % 0.13/0.35 X127 = X147). % 0.13/0.35 cnf(a148, assumption, % 0.13/0.35 X128 = X148). % 0.13/0.35 cnf(a149, assumption, % 0.13/0.35 X129 = X149). % 0.13/0.35 cnf(a150, assumption, % 0.13/0.35 X130 = X150). % 0.13/0.35 cnf(a151, assumption, % 0.13/0.35 X131 = X151). % 0.13/0.35 cnf(a152, assumption, % 0.13/0.35 X132 = X152). % 0.13/0.35 cnf(a153, assumption, % 0.13/0.35 X133 = X153). % 0.13/0.35 cnf(a154, assumption, % 0.13/0.35 X134 = X154). % 0.13/0.35 cnf(a155, assumption, % 0.13/0.35 X135 = X155). % 0.13/0.35 cnf(a156, assumption, % 0.13/0.35 X136 = X156). % 0.13/0.35 cnf(a157, assumption, % 0.13/0.35 X137 = X157). % 0.13/0.35 cnf(a158, assumption, % 0.13/0.35 X138 = X158). % 0.13/0.35 cnf(a159, assumption, % 0.13/0.35 X139 = X159). % 0.13/0.35 cnf(c24, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159])], [c22, c23])). % 0.13/0.35 cnf(c25, plain, % 0.13/0.35 ~state(X159,X140,X141,X142,X143,X144,X145,X146,X147,X148,X149,X150,X151,X152,X153,X154,X155,X156,X157,X158), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159])], [c22, c23])). % 0.13/0.35 % 0.13/0.35 cnf(c26, axiom, % 0.13/0.35 state(X160,X161,X162,X163,X164,X165,X166,X167,X168,X169,X170,X171,X172,X173,X174,X175,X176,X177,X178,X179) | ~state(X163,X162,X161,X160,X164,X165,X166,X167,X168,X169,X170,X171,X172,X173,X174,X175,X176,X177,X178,X179)). % 0.13/0.35 cnf(a160, assumption, % 0.13/0.35 X159 = X160). % 0.13/0.35 cnf(a161, assumption, % 0.13/0.35 X140 = X161). % 0.13/0.35 cnf(a162, assumption, % 0.13/0.35 X141 = X162). % 0.13/0.35 cnf(a163, assumption, % 0.13/0.35 X142 = X163). % 0.13/0.35 cnf(a164, assumption, % 0.13/0.35 X143 = X164). % 0.13/0.35 cnf(a165, assumption, % 0.13/0.35 X144 = X165). % 0.13/0.35 cnf(a166, assumption, % 0.13/0.35 X145 = X166). % 0.13/0.35 cnf(a167, assumption, % 0.13/0.35 X146 = X167). % 0.13/0.35 cnf(a168, assumption, % 0.13/0.35 X147 = X168). % 0.13/0.35 cnf(a169, assumption, % 0.13/0.35 X148 = X169). % 0.13/0.35 cnf(a170, assumption, % 0.13/0.35 X149 = X170). % 0.13/0.35 cnf(a171, assumption, % 0.13/0.35 X150 = X171). % 0.13/0.35 cnf(a172, assumption, % 0.13/0.35 X151 = X172). % 0.13/0.35 cnf(a173, assumption, % 0.13/0.35 X152 = X173). % 0.13/0.35 cnf(a174, assumption, % 0.13/0.35 X153 = X174). % 0.13/0.35 cnf(a175, assumption, % 0.13/0.35 X154 = X175). % 0.13/0.35 cnf(a176, assumption, % 0.13/0.35 X155 = X176). % 0.13/0.35 cnf(a177, assumption, % 0.13/0.35 X156 = X177). % 0.13/0.35 cnf(a178, assumption, % 0.13/0.35 X157 = X178). % 0.13/0.35 cnf(a179, assumption, % 0.13/0.35 X158 = X179). % 0.13/0.35 cnf(c27, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a160, a161, a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179])], [c25, c26])). % 0.13/0.35 cnf(c28, plain, % 0.13/0.35 ~state(X163,X162,X161,X160,X164,X165,X166,X167,X168,X169,X170,X171,X172,X173,X174,X175,X176,X177,X178,X179), % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a160, a161, a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179])], [c25, c26])). % 0.13/0.35 % 0.13/0.35 cnf(c29, axiom, % 0.13/0.35 state(p_5,p_4,p_3,p_2,p_1,p_6,p_7,p_8,p_9,p_10,p_11,p_12,p_13,p_14,p_15,p_16,p_17,p_18,p_19,p_20)). % 0.13/0.35 cnf(a180, assumption, % 0.13/0.35 X163 = p_5). % 0.13/0.35 cnf(a181, assumption, % 0.13/0.35 X162 = p_4). % 0.13/0.35 cnf(a182, assumption, % 0.13/0.35 X161 = p_3). % 0.13/0.35 cnf(a183, assumption, % 0.13/0.35 X160 = p_2). % 0.13/0.35 cnf(a184, assumption, % 0.13/0.35 X164 = p_1). % 0.13/0.35 cnf(a185, assumption, % 0.13/0.35 X165 = p_6). % 0.13/0.35 cnf(a186, assumption, % 0.13/0.35 X166 = p_7). % 0.13/0.35 cnf(a187, assumption, % 0.13/0.35 X167 = p_8). % 0.13/0.35 cnf(a188, assumption, % 0.13/0.35 X168 = p_9). % 0.13/0.35 cnf(a189, assumption, % 0.13/0.35 X169 = p_10). % 0.13/0.35 cnf(a190, assumption, % 0.13/0.35 X170 = p_11). % 0.13/0.35 cnf(a191, assumption, % 0.13/0.35 X171 = p_12). % 0.13/0.35 cnf(a192, assumption, % 0.13/0.35 X172 = p_13). % 0.13/0.35 cnf(a193, assumption, % 0.13/0.35 X173 = p_14). % 0.13/0.35 cnf(a194, assumption, % 0.13/0.35 X174 = p_15). % 0.13/0.35 cnf(a195, assumption, % 0.13/0.35 X175 = p_16). % 0.13/0.35 cnf(a196, assumption, % 0.13/0.35 X176 = p_17). % 0.13/0.35 cnf(a197, assumption, % 0.13/0.35 X177 = p_18). % 0.13/0.35 cnf(a198, assumption, % 0.13/0.35 X178 = p_19). % 0.13/0.35 cnf(a199, assumption, % 0.13/0.35 X179 = p_20). % 0.13/0.35 cnf(c30, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199])], [c28, c29])). % 0.13/0.35 cnf(c31, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(strict_predicate_extension, [assumptions([a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199])], [c28, c29])). % 0.13/0.35 % 0.13/0.35 cnf(c32, plain, % 0.13/0.35 $false, % 0.13/0.35 inference(constraint_solving, [ % 0.13/0.35 bind(X0, p_1), % 0.13/0.35 bind(X1, p_2), % 0.13/0.35 bind(X2, p_3), % 0.13/0.35 bind(X3, p_4), % 0.13/0.35 bind(X4, p_5), % 0.13/0.35 bind(X5, p_6), % 0.13/0.35 bind(X6, p_7), % 0.13/0.35 bind(X7, p_8), % 0.13/0.35 bind(X8, p_9), % 0.13/0.35 bind(X9, p_10), % 0.13/0.35 bind(X10, p_11), % 0.13/0.35 bind(X11, p_12), % 0.13/0.35 bind(X12, p_13), % 0.13/0.35 bind(X13, p_14), % 0.13/0.35 bind(X14, p_15), % 0.13/0.35 bind(X15, p_16), % 0.13/0.35 bind(X16, p_17), % 0.13/0.35 bind(X17, p_18), % 0.13/0.35 bind(X18, p_19), % 0.13/0.35 bind(X19, p_20), % 0.13/0.35 bind(X20, p_4), % 0.13/0.35 bind(X21, p_3), % 0.13/0.35 bind(X22, p_2), % 0.13/0.35 bind(X23, p_1), % 0.13/0.35 bind(X24, p_5), % 0.13/0.35 bind(X25, p_6), % 0.13/0.35 bind(X26, p_7), % 0.13/0.35 bind(X27, p_8), % 0.13/0.35 bind(X28, p_9), % 0.13/0.35 bind(X29, p_10), % 0.13/0.35 bind(X30, p_11), % 0.13/0.35 bind(X31, p_12), % 0.13/0.35 bind(X32, p_13), % 0.13/0.35 bind(X33, p_14), % 0.13/0.35 bind(X34, p_15), % 0.13/0.35 bind(X35, p_16), % 0.13/0.35 bind(X36, p_17), % 0.13/0.35 bind(X37, p_18), % 0.13/0.35 bind(X38, p_19), % 0.13/0.35 bind(X39, p_20), % 0.13/0.35 bind(X40, p_3), % 0.13/0.35 bind(X41, p_2), % 0.13/0.35 bind(X42, p_1), % 0.13/0.35 bind(X43, p_5), % 0.13/0.35 bind(X44, p_6), % 0.13/0.35 bind(X45, p_7), % 0.13/0.35 bind(X46, p_8), % 0.13/0.35 bind(X47, p_9), % 0.13/0.35 bind(X48, p_10), % 0.13/0.35 bind(X49, p_11), % 0.13/0.35 bind(X50, p_12), % 0.13/0.35 bind(X51, p_13), % 0.13/0.35 bind(X52, p_14), % 0.13/0.35 bind(X53, p_15), % 0.13/0.35 bind(X54, p_16), % 0.13/0.35 bind(X55, p_17), % 0.13/0.35 bind(X56, p_18), % 0.13/0.35 bind(X57, p_19), % 0.13/0.35 bind(X58, p_20), % 0.13/0.35 bind(X59, p_4), % 0.13/0.35 bind(X60, p_5), % 0.13/0.35 bind(X61, p_1), % 0.13/0.35 bind(X62, p_2), % 0.13/0.35 bind(X63, p_3), % 0.13/0.35 bind(X64, p_6), % 0.13/0.35 bind(X65, p_7), % 0.13/0.35 bind(X66, p_8), % 0.13/0.35 bind(X67, p_9), % 0.13/0.35 bind(X68, p_10), % 0.13/0.35 bind(X69, p_11), % 0.13/0.35 bind(X70, p_12), % 0.13/0.35 bind(X71, p_13), % 0.13/0.35 bind(X72, p_14), % 0.13/0.35 bind(X73, p_15), % 0.13/0.35 bind(X74, p_16), % 0.13/0.35 bind(X75, p_17), % 0.13/0.35 bind(X76, p_18), % 0.13/0.35 bind(X77, p_19), % 0.13/0.35 bind(X78, p_20), % 0.13/0.35 bind(X79, p_4), % 0.13/0.35 bind(X80, p_4), % 0.13/0.35 bind(X81, p_5), % 0.13/0.35 bind(X82, p_1), % 0.13/0.35 bind(X83, p_2), % 0.13/0.35 bind(X84, p_3), % 0.13/0.35 bind(X85, p_6), % 0.13/0.35 bind(X86, p_7), % 0.13/0.35 bind(X87, p_8), % 0.13/0.35 bind(X88, p_9), % 0.13/0.35 bind(X89, p_10), % 0.13/0.35 bind(X90, p_11), % 0.13/0.35 bind(X91, p_12), % 0.13/0.35 bind(X92, p_13), % 0.13/0.35 bind(X93, p_14), % 0.13/0.35 bind(X94, p_15), % 0.13/0.35 bind(X95, p_16), % 0.13/0.35 bind(X96, p_17), % 0.13/0.35 bind(X97, p_18), % 0.13/0.35 bind(X98, p_19), % 0.13/0.35 bind(X99, p_20), % 0.13/0.35 bind(X100, p_2), % 0.13/0.35 bind(X101, p_1), % 0.13/0.35 bind(X102, p_5), % 0.13/0.35 bind(X103, p_4), % 0.13/0.35 bind(X104, p_3), % 0.13/0.35 bind(X105, p_6), % 0.13/0.35 bind(X106, p_7), % 0.13/0.35 bind(X107, p_8), % 0.13/0.35 bind(X108, p_9), % 0.13/0.35 bind(X109, p_10), % 0.13/0.35 bind(X110, p_11), % 0.13/0.35 bind(X111, p_12), % 0.13/0.35 bind(X112, p_13), % 0.13/0.35 bind(X113, p_14), % 0.13/0.35 bind(X114, p_15), % 0.13/0.35 bind(X115, p_16), % 0.13/0.35 bind(X116, p_17), % 0.13/0.35 bind(X117, p_18), % 0.13/0.35 bind(X118, p_19), % 0.13/0.35 bind(X119, p_20), % 0.13/0.35 bind(X120, p_1), % 0.13/0.35 bind(X121, p_5), % 0.13/0.35 bind(X122, p_4), % 0.13/0.35 bind(X123, p_3), % 0.13/0.35 bind(X124, p_6), % 0.13/0.35 bind(X125, p_7), % 0.13/0.35 bind(X126, p_8), % 0.13/0.35 bind(X127, p_9), % 0.13/0.35 bind(X128, p_10), % 0.13/0.35 bind(X129, p_11), % 0.13/0.35 bind(X130, p_12), % 0.13/0.35 bind(X131, p_13), % 0.13/0.35 bind(X132, p_14), % 0.13/0.35 bind(X133, p_15), % 0.13/0.35 bind(X134, p_16), % 0.13/0.35 bind(X135, p_17), % 0.13/0.35 bind(X136, p_18), % 0.13/0.35 bind(X137, p_19), % 0.13/0.35 bind(X138, p_20), % 0.13/0.35 bind(X139, p_2), % 0.13/0.35 bind(X140, p_3), % 0.13/0.35 bind(X141, p_4), % 0.13/0.35 bind(X142, p_5), % 0.13/0.35 bind(X143, p_1), % 0.13/0.35 bind(X144, p_6), % 0.13/0.35 bind(X145, p_7), % 0.13/0.35 bind(X146, p_8), % 0.13/0.35 bind(X147, p_9), % 0.13/0.35 bind(X148, p_10), % 0.13/0.35 bind(X149, p_11), % 0.13/0.35 bind(X150, p_12), % 0.13/0.35 bind(X151, p_13), % 0.13/0.35 bind(X152, p_14), % 0.13/0.35 bind(X153, p_15), % 0.13/0.35 bind(X154, p_16), % 0.13/0.35 bind(X155, p_17), % 0.13/0.35 bind(X156, p_18), % 0.13/0.35 bind(X157, p_19), % 0.13/0.35 bind(X158, p_20), % 0.13/0.35 bind(X159, p_2), % 0.13/0.35 bind(X160, p_2), % 0.13/0.35 bind(X161, p_3), % 0.13/0.35 bind(X162, p_4), % 0.13/0.35 bind(X163, p_5), % 0.13/0.35 bind(X164, p_1), % 0.13/0.35 bind(X165, p_6), % 0.13/0.35 bind(X166, p_7), % 0.13/0.35 bind(X167, p_8), % 0.13/0.35 bind(X168, p_9), % 0.13/0.35 bind(X169, p_10), % 0.13/0.35 bind(X170, p_11), % 0.13/0.35 bind(X171, p_12), % 0.13/0.35 bind(X172, p_13), % 0.13/0.35 bind(X173, p_14), % 0.13/0.35 bind(X174, p_15), % 0.13/0.35 bind(X175, p_16), % 0.13/0.35 bind(X176, p_17), % 0.13/0.35 bind(X177, p_18), % 0.13/0.35 bind(X178, p_19), % 0.13/0.35 bind(X179, p_20) % 0.13/0.35 ], % 0.13/0.35 [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])). % 0.13/0.35 % 0.13/0.35 % SZS output end IncompleteProof %------------------------------------------------------------------------------