%------------------------------------------------------------------------------ % File : lazyCoP---0.1 % Problem : NUM283-1.005 : TPTP v8.1.0. Released v1.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 : n003.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 11:31:56 EDT 2022 % Result : Unsatisfiable 280.50s 35.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM283-1.005 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jul 7 01:08:27 EDT 2022 % 0.13/0.34 % CPUTime : % 280.50/35.53 % SZS status Unsatisfiable % 280.50/35.53 % SZS output begin IncompleteProof % 280.50/35.53 cnf(c0, axiom, % 280.50/35.53 ~factorial(s(s(s(s(s(n0))))),X0)). % 280.50/35.53 cnf(c1, plain, % 280.50/35.53 ~factorial(s(s(s(s(s(n0))))),X0), % 280.50/35.53 inference(start, [], [c0])). % 280.50/35.53 % 280.50/35.53 cnf(c2, axiom, % 280.50/35.53 factorial(s(X1),X2) | ~product(s(X1),X3,X2) | ~factorial(X1,X3)). % 280.50/35.53 cnf(a0, assumption, % 280.50/35.53 s(s(s(s(s(n0))))) = s(X1)). % 280.50/35.53 cnf(a1, assumption, % 280.50/35.53 X0 = X2). % 280.50/35.53 cnf(c3, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a0, a1])], [c1, c2])). % 280.50/35.53 cnf(c4, plain, % 280.50/35.53 ~product(s(X1),X3,X2) | ~factorial(X1,X3), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a0, a1])], [c1, c2])). % 280.50/35.53 % 280.50/35.53 cnf(c5, axiom, % 280.50/35.53 product(s(X4),X5,X6) | ~product(X4,X5,X7) | ~sum(X7,X5,X6)). % 280.50/35.53 cnf(a2, assumption, % 280.50/35.53 s(X1) = s(X4)). % 280.50/35.53 cnf(a3, assumption, % 280.50/35.53 X3 = X5). % 280.50/35.53 cnf(a4, assumption, % 280.50/35.53 X2 = X6). % 280.50/35.53 cnf(c6, plain, % 280.50/35.53 ~factorial(X1,X3), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a2, a3, a4])], [c4, c5])). % 280.50/35.53 cnf(c7, plain, % 280.50/35.53 ~product(X4,X5,X7) | ~sum(X7,X5,X6), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a2, a3, a4])], [c4, c5])). % 280.50/35.53 % 280.50/35.53 cnf(c8, axiom, % 280.50/35.53 product(s(X8),X9,X10) | ~product(X8,X9,X11) | ~sum(X11,X9,X10)). % 280.50/35.53 cnf(a5, assumption, % 280.50/35.53 X4 = s(X8)). % 280.50/35.53 cnf(a6, assumption, % 280.50/35.53 X5 = X9). % 280.50/35.53 cnf(a7, assumption, % 280.50/35.53 X7 = X10). % 280.50/35.53 cnf(c9, plain, % 280.50/35.53 ~sum(X7,X5,X6), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a5, a6, a7])], [c7, c8])). % 280.50/35.53 cnf(c10, plain, % 280.50/35.53 ~product(X8,X9,X11) | ~sum(X11,X9,X10), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a5, a6, a7])], [c7, c8])). % 280.50/35.53 % 280.50/35.53 cnf(c11, axiom, % 280.50/35.53 product(s(X12),X13,X14) | ~product(X12,X13,X15) | ~sum(X15,X13,X14)). % 280.50/35.53 cnf(a8, assumption, % 280.50/35.53 X8 = s(X12)). % 280.50/35.53 cnf(a9, assumption, % 280.50/35.53 X9 = X13). % 280.50/35.53 cnf(a10, assumption, % 280.50/35.53 X11 = X14). % 280.50/35.53 cnf(c12, plain, % 280.50/35.53 ~sum(X11,X9,X10), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a8, a9, a10])], [c10, c11])). % 280.50/35.53 cnf(c13, plain, % 280.50/35.53 ~product(X12,X13,X15) | ~sum(X15,X13,X14), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a8, a9, a10])], [c10, c11])). % 280.50/35.53 % 280.50/35.53 cnf(c14, axiom, % 280.50/35.53 product(s(X16),X17,X18) | ~product(X16,X17,X19) | ~sum(X19,X17,X18)). % 280.50/35.53 cnf(a11, assumption, % 280.50/35.53 X12 = s(X16)). % 280.50/35.53 cnf(a12, assumption, % 280.50/35.53 X13 = X17). % 280.50/35.53 cnf(a13, assumption, % 280.50/35.53 X15 = X18). % 280.50/35.53 cnf(c15, plain, % 280.50/35.53 ~sum(X15,X13,X14), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a11, a12, a13])], [c13, c14])). % 280.50/35.53 cnf(c16, plain, % 280.50/35.53 ~product(X16,X17,X19) | ~sum(X19,X17,X18), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a11, a12, a13])], [c13, c14])). % 280.50/35.53 % 280.50/35.53 cnf(c17, axiom, % 280.50/35.53 product(s(n0),X20,X20)). % 280.50/35.53 cnf(a14, assumption, % 280.50/35.53 X16 = s(n0)). % 280.50/35.53 cnf(a15, assumption, % 280.50/35.53 X17 = X20). % 280.50/35.53 cnf(a16, assumption, % 280.50/35.53 X19 = X20). % 280.50/35.53 cnf(c18, plain, % 280.50/35.53 ~sum(X19,X17,X18), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a14, a15, a16])], [c16, c17])). % 280.50/35.53 cnf(c19, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a14, a15, a16])], [c16, c17])). % 280.50/35.53 % 280.50/35.53 cnf(c20, axiom, % 280.50/35.53 sum(X21,s(X22),s(X23)) | ~sum(X21,X22,X23)). % 280.50/35.53 cnf(a17, assumption, % 280.50/35.53 X19 = X21). % 280.50/35.53 cnf(a18, assumption, % 280.50/35.53 X17 = s(X22)). % 280.50/35.53 cnf(a19, assumption, % 280.50/35.53 X18 = s(X23)). % 280.50/35.53 cnf(c21, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a17, a18, a19])], [c18, c20])). % 280.50/35.53 cnf(c22, plain, % 280.50/35.53 ~sum(X21,X22,X23), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a17, a18, a19])], [c18, c20])). % 280.50/35.53 % 280.50/35.53 cnf(c23, axiom, % 280.50/35.53 sum(X24,s(X25),s(X26)) | ~sum(X24,X25,X26)). % 280.50/35.53 cnf(a20, assumption, % 280.50/35.53 X21 = X24). % 280.50/35.53 cnf(a21, assumption, % 280.50/35.53 X22 = s(X25)). % 280.50/35.53 cnf(a22, assumption, % 280.50/35.53 X23 = s(X26)). % 280.50/35.53 cnf(c24, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a20, a21, a22])], [c22, c23])). % 280.50/35.53 cnf(c25, plain, % 280.50/35.53 ~sum(X24,X25,X26), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a20, a21, a22])], [c22, c23])). % 280.50/35.53 % 280.50/35.53 cnf(c26, axiom, % 280.50/35.53 sum(X27,s(X28),s(X29)) | ~sum(X27,X28,X29)). % 280.50/35.53 cnf(a23, assumption, % 280.50/35.53 X24 = X27). % 280.50/35.53 cnf(a24, assumption, % 280.50/35.53 X25 = s(X28)). % 280.50/35.53 cnf(a25, assumption, % 280.50/35.53 X26 = s(X29)). % 280.50/35.53 cnf(c27, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a23, a24, a25])], [c25, c26])). % 280.50/35.53 cnf(c28, plain, % 280.50/35.53 ~sum(X27,X28,X29), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a23, a24, a25])], [c25, c26])). % 280.50/35.53 % 280.50/35.53 cnf(c29, axiom, % 280.50/35.53 sum(X30,s(X31),s(X32)) | ~sum(X30,X31,X32)). % 280.50/35.53 cnf(a26, assumption, % 280.50/35.53 X27 = X30). % 280.50/35.53 cnf(a27, assumption, % 280.50/35.53 X28 = s(X31)). % 280.50/35.53 cnf(a28, assumption, % 280.50/35.53 X29 = s(X32)). % 280.50/35.53 cnf(c30, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a26, a27, a28])], [c28, c29])). % 280.50/35.53 cnf(c31, plain, % 280.50/35.53 ~sum(X30,X31,X32), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a26, a27, a28])], [c28, c29])). % 280.50/35.53 % 280.50/35.53 cnf(c32, axiom, % 280.50/35.53 sum(X33,s(X34),s(X35)) | ~sum(X33,X34,X35)). % 280.50/35.53 cnf(a29, assumption, % 280.50/35.53 X30 = X33). % 280.50/35.53 cnf(a30, assumption, % 280.50/35.53 X31 = s(X34)). % 280.50/35.53 cnf(a31, assumption, % 280.50/35.53 X32 = s(X35)). % 280.50/35.53 cnf(c33, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a29, a30, a31])], [c31, c32])). % 280.50/35.53 cnf(c34, plain, % 280.50/35.53 ~sum(X33,X34,X35), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a29, a30, a31])], [c31, c32])). % 280.50/35.53 % 280.50/35.53 cnf(c35, axiom, % 280.50/35.53 sum(X36,s(X37),s(X38)) | ~sum(X36,X37,X38)). % 280.50/35.53 cnf(a32, assumption, % 280.50/35.53 X33 = X36). % 280.50/35.53 cnf(a33, assumption, % 280.50/35.53 X34 = s(X37)). % 280.50/35.53 cnf(a34, assumption, % 280.50/35.53 X35 = s(X38)). % 280.50/35.53 cnf(c36, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a32, a33, a34])], [c34, c35])). % 280.50/35.53 cnf(c37, plain, % 280.50/35.53 ~sum(X36,X37,X38), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a32, a33, a34])], [c34, c35])). % 280.50/35.53 % 280.50/35.53 cnf(c38, axiom, % 280.50/35.53 sum(X39,s(X40),s(X41)) | ~sum(X39,X40,X41)). % 280.50/35.53 cnf(a35, assumption, % 280.50/35.53 X36 = X39). % 280.50/35.53 cnf(a36, assumption, % 280.50/35.53 X37 = s(X40)). % 280.50/35.53 cnf(a37, assumption, % 280.50/35.53 X38 = s(X41)). % 280.50/35.53 cnf(c39, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a35, a36, a37])], [c37, c38])). % 280.50/35.53 cnf(c40, plain, % 280.50/35.53 ~sum(X39,X40,X41), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a35, a36, a37])], [c37, c38])). % 280.50/35.53 % 280.50/35.53 cnf(c41, axiom, % 280.50/35.53 sum(X42,s(X43),s(X44)) | ~sum(X42,X43,X44)). % 280.50/35.53 cnf(a38, assumption, % 280.50/35.53 X39 = X42). % 280.50/35.53 cnf(a39, assumption, % 280.50/35.53 X40 = s(X43)). % 280.50/35.53 cnf(a40, assumption, % 280.50/35.53 X41 = s(X44)). % 280.50/35.53 cnf(c42, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a38, a39, a40])], [c40, c41])). % 280.50/35.53 cnf(c43, plain, % 280.50/35.53 ~sum(X42,X43,X44), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a38, a39, a40])], [c40, c41])). % 280.50/35.53 % 280.50/35.53 cnf(c44, axiom, % 280.50/35.53 sum(X45,s(X46),s(X47)) | ~sum(X45,X46,X47)). % 280.50/35.53 cnf(a41, assumption, % 280.50/35.53 X42 = X45). % 280.50/35.53 cnf(a42, assumption, % 280.50/35.53 X43 = s(X46)). % 280.50/35.53 cnf(a43, assumption, % 280.50/35.53 X44 = s(X47)). % 280.50/35.53 cnf(c45, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a41, a42, a43])], [c43, c44])). % 280.50/35.53 cnf(c46, plain, % 280.50/35.53 ~sum(X45,X46,X47), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a41, a42, a43])], [c43, c44])). % 280.50/35.53 % 280.50/35.53 cnf(c47, axiom, % 280.50/35.53 sum(X48,s(X49),s(X50)) | ~sum(X48,X49,X50)). % 280.50/35.53 cnf(a44, assumption, % 280.50/35.53 X45 = X48). % 280.50/35.53 cnf(a45, assumption, % 280.50/35.53 X46 = s(X49)). % 280.50/35.53 cnf(a46, assumption, % 280.50/35.53 X47 = s(X50)). % 280.50/35.53 cnf(c48, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a44, a45, a46])], [c46, c47])). % 280.50/35.53 cnf(c49, plain, % 280.50/35.53 ~sum(X48,X49,X50), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a44, a45, a46])], [c46, c47])). % 280.50/35.53 % 280.50/35.53 cnf(c50, axiom, % 280.50/35.53 sum(X51,s(X52),s(X53)) | ~sum(X51,X52,X53)). % 280.50/35.53 cnf(a47, assumption, % 280.50/35.53 X48 = X51). % 280.50/35.53 cnf(a48, assumption, % 280.50/35.53 X49 = s(X52)). % 280.50/35.53 cnf(a49, assumption, % 280.50/35.53 X50 = s(X53)). % 280.50/35.53 cnf(c51, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a47, a48, a49])], [c49, c50])). % 280.50/35.53 cnf(c52, plain, % 280.50/35.53 ~sum(X51,X52,X53), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a47, a48, a49])], [c49, c50])). % 280.50/35.53 % 280.50/35.53 cnf(c53, axiom, % 280.50/35.53 sum(X54,s(X55),s(X56)) | ~sum(X54,X55,X56)). % 280.50/35.53 cnf(a50, assumption, % 280.50/35.53 X51 = X54). % 280.50/35.53 cnf(a51, assumption, % 280.50/35.53 X52 = s(X55)). % 280.50/35.53 cnf(a52, assumption, % 280.50/35.53 X53 = s(X56)). % 280.50/35.53 cnf(c54, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a50, a51, a52])], [c52, c53])). % 280.50/35.53 cnf(c55, plain, % 280.50/35.53 ~sum(X54,X55,X56), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a50, a51, a52])], [c52, c53])). % 280.50/35.53 % 280.50/35.53 cnf(c56, axiom, % 280.50/35.53 sum(X57,s(X58),s(X59)) | ~sum(X57,X58,X59)). % 280.50/35.53 cnf(a53, assumption, % 280.50/35.53 X54 = X57). % 280.50/35.53 cnf(a54, assumption, % 280.50/35.53 X55 = s(X58)). % 280.50/35.53 cnf(a55, assumption, % 280.50/35.53 X56 = s(X59)). % 280.50/35.53 cnf(c57, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a53, a54, a55])], [c55, c56])). % 280.50/35.53 cnf(c58, plain, % 280.50/35.53 ~sum(X57,X58,X59), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a53, a54, a55])], [c55, c56])). % 280.50/35.53 % 280.50/35.53 cnf(c59, axiom, % 280.50/35.53 sum(X60,s(X61),s(X62)) | ~sum(X60,X61,X62)). % 280.50/35.53 cnf(a56, assumption, % 280.50/35.53 X57 = X60). % 280.50/35.53 cnf(a57, assumption, % 280.50/35.53 X58 = s(X61)). % 280.50/35.53 cnf(a58, assumption, % 280.50/35.53 X59 = s(X62)). % 280.50/35.53 cnf(c60, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a56, a57, a58])], [c58, c59])). % 280.50/35.53 cnf(c61, plain, % 280.50/35.53 ~sum(X60,X61,X62), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a56, a57, a58])], [c58, c59])). % 280.50/35.53 % 280.50/35.53 cnf(c62, axiom, % 280.50/35.53 sum(X63,s(X64),s(X65)) | ~sum(X63,X64,X65)). % 280.50/35.53 cnf(a59, assumption, % 280.50/35.53 X60 = X63). % 280.50/35.53 cnf(a60, assumption, % 280.50/35.53 X61 = s(X64)). % 280.50/35.53 cnf(a61, assumption, % 280.50/35.53 X62 = s(X65)). % 280.50/35.53 cnf(c63, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a59, a60, a61])], [c61, c62])). % 280.50/35.53 cnf(c64, plain, % 280.50/35.53 ~sum(X63,X64,X65), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a59, a60, a61])], [c61, c62])). % 280.50/35.53 % 280.50/35.53 cnf(c65, axiom, % 280.50/35.53 sum(X66,s(X67),s(X68)) | ~sum(X66,X67,X68)). % 280.50/35.53 cnf(a62, assumption, % 280.50/35.53 X63 = X66). % 280.50/35.53 cnf(a63, assumption, % 280.50/35.53 X64 = s(X67)). % 280.50/35.53 cnf(a64, assumption, % 280.50/35.53 X65 = s(X68)). % 280.50/35.53 cnf(c66, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a62, a63, a64])], [c64, c65])). % 280.50/35.53 cnf(c67, plain, % 280.50/35.53 ~sum(X66,X67,X68), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a62, a63, a64])], [c64, c65])). % 280.50/35.53 % 280.50/35.53 cnf(c68, axiom, % 280.50/35.53 sum(X69,s(X70),s(X71)) | ~sum(X69,X70,X71)). % 280.50/35.53 cnf(a65, assumption, % 280.50/35.53 X66 = X69). % 280.50/35.53 cnf(a66, assumption, % 280.50/35.53 X67 = s(X70)). % 280.50/35.53 cnf(a67, assumption, % 280.50/35.53 X68 = s(X71)). % 280.50/35.53 cnf(c69, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a65, a66, a67])], [c67, c68])). % 280.50/35.53 cnf(c70, plain, % 280.50/35.53 ~sum(X69,X70,X71), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a65, a66, a67])], [c67, c68])). % 280.50/35.53 % 280.50/35.53 cnf(c71, axiom, % 280.50/35.53 sum(X72,s(X73),s(X74)) | ~sum(X72,X73,X74)). % 280.50/35.53 cnf(a68, assumption, % 280.50/35.53 X69 = X72). % 280.50/35.53 cnf(a69, assumption, % 280.50/35.53 X70 = s(X73)). % 280.50/35.53 cnf(a70, assumption, % 280.50/35.53 X71 = s(X74)). % 280.50/35.53 cnf(c72, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a68, a69, a70])], [c70, c71])). % 280.50/35.53 cnf(c73, plain, % 280.50/35.53 ~sum(X72,X73,X74), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a68, a69, a70])], [c70, c71])). % 280.50/35.53 % 280.50/35.53 cnf(c74, axiom, % 280.50/35.53 sum(X75,s(X76),s(X77)) | ~sum(X75,X76,X77)). % 280.50/35.53 cnf(a71, assumption, % 280.50/35.53 X72 = X75). % 280.50/35.53 cnf(a72, assumption, % 280.50/35.53 X73 = s(X76)). % 280.50/35.53 cnf(a73, assumption, % 280.50/35.53 X74 = s(X77)). % 280.50/35.53 cnf(c75, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a71, a72, a73])], [c73, c74])). % 280.50/35.53 cnf(c76, plain, % 280.50/35.53 ~sum(X75,X76,X77), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a71, a72, a73])], [c73, c74])). % 280.50/35.53 % 280.50/35.53 cnf(c77, axiom, % 280.50/35.53 sum(X78,s(X79),s(X80)) | ~sum(X78,X79,X80)). % 280.50/35.53 cnf(a74, assumption, % 280.50/35.53 X75 = X78). % 280.50/35.53 cnf(a75, assumption, % 280.50/35.53 X76 = s(X79)). % 280.50/35.53 cnf(a76, assumption, % 280.50/35.53 X77 = s(X80)). % 280.50/35.53 cnf(c78, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a74, a75, a76])], [c76, c77])). % 280.50/35.53 cnf(c79, plain, % 280.50/35.53 ~sum(X78,X79,X80), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a74, a75, a76])], [c76, c77])). % 280.50/35.53 % 280.50/35.53 cnf(c80, axiom, % 280.50/35.53 sum(X81,s(X82),s(X83)) | ~sum(X81,X82,X83)). % 280.50/35.53 cnf(a77, assumption, % 280.50/35.53 X78 = X81). % 280.50/35.53 cnf(a78, assumption, % 280.50/35.53 X79 = s(X82)). % 280.50/35.53 cnf(a79, assumption, % 280.50/35.53 X80 = s(X83)). % 280.50/35.53 cnf(c81, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a77, a78, a79])], [c79, c80])). % 280.50/35.53 cnf(c82, plain, % 280.50/35.53 ~sum(X81,X82,X83), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a77, a78, a79])], [c79, c80])). % 280.50/35.53 % 280.50/35.53 cnf(c83, axiom, % 280.50/35.53 sum(X84,s(X85),s(X86)) | ~sum(X84,X85,X86)). % 280.50/35.53 cnf(a80, assumption, % 280.50/35.53 X81 = X84). % 280.50/35.53 cnf(a81, assumption, % 280.50/35.53 X82 = s(X85)). % 280.50/35.53 cnf(a82, assumption, % 280.50/35.53 X83 = s(X86)). % 280.50/35.53 cnf(c84, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a80, a81, a82])], [c82, c83])). % 280.50/35.53 cnf(c85, plain, % 280.50/35.53 ~sum(X84,X85,X86), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a80, a81, a82])], [c82, c83])). % 280.50/35.53 % 280.50/35.53 cnf(c86, axiom, % 280.50/35.53 sum(X87,s(X88),s(X89)) | ~sum(X87,X88,X89)). % 280.50/35.53 cnf(a83, assumption, % 280.50/35.53 X84 = X87). % 280.50/35.53 cnf(a84, assumption, % 280.50/35.53 X85 = s(X88)). % 280.50/35.53 cnf(a85, assumption, % 280.50/35.53 X86 = s(X89)). % 280.50/35.53 cnf(c87, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a83, a84, a85])], [c85, c86])). % 280.50/35.53 cnf(c88, plain, % 280.50/35.53 ~sum(X87,X88,X89), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a83, a84, a85])], [c85, c86])). % 280.50/35.53 % 280.50/35.53 cnf(c89, axiom, % 280.50/35.53 sum(X90,s(X91),s(X92)) | ~sum(X90,X91,X92)). % 280.50/35.53 cnf(a86, assumption, % 280.50/35.53 X87 = X90). % 280.50/35.53 cnf(a87, assumption, % 280.50/35.53 X88 = s(X91)). % 280.50/35.53 cnf(a88, assumption, % 280.50/35.53 X89 = s(X92)). % 280.50/35.53 cnf(c90, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a86, a87, a88])], [c88, c89])). % 280.50/35.53 cnf(c91, plain, % 280.50/35.53 ~sum(X90,X91,X92), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a86, a87, a88])], [c88, c89])). % 280.50/35.53 % 280.50/35.53 cnf(c92, axiom, % 280.50/35.53 sum(X93,n0,X93)). % 280.50/35.53 cnf(a89, assumption, % 280.50/35.53 X90 = X93). % 280.50/35.53 cnf(a90, assumption, % 280.50/35.53 X91 = n0). % 280.50/35.53 cnf(a91, assumption, % 280.50/35.53 X92 = X93). % 280.50/35.53 cnf(c93, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a89, a90, a91])], [c91, c92])). % 280.50/35.53 cnf(c94, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a89, a90, a91])], [c91, c92])). % 280.50/35.53 % 280.50/35.53 cnf(c95, axiom, % 280.50/35.53 sum(X94,s(X95),s(X96)) | ~sum(X94,X95,X96)). % 280.50/35.53 cnf(a92, assumption, % 280.50/35.53 X15 = X94). % 280.50/35.53 cnf(a93, assumption, % 280.50/35.53 X13 = s(X95)). % 280.50/35.53 cnf(a94, assumption, % 280.50/35.53 X14 = s(X96)). % 280.50/35.53 cnf(c96, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a92, a93, a94])], [c15, c95])). % 280.50/35.53 cnf(c97, plain, % 280.50/35.53 ~sum(X94,X95,X96), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a92, a93, a94])], [c15, c95])). % 280.50/35.53 % 280.50/35.53 cnf(c98, axiom, % 280.50/35.53 sum(X97,s(X98),s(X99)) | ~sum(X97,X98,X99)). % 280.50/35.53 cnf(a95, assumption, % 280.50/35.53 X94 = X97). % 280.50/35.53 cnf(a96, assumption, % 280.50/35.53 X95 = s(X98)). % 280.50/35.53 cnf(a97, assumption, % 280.50/35.53 X96 = s(X99)). % 280.50/35.53 cnf(c99, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a95, a96, a97])], [c97, c98])). % 280.50/35.53 cnf(c100, plain, % 280.50/35.53 ~sum(X97,X98,X99), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a95, a96, a97])], [c97, c98])). % 280.50/35.53 % 280.50/35.53 cnf(c101, axiom, % 280.50/35.53 sum(X100,s(X101),s(X102)) | ~sum(X100,X101,X102)). % 280.50/35.53 cnf(a98, assumption, % 280.50/35.53 X97 = X100). % 280.50/35.53 cnf(a99, assumption, % 280.50/35.53 X98 = s(X101)). % 280.50/35.53 cnf(a100, assumption, % 280.50/35.53 X99 = s(X102)). % 280.50/35.53 cnf(c102, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a98, a99, a100])], [c100, c101])). % 280.50/35.53 cnf(c103, plain, % 280.50/35.53 ~sum(X100,X101,X102), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a98, a99, a100])], [c100, c101])). % 280.50/35.53 % 280.50/35.53 cnf(c104, axiom, % 280.50/35.53 sum(X103,s(X104),s(X105)) | ~sum(X103,X104,X105)). % 280.50/35.53 cnf(a101, assumption, % 280.50/35.53 X100 = X103). % 280.50/35.53 cnf(a102, assumption, % 280.50/35.53 X101 = s(X104)). % 280.50/35.53 cnf(a103, assumption, % 280.50/35.53 X102 = s(X105)). % 280.50/35.53 cnf(c105, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a101, a102, a103])], [c103, c104])). % 280.50/35.53 cnf(c106, plain, % 280.50/35.53 ~sum(X103,X104,X105), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a101, a102, a103])], [c103, c104])). % 280.50/35.53 % 280.50/35.53 cnf(c107, axiom, % 280.50/35.53 sum(X106,s(X107),s(X108)) | ~sum(X106,X107,X108)). % 280.50/35.53 cnf(a104, assumption, % 280.50/35.53 X103 = X106). % 280.50/35.53 cnf(a105, assumption, % 280.50/35.53 X104 = s(X107)). % 280.50/35.53 cnf(a106, assumption, % 280.50/35.53 X105 = s(X108)). % 280.50/35.53 cnf(c108, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a104, a105, a106])], [c106, c107])). % 280.50/35.53 cnf(c109, plain, % 280.50/35.53 ~sum(X106,X107,X108), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a104, a105, a106])], [c106, c107])). % 280.50/35.53 % 280.50/35.53 cnf(c110, axiom, % 280.50/35.53 sum(X109,s(X110),s(X111)) | ~sum(X109,X110,X111)). % 280.50/35.53 cnf(a107, assumption, % 280.50/35.53 X106 = X109). % 280.50/35.53 cnf(a108, assumption, % 280.50/35.53 X107 = s(X110)). % 280.50/35.53 cnf(a109, assumption, % 280.50/35.53 X108 = s(X111)). % 280.50/35.53 cnf(c111, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a107, a108, a109])], [c109, c110])). % 280.50/35.53 cnf(c112, plain, % 280.50/35.53 ~sum(X109,X110,X111), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a107, a108, a109])], [c109, c110])). % 280.50/35.53 % 280.50/35.53 cnf(c113, axiom, % 280.50/35.53 sum(X112,s(X113),s(X114)) | ~sum(X112,X113,X114)). % 280.50/35.53 cnf(a110, assumption, % 280.50/35.53 X109 = X112). % 280.50/35.53 cnf(a111, assumption, % 280.50/35.53 X110 = s(X113)). % 280.50/35.53 cnf(a112, assumption, % 280.50/35.53 X111 = s(X114)). % 280.50/35.53 cnf(c114, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a110, a111, a112])], [c112, c113])). % 280.50/35.53 cnf(c115, plain, % 280.50/35.53 ~sum(X112,X113,X114), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a110, a111, a112])], [c112, c113])). % 280.50/35.53 % 280.50/35.53 cnf(c116, axiom, % 280.50/35.53 sum(X115,s(X116),s(X117)) | ~sum(X115,X116,X117)). % 280.50/35.53 cnf(a113, assumption, % 280.50/35.53 X112 = X115). % 280.50/35.53 cnf(a114, assumption, % 280.50/35.53 X113 = s(X116)). % 280.50/35.53 cnf(a115, assumption, % 280.50/35.53 X114 = s(X117)). % 280.50/35.53 cnf(c117, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a113, a114, a115])], [c115, c116])). % 280.50/35.53 cnf(c118, plain, % 280.50/35.53 ~sum(X115,X116,X117), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a113, a114, a115])], [c115, c116])). % 280.50/35.53 % 280.50/35.53 cnf(c119, axiom, % 280.50/35.53 sum(X118,s(X119),s(X120)) | ~sum(X118,X119,X120)). % 280.50/35.53 cnf(a116, assumption, % 280.50/35.53 X115 = X118). % 280.50/35.53 cnf(a117, assumption, % 280.50/35.53 X116 = s(X119)). % 280.50/35.53 cnf(a118, assumption, % 280.50/35.53 X117 = s(X120)). % 280.50/35.53 cnf(c120, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a116, a117, a118])], [c118, c119])). % 280.50/35.53 cnf(c121, plain, % 280.50/35.53 ~sum(X118,X119,X120), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a116, a117, a118])], [c118, c119])). % 280.50/35.53 % 280.50/35.53 cnf(c122, axiom, % 280.50/35.53 sum(X121,s(X122),s(X123)) | ~sum(X121,X122,X123)). % 280.50/35.53 cnf(a119, assumption, % 280.50/35.53 X118 = X121). % 280.50/35.53 cnf(a120, assumption, % 280.50/35.53 X119 = s(X122)). % 280.50/35.53 cnf(a121, assumption, % 280.50/35.53 X120 = s(X123)). % 280.50/35.53 cnf(c123, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a119, a120, a121])], [c121, c122])). % 280.50/35.53 cnf(c124, plain, % 280.50/35.53 ~sum(X121,X122,X123), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a119, a120, a121])], [c121, c122])). % 280.50/35.53 % 280.50/35.53 cnf(c125, axiom, % 280.50/35.53 sum(X124,s(X125),s(X126)) | ~sum(X124,X125,X126)). % 280.50/35.53 cnf(a122, assumption, % 280.50/35.53 X121 = X124). % 280.50/35.53 cnf(a123, assumption, % 280.50/35.53 X122 = s(X125)). % 280.50/35.53 cnf(a124, assumption, % 280.50/35.53 X123 = s(X126)). % 280.50/35.53 cnf(c126, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a122, a123, a124])], [c124, c125])). % 280.50/35.53 cnf(c127, plain, % 280.50/35.53 ~sum(X124,X125,X126), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a122, a123, a124])], [c124, c125])). % 280.50/35.53 % 280.50/35.53 cnf(c128, axiom, % 280.50/35.53 sum(X127,s(X128),s(X129)) | ~sum(X127,X128,X129)). % 280.50/35.53 cnf(a125, assumption, % 280.50/35.53 X124 = X127). % 280.50/35.53 cnf(a126, assumption, % 280.50/35.53 X125 = s(X128)). % 280.50/35.53 cnf(a127, assumption, % 280.50/35.53 X126 = s(X129)). % 280.50/35.53 cnf(c129, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a125, a126, a127])], [c127, c128])). % 280.50/35.53 cnf(c130, plain, % 280.50/35.53 ~sum(X127,X128,X129), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a125, a126, a127])], [c127, c128])). % 280.50/35.53 % 280.50/35.53 cnf(c131, axiom, % 280.50/35.53 sum(X130,s(X131),s(X132)) | ~sum(X130,X131,X132)). % 280.50/35.53 cnf(a128, assumption, % 280.50/35.53 X127 = X130). % 280.50/35.53 cnf(a129, assumption, % 280.50/35.53 X128 = s(X131)). % 280.50/35.53 cnf(a130, assumption, % 280.50/35.53 X129 = s(X132)). % 280.50/35.53 cnf(c132, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a128, a129, a130])], [c130, c131])). % 280.50/35.53 cnf(c133, plain, % 280.50/35.53 ~sum(X130,X131,X132), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a128, a129, a130])], [c130, c131])). % 280.50/35.53 % 280.50/35.53 cnf(c134, axiom, % 280.50/35.53 sum(X133,s(X134),s(X135)) | ~sum(X133,X134,X135)). % 280.50/35.53 cnf(a131, assumption, % 280.50/35.53 X130 = X133). % 280.50/35.53 cnf(a132, assumption, % 280.50/35.53 X131 = s(X134)). % 280.50/35.53 cnf(a133, assumption, % 280.50/35.53 X132 = s(X135)). % 280.50/35.53 cnf(c135, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a131, a132, a133])], [c133, c134])). % 280.50/35.53 cnf(c136, plain, % 280.50/35.53 ~sum(X133,X134,X135), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a131, a132, a133])], [c133, c134])). % 280.50/35.53 % 280.50/35.53 cnf(c137, axiom, % 280.50/35.53 sum(X136,s(X137),s(X138)) | ~sum(X136,X137,X138)). % 280.50/35.53 cnf(a134, assumption, % 280.50/35.53 X133 = X136). % 280.50/35.53 cnf(a135, assumption, % 280.50/35.53 X134 = s(X137)). % 280.50/35.53 cnf(a136, assumption, % 280.50/35.53 X135 = s(X138)). % 280.50/35.53 cnf(c138, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a134, a135, a136])], [c136, c137])). % 280.50/35.53 cnf(c139, plain, % 280.50/35.53 ~sum(X136,X137,X138), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a134, a135, a136])], [c136, c137])). % 280.50/35.53 % 280.50/35.53 cnf(c140, axiom, % 280.50/35.53 sum(X139,s(X140),s(X141)) | ~sum(X139,X140,X141)). % 280.50/35.53 cnf(a137, assumption, % 280.50/35.53 X136 = X139). % 280.50/35.53 cnf(a138, assumption, % 280.50/35.53 X137 = s(X140)). % 280.50/35.53 cnf(a139, assumption, % 280.50/35.53 X138 = s(X141)). % 280.50/35.53 cnf(c141, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a137, a138, a139])], [c139, c140])). % 280.50/35.53 cnf(c142, plain, % 280.50/35.53 ~sum(X139,X140,X141), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a137, a138, a139])], [c139, c140])). % 280.50/35.53 % 280.50/35.53 cnf(c143, axiom, % 280.50/35.53 sum(X142,s(X143),s(X144)) | ~sum(X142,X143,X144)). % 280.50/35.53 cnf(a140, assumption, % 280.50/35.53 X139 = X142). % 280.50/35.53 cnf(a141, assumption, % 280.50/35.53 X140 = s(X143)). % 280.50/35.53 cnf(a142, assumption, % 280.50/35.53 X141 = s(X144)). % 280.50/35.53 cnf(c144, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a140, a141, a142])], [c142, c143])). % 280.50/35.53 cnf(c145, plain, % 280.50/35.53 ~sum(X142,X143,X144), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a140, a141, a142])], [c142, c143])). % 280.50/35.53 % 280.50/35.53 cnf(c146, axiom, % 280.50/35.53 sum(X145,s(X146),s(X147)) | ~sum(X145,X146,X147)). % 280.50/35.53 cnf(a143, assumption, % 280.50/35.53 X142 = X145). % 280.50/35.53 cnf(a144, assumption, % 280.50/35.53 X143 = s(X146)). % 280.50/35.53 cnf(a145, assumption, % 280.50/35.53 X144 = s(X147)). % 280.50/35.53 cnf(c147, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a143, a144, a145])], [c145, c146])). % 280.50/35.53 cnf(c148, plain, % 280.50/35.53 ~sum(X145,X146,X147), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a143, a144, a145])], [c145, c146])). % 280.50/35.53 % 280.50/35.53 cnf(c149, axiom, % 280.50/35.53 sum(X148,s(X149),s(X150)) | ~sum(X148,X149,X150)). % 280.50/35.53 cnf(a146, assumption, % 280.50/35.53 X145 = X148). % 280.50/35.53 cnf(a147, assumption, % 280.50/35.53 X146 = s(X149)). % 280.50/35.53 cnf(a148, assumption, % 280.50/35.53 X147 = s(X150)). % 280.50/35.53 cnf(c150, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a146, a147, a148])], [c148, c149])). % 280.50/35.53 cnf(c151, plain, % 280.50/35.53 ~sum(X148,X149,X150), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a146, a147, a148])], [c148, c149])). % 280.50/35.53 % 280.50/35.53 cnf(c152, axiom, % 280.50/35.53 sum(X151,s(X152),s(X153)) | ~sum(X151,X152,X153)). % 280.50/35.53 cnf(a149, assumption, % 280.50/35.53 X148 = X151). % 280.50/35.53 cnf(a150, assumption, % 280.50/35.53 X149 = s(X152)). % 280.50/35.53 cnf(a151, assumption, % 280.50/35.53 X150 = s(X153)). % 280.50/35.53 cnf(c153, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a149, a150, a151])], [c151, c152])). % 280.50/35.53 cnf(c154, plain, % 280.50/35.53 ~sum(X151,X152,X153), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a149, a150, a151])], [c151, c152])). % 280.50/35.53 % 280.50/35.53 cnf(c155, axiom, % 280.50/35.53 sum(X154,s(X155),s(X156)) | ~sum(X154,X155,X156)). % 280.50/35.53 cnf(a152, assumption, % 280.50/35.53 X151 = X154). % 280.50/35.53 cnf(a153, assumption, % 280.50/35.53 X152 = s(X155)). % 280.50/35.53 cnf(a154, assumption, % 280.50/35.53 X153 = s(X156)). % 280.50/35.53 cnf(c156, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a152, a153, a154])], [c154, c155])). % 280.50/35.53 cnf(c157, plain, % 280.50/35.53 ~sum(X154,X155,X156), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a152, a153, a154])], [c154, c155])). % 280.50/35.53 % 280.50/35.53 cnf(c158, axiom, % 280.50/35.53 sum(X157,s(X158),s(X159)) | ~sum(X157,X158,X159)). % 280.50/35.53 cnf(a155, assumption, % 280.50/35.53 X154 = X157). % 280.50/35.53 cnf(a156, assumption, % 280.50/35.53 X155 = s(X158)). % 280.50/35.53 cnf(a157, assumption, % 280.50/35.53 X156 = s(X159)). % 280.50/35.53 cnf(c159, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a155, a156, a157])], [c157, c158])). % 280.50/35.53 cnf(c160, plain, % 280.50/35.53 ~sum(X157,X158,X159), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a155, a156, a157])], [c157, c158])). % 280.50/35.53 % 280.50/35.53 cnf(c161, axiom, % 280.50/35.53 sum(X160,s(X161),s(X162)) | ~sum(X160,X161,X162)). % 280.50/35.53 cnf(a158, assumption, % 280.50/35.53 X157 = X160). % 280.50/35.53 cnf(a159, assumption, % 280.50/35.53 X158 = s(X161)). % 280.50/35.53 cnf(a160, assumption, % 280.50/35.53 X159 = s(X162)). % 280.50/35.53 cnf(c162, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a158, a159, a160])], [c160, c161])). % 280.50/35.53 cnf(c163, plain, % 280.50/35.53 ~sum(X160,X161,X162), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a158, a159, a160])], [c160, c161])). % 280.50/35.53 % 280.50/35.53 cnf(c164, axiom, % 280.50/35.53 sum(X163,s(X164),s(X165)) | ~sum(X163,X164,X165)). % 280.50/35.53 cnf(a161, assumption, % 280.50/35.53 X160 = X163). % 280.50/35.53 cnf(a162, assumption, % 280.50/35.53 X161 = s(X164)). % 280.50/35.53 cnf(a163, assumption, % 280.50/35.53 X162 = s(X165)). % 280.50/35.53 cnf(c165, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a161, a162, a163])], [c163, c164])). % 280.50/35.53 cnf(c166, plain, % 280.50/35.53 ~sum(X163,X164,X165), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a161, a162, a163])], [c163, c164])). % 280.50/35.53 % 280.50/35.53 cnf(c167, axiom, % 280.50/35.53 sum(X166,n0,X166)). % 280.50/35.53 cnf(a164, assumption, % 280.50/35.53 X163 = X166). % 280.50/35.53 cnf(a165, assumption, % 280.50/35.53 X164 = n0). % 280.50/35.53 cnf(a166, assumption, % 280.50/35.53 X165 = X166). % 280.50/35.53 cnf(c168, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a164, a165, a166])], [c166, c167])). % 280.50/35.53 cnf(c169, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a164, a165, a166])], [c166, c167])). % 280.50/35.53 % 280.50/35.53 cnf(c170, axiom, % 280.50/35.53 sum(X167,s(X168),s(X169)) | ~sum(X167,X168,X169)). % 280.50/35.53 cnf(a167, assumption, % 280.50/35.53 X11 = X167). % 280.50/35.53 cnf(a168, assumption, % 280.50/35.53 X9 = s(X168)). % 280.50/35.53 cnf(a169, assumption, % 280.50/35.53 X10 = s(X169)). % 280.50/35.53 cnf(c171, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a167, a168, a169])], [c12, c170])). % 280.50/35.53 cnf(c172, plain, % 280.50/35.53 ~sum(X167,X168,X169), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a167, a168, a169])], [c12, c170])). % 280.50/35.53 % 280.50/35.53 cnf(c173, axiom, % 280.50/35.53 sum(X170,s(X171),s(X172)) | ~sum(X170,X171,X172)). % 280.50/35.53 cnf(a170, assumption, % 280.50/35.53 X167 = X170). % 280.50/35.53 cnf(a171, assumption, % 280.50/35.53 X168 = s(X171)). % 280.50/35.53 cnf(a172, assumption, % 280.50/35.53 X169 = s(X172)). % 280.50/35.53 cnf(c174, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a170, a171, a172])], [c172, c173])). % 280.50/35.53 cnf(c175, plain, % 280.50/35.53 ~sum(X170,X171,X172), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a170, a171, a172])], [c172, c173])). % 280.50/35.53 % 280.50/35.53 cnf(c176, axiom, % 280.50/35.53 sum(X173,s(X174),s(X175)) | ~sum(X173,X174,X175)). % 280.50/35.53 cnf(a173, assumption, % 280.50/35.53 X170 = X173). % 280.50/35.53 cnf(a174, assumption, % 280.50/35.53 X171 = s(X174)). % 280.50/35.53 cnf(a175, assumption, % 280.50/35.53 X172 = s(X175)). % 280.50/35.53 cnf(c177, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a173, a174, a175])], [c175, c176])). % 280.50/35.53 cnf(c178, plain, % 280.50/35.53 ~sum(X173,X174,X175), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a173, a174, a175])], [c175, c176])). % 280.50/35.53 % 280.50/35.53 cnf(c179, axiom, % 280.50/35.53 sum(X176,s(X177),s(X178)) | ~sum(X176,X177,X178)). % 280.50/35.53 cnf(a176, assumption, % 280.50/35.53 X173 = X176). % 280.50/35.53 cnf(a177, assumption, % 280.50/35.53 X174 = s(X177)). % 280.50/35.53 cnf(a178, assumption, % 280.50/35.53 X175 = s(X178)). % 280.50/35.53 cnf(c180, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a176, a177, a178])], [c178, c179])). % 280.50/35.53 cnf(c181, plain, % 280.50/35.53 ~sum(X176,X177,X178), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a176, a177, a178])], [c178, c179])). % 280.50/35.53 % 280.50/35.53 cnf(c182, axiom, % 280.50/35.53 sum(X179,s(X180),s(X181)) | ~sum(X179,X180,X181)). % 280.50/35.53 cnf(a179, assumption, % 280.50/35.53 X176 = X179). % 280.50/35.53 cnf(a180, assumption, % 280.50/35.53 X177 = s(X180)). % 280.50/35.53 cnf(a181, assumption, % 280.50/35.53 X178 = s(X181)). % 280.50/35.53 cnf(c183, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a179, a180, a181])], [c181, c182])). % 280.50/35.53 cnf(c184, plain, % 280.50/35.53 ~sum(X179,X180,X181), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a179, a180, a181])], [c181, c182])). % 280.50/35.53 % 280.50/35.53 cnf(c185, axiom, % 280.50/35.53 sum(X182,s(X183),s(X184)) | ~sum(X182,X183,X184)). % 280.50/35.53 cnf(a182, assumption, % 280.50/35.53 X179 = X182). % 280.50/35.53 cnf(a183, assumption, % 280.50/35.53 X180 = s(X183)). % 280.50/35.53 cnf(a184, assumption, % 280.50/35.53 X181 = s(X184)). % 280.50/35.53 cnf(c186, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a182, a183, a184])], [c184, c185])). % 280.50/35.53 cnf(c187, plain, % 280.50/35.53 ~sum(X182,X183,X184), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a182, a183, a184])], [c184, c185])). % 280.50/35.53 % 280.50/35.53 cnf(c188, axiom, % 280.50/35.53 sum(X185,s(X186),s(X187)) | ~sum(X185,X186,X187)). % 280.50/35.53 cnf(a185, assumption, % 280.50/35.53 X182 = X185). % 280.50/35.53 cnf(a186, assumption, % 280.50/35.53 X183 = s(X186)). % 280.50/35.53 cnf(a187, assumption, % 280.50/35.53 X184 = s(X187)). % 280.50/35.53 cnf(c189, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a185, a186, a187])], [c187, c188])). % 280.50/35.53 cnf(c190, plain, % 280.50/35.53 ~sum(X185,X186,X187), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a185, a186, a187])], [c187, c188])). % 280.50/35.53 % 280.50/35.53 cnf(c191, axiom, % 280.50/35.53 sum(X188,s(X189),s(X190)) | ~sum(X188,X189,X190)). % 280.50/35.53 cnf(a188, assumption, % 280.50/35.53 X185 = X188). % 280.50/35.53 cnf(a189, assumption, % 280.50/35.53 X186 = s(X189)). % 280.50/35.53 cnf(a190, assumption, % 280.50/35.53 X187 = s(X190)). % 280.50/35.53 cnf(c192, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a188, a189, a190])], [c190, c191])). % 280.50/35.53 cnf(c193, plain, % 280.50/35.53 ~sum(X188,X189,X190), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a188, a189, a190])], [c190, c191])). % 280.50/35.53 % 280.50/35.53 cnf(c194, axiom, % 280.50/35.53 sum(X191,s(X192),s(X193)) | ~sum(X191,X192,X193)). % 280.50/35.53 cnf(a191, assumption, % 280.50/35.53 X188 = X191). % 280.50/35.53 cnf(a192, assumption, % 280.50/35.53 X189 = s(X192)). % 280.50/35.53 cnf(a193, assumption, % 280.50/35.53 X190 = s(X193)). % 280.50/35.53 cnf(c195, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a191, a192, a193])], [c193, c194])). % 280.50/35.53 cnf(c196, plain, % 280.50/35.53 ~sum(X191,X192,X193), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a191, a192, a193])], [c193, c194])). % 280.50/35.53 % 280.50/35.53 cnf(c197, axiom, % 280.50/35.53 sum(X194,s(X195),s(X196)) | ~sum(X194,X195,X196)). % 280.50/35.53 cnf(a194, assumption, % 280.50/35.53 X191 = X194). % 280.50/35.53 cnf(a195, assumption, % 280.50/35.53 X192 = s(X195)). % 280.50/35.53 cnf(a196, assumption, % 280.50/35.53 X193 = s(X196)). % 280.50/35.53 cnf(c198, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a194, a195, a196])], [c196, c197])). % 280.50/35.53 cnf(c199, plain, % 280.50/35.53 ~sum(X194,X195,X196), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a194, a195, a196])], [c196, c197])). % 280.50/35.53 % 280.50/35.53 cnf(c200, axiom, % 280.50/35.53 sum(X197,s(X198),s(X199)) | ~sum(X197,X198,X199)). % 280.50/35.53 cnf(a197, assumption, % 280.50/35.53 X194 = X197). % 280.50/35.53 cnf(a198, assumption, % 280.50/35.53 X195 = s(X198)). % 280.50/35.53 cnf(a199, assumption, % 280.50/35.53 X196 = s(X199)). % 280.50/35.53 cnf(c201, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a197, a198, a199])], [c199, c200])). % 280.50/35.53 cnf(c202, plain, % 280.50/35.53 ~sum(X197,X198,X199), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a197, a198, a199])], [c199, c200])). % 280.50/35.53 % 280.50/35.53 cnf(c203, axiom, % 280.50/35.53 sum(X200,s(X201),s(X202)) | ~sum(X200,X201,X202)). % 280.50/35.53 cnf(a200, assumption, % 280.50/35.53 X197 = X200). % 280.50/35.53 cnf(a201, assumption, % 280.50/35.53 X198 = s(X201)). % 280.50/35.53 cnf(a202, assumption, % 280.50/35.53 X199 = s(X202)). % 280.50/35.53 cnf(c204, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a200, a201, a202])], [c202, c203])). % 280.50/35.53 cnf(c205, plain, % 280.50/35.53 ~sum(X200,X201,X202), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a200, a201, a202])], [c202, c203])). % 280.50/35.53 % 280.50/35.53 cnf(c206, axiom, % 280.50/35.53 sum(X203,s(X204),s(X205)) | ~sum(X203,X204,X205)). % 280.50/35.53 cnf(a203, assumption, % 280.50/35.53 X200 = X203). % 280.50/35.53 cnf(a204, assumption, % 280.50/35.53 X201 = s(X204)). % 280.50/35.53 cnf(a205, assumption, % 280.50/35.53 X202 = s(X205)). % 280.50/35.53 cnf(c207, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a203, a204, a205])], [c205, c206])). % 280.50/35.53 cnf(c208, plain, % 280.50/35.53 ~sum(X203,X204,X205), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a203, a204, a205])], [c205, c206])). % 280.50/35.53 % 280.50/35.53 cnf(c209, axiom, % 280.50/35.53 sum(X206,s(X207),s(X208)) | ~sum(X206,X207,X208)). % 280.50/35.53 cnf(a206, assumption, % 280.50/35.53 X203 = X206). % 280.50/35.53 cnf(a207, assumption, % 280.50/35.53 X204 = s(X207)). % 280.50/35.53 cnf(a208, assumption, % 280.50/35.53 X205 = s(X208)). % 280.50/35.53 cnf(c210, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a206, a207, a208])], [c208, c209])). % 280.50/35.53 cnf(c211, plain, % 280.50/35.53 ~sum(X206,X207,X208), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a206, a207, a208])], [c208, c209])). % 280.50/35.53 % 280.50/35.53 cnf(c212, axiom, % 280.50/35.53 sum(X209,s(X210),s(X211)) | ~sum(X209,X210,X211)). % 280.50/35.53 cnf(a209, assumption, % 280.50/35.53 X206 = X209). % 280.50/35.53 cnf(a210, assumption, % 280.50/35.53 X207 = s(X210)). % 280.50/35.53 cnf(a211, assumption, % 280.50/35.53 X208 = s(X211)). % 280.50/35.53 cnf(c213, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a209, a210, a211])], [c211, c212])). % 280.50/35.53 cnf(c214, plain, % 280.50/35.53 ~sum(X209,X210,X211), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a209, a210, a211])], [c211, c212])). % 280.50/35.53 % 280.50/35.53 cnf(c215, axiom, % 280.50/35.53 sum(X212,s(X213),s(X214)) | ~sum(X212,X213,X214)). % 280.50/35.53 cnf(a212, assumption, % 280.50/35.53 X209 = X212). % 280.50/35.53 cnf(a213, assumption, % 280.50/35.53 X210 = s(X213)). % 280.50/35.53 cnf(a214, assumption, % 280.50/35.53 X211 = s(X214)). % 280.50/35.53 cnf(c216, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a212, a213, a214])], [c214, c215])). % 280.50/35.53 cnf(c217, plain, % 280.50/35.53 ~sum(X212,X213,X214), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a212, a213, a214])], [c214, c215])). % 280.50/35.53 % 280.50/35.53 cnf(c218, axiom, % 280.50/35.53 sum(X215,s(X216),s(X217)) | ~sum(X215,X216,X217)). % 280.50/35.53 cnf(a215, assumption, % 280.50/35.53 X212 = X215). % 280.50/35.53 cnf(a216, assumption, % 280.50/35.53 X213 = s(X216)). % 280.50/35.53 cnf(a217, assumption, % 280.50/35.53 X214 = s(X217)). % 280.50/35.53 cnf(c219, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a215, a216, a217])], [c217, c218])). % 280.50/35.53 cnf(c220, plain, % 280.50/35.53 ~sum(X215,X216,X217), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a215, a216, a217])], [c217, c218])). % 280.50/35.53 % 280.50/35.53 cnf(c221, axiom, % 280.50/35.53 sum(X218,s(X219),s(X220)) | ~sum(X218,X219,X220)). % 280.50/35.53 cnf(a218, assumption, % 280.50/35.53 X215 = X218). % 280.50/35.53 cnf(a219, assumption, % 280.50/35.53 X216 = s(X219)). % 280.50/35.53 cnf(a220, assumption, % 280.50/35.53 X217 = s(X220)). % 280.50/35.53 cnf(c222, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a218, a219, a220])], [c220, c221])). % 280.50/35.53 cnf(c223, plain, % 280.50/35.53 ~sum(X218,X219,X220), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a218, a219, a220])], [c220, c221])). % 280.50/35.53 % 280.50/35.53 cnf(c224, axiom, % 280.50/35.53 sum(X221,s(X222),s(X223)) | ~sum(X221,X222,X223)). % 280.50/35.53 cnf(a221, assumption, % 280.50/35.53 X218 = X221). % 280.50/35.53 cnf(a222, assumption, % 280.50/35.53 X219 = s(X222)). % 280.50/35.53 cnf(a223, assumption, % 280.50/35.53 X220 = s(X223)). % 280.50/35.53 cnf(c225, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a221, a222, a223])], [c223, c224])). % 280.50/35.53 cnf(c226, plain, % 280.50/35.53 ~sum(X221,X222,X223), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a221, a222, a223])], [c223, c224])). % 280.50/35.53 % 280.50/35.53 cnf(c227, axiom, % 280.50/35.53 sum(X224,s(X225),s(X226)) | ~sum(X224,X225,X226)). % 280.50/35.53 cnf(a224, assumption, % 280.50/35.53 X221 = X224). % 280.50/35.53 cnf(a225, assumption, % 280.50/35.53 X222 = s(X225)). % 280.50/35.53 cnf(a226, assumption, % 280.50/35.53 X223 = s(X226)). % 280.50/35.53 cnf(c228, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a224, a225, a226])], [c226, c227])). % 280.50/35.53 cnf(c229, plain, % 280.50/35.53 ~sum(X224,X225,X226), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a224, a225, a226])], [c226, c227])). % 280.50/35.53 % 280.50/35.53 cnf(c230, axiom, % 280.50/35.53 sum(X227,s(X228),s(X229)) | ~sum(X227,X228,X229)). % 280.50/35.53 cnf(a227, assumption, % 280.50/35.53 X224 = X227). % 280.50/35.53 cnf(a228, assumption, % 280.50/35.53 X225 = s(X228)). % 280.50/35.53 cnf(a229, assumption, % 280.50/35.53 X226 = s(X229)). % 280.50/35.53 cnf(c231, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a227, a228, a229])], [c229, c230])). % 280.50/35.53 cnf(c232, plain, % 280.50/35.53 ~sum(X227,X228,X229), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a227, a228, a229])], [c229, c230])). % 280.50/35.53 % 280.50/35.53 cnf(c233, axiom, % 280.50/35.53 sum(X230,s(X231),s(X232)) | ~sum(X230,X231,X232)). % 280.50/35.53 cnf(a230, assumption, % 280.50/35.53 X227 = X230). % 280.50/35.53 cnf(a231, assumption, % 280.50/35.53 X228 = s(X231)). % 280.50/35.53 cnf(a232, assumption, % 280.50/35.53 X229 = s(X232)). % 280.50/35.53 cnf(c234, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a230, a231, a232])], [c232, c233])). % 280.50/35.53 cnf(c235, plain, % 280.50/35.53 ~sum(X230,X231,X232), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a230, a231, a232])], [c232, c233])). % 280.50/35.53 % 280.50/35.53 cnf(c236, axiom, % 280.50/35.53 sum(X233,s(X234),s(X235)) | ~sum(X233,X234,X235)). % 280.50/35.53 cnf(a233, assumption, % 280.50/35.53 X230 = X233). % 280.50/35.53 cnf(a234, assumption, % 280.50/35.53 X231 = s(X234)). % 280.50/35.53 cnf(a235, assumption, % 280.50/35.53 X232 = s(X235)). % 280.50/35.53 cnf(c237, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a233, a234, a235])], [c235, c236])). % 280.50/35.53 cnf(c238, plain, % 280.50/35.53 ~sum(X233,X234,X235), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a233, a234, a235])], [c235, c236])). % 280.50/35.53 % 280.50/35.53 cnf(c239, axiom, % 280.50/35.53 sum(X236,s(X237),s(X238)) | ~sum(X236,X237,X238)). % 280.50/35.53 cnf(a236, assumption, % 280.50/35.53 X233 = X236). % 280.50/35.53 cnf(a237, assumption, % 280.50/35.53 X234 = s(X237)). % 280.50/35.53 cnf(a238, assumption, % 280.50/35.53 X235 = s(X238)). % 280.50/35.53 cnf(c240, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a236, a237, a238])], [c238, c239])). % 280.50/35.53 cnf(c241, plain, % 280.50/35.53 ~sum(X236,X237,X238), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a236, a237, a238])], [c238, c239])). % 280.50/35.53 % 280.50/35.53 cnf(c242, axiom, % 280.50/35.53 sum(X239,n0,X239)). % 280.50/35.53 cnf(a239, assumption, % 280.50/35.53 X236 = X239). % 280.50/35.53 cnf(a240, assumption, % 280.50/35.53 X237 = n0). % 280.50/35.53 cnf(a241, assumption, % 280.50/35.53 X238 = X239). % 280.50/35.53 cnf(c243, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a239, a240, a241])], [c241, c242])). % 280.50/35.53 cnf(c244, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a239, a240, a241])], [c241, c242])). % 280.50/35.53 % 280.50/35.53 cnf(c245, axiom, % 280.50/35.53 sum(X240,s(X241),s(X242)) | ~sum(X240,X241,X242)). % 280.50/35.53 cnf(a242, assumption, % 280.50/35.53 X7 = X240). % 280.50/35.53 cnf(a243, assumption, % 280.50/35.53 X5 = s(X241)). % 280.50/35.53 cnf(a244, assumption, % 280.50/35.53 X6 = s(X242)). % 280.50/35.53 cnf(c246, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a242, a243, a244])], [c9, c245])). % 280.50/35.53 cnf(c247, plain, % 280.50/35.53 ~sum(X240,X241,X242), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a242, a243, a244])], [c9, c245])). % 280.50/35.53 % 280.50/35.53 cnf(c248, axiom, % 280.50/35.53 sum(X243,s(X244),s(X245)) | ~sum(X243,X244,X245)). % 280.50/35.53 cnf(a245, assumption, % 280.50/35.53 X240 = X243). % 280.50/35.53 cnf(a246, assumption, % 280.50/35.53 X241 = s(X244)). % 280.50/35.53 cnf(a247, assumption, % 280.50/35.53 X242 = s(X245)). % 280.50/35.53 cnf(c249, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a245, a246, a247])], [c247, c248])). % 280.50/35.53 cnf(c250, plain, % 280.50/35.53 ~sum(X243,X244,X245), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a245, a246, a247])], [c247, c248])). % 280.50/35.53 % 280.50/35.53 cnf(c251, axiom, % 280.50/35.53 sum(X246,s(X247),s(X248)) | ~sum(X246,X247,X248)). % 280.50/35.53 cnf(a248, assumption, % 280.50/35.53 X243 = X246). % 280.50/35.53 cnf(a249, assumption, % 280.50/35.53 X244 = s(X247)). % 280.50/35.53 cnf(a250, assumption, % 280.50/35.53 X245 = s(X248)). % 280.50/35.53 cnf(c252, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a248, a249, a250])], [c250, c251])). % 280.50/35.53 cnf(c253, plain, % 280.50/35.53 ~sum(X246,X247,X248), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a248, a249, a250])], [c250, c251])). % 280.50/35.53 % 280.50/35.53 cnf(c254, axiom, % 280.50/35.53 sum(X249,s(X250),s(X251)) | ~sum(X249,X250,X251)). % 280.50/35.53 cnf(a251, assumption, % 280.50/35.53 X246 = X249). % 280.50/35.53 cnf(a252, assumption, % 280.50/35.53 X247 = s(X250)). % 280.50/35.53 cnf(a253, assumption, % 280.50/35.53 X248 = s(X251)). % 280.50/35.53 cnf(c255, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a251, a252, a253])], [c253, c254])). % 280.50/35.53 cnf(c256, plain, % 280.50/35.53 ~sum(X249,X250,X251), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a251, a252, a253])], [c253, c254])). % 280.50/35.53 % 280.50/35.53 cnf(c257, axiom, % 280.50/35.53 sum(X252,s(X253),s(X254)) | ~sum(X252,X253,X254)). % 280.50/35.53 cnf(a254, assumption, % 280.50/35.53 X249 = X252). % 280.50/35.53 cnf(a255, assumption, % 280.50/35.53 X250 = s(X253)). % 280.50/35.53 cnf(a256, assumption, % 280.50/35.53 X251 = s(X254)). % 280.50/35.53 cnf(c258, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a254, a255, a256])], [c256, c257])). % 280.50/35.53 cnf(c259, plain, % 280.50/35.53 ~sum(X252,X253,X254), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a254, a255, a256])], [c256, c257])). % 280.50/35.53 % 280.50/35.53 cnf(c260, axiom, % 280.50/35.53 sum(X255,s(X256),s(X257)) | ~sum(X255,X256,X257)). % 280.50/35.53 cnf(a257, assumption, % 280.50/35.53 X252 = X255). % 280.50/35.53 cnf(a258, assumption, % 280.50/35.53 X253 = s(X256)). % 280.50/35.53 cnf(a259, assumption, % 280.50/35.53 X254 = s(X257)). % 280.50/35.53 cnf(c261, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a257, a258, a259])], [c259, c260])). % 280.50/35.53 cnf(c262, plain, % 280.50/35.53 ~sum(X255,X256,X257), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a257, a258, a259])], [c259, c260])). % 280.50/35.53 % 280.50/35.53 cnf(c263, axiom, % 280.50/35.53 sum(X258,s(X259),s(X260)) | ~sum(X258,X259,X260)). % 280.50/35.53 cnf(a260, assumption, % 280.50/35.53 X255 = X258). % 280.50/35.53 cnf(a261, assumption, % 280.50/35.53 X256 = s(X259)). % 280.50/35.53 cnf(a262, assumption, % 280.50/35.53 X257 = s(X260)). % 280.50/35.53 cnf(c264, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a260, a261, a262])], [c262, c263])). % 280.50/35.53 cnf(c265, plain, % 280.50/35.53 ~sum(X258,X259,X260), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a260, a261, a262])], [c262, c263])). % 280.50/35.53 % 280.50/35.53 cnf(c266, axiom, % 280.50/35.53 sum(X261,s(X262),s(X263)) | ~sum(X261,X262,X263)). % 280.50/35.53 cnf(a263, assumption, % 280.50/35.53 X258 = X261). % 280.50/35.53 cnf(a264, assumption, % 280.50/35.53 X259 = s(X262)). % 280.50/35.53 cnf(a265, assumption, % 280.50/35.53 X260 = s(X263)). % 280.50/35.53 cnf(c267, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a263, a264, a265])], [c265, c266])). % 280.50/35.53 cnf(c268, plain, % 280.50/35.53 ~sum(X261,X262,X263), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a263, a264, a265])], [c265, c266])). % 280.50/35.53 % 280.50/35.53 cnf(c269, axiom, % 280.50/35.53 sum(X264,s(X265),s(X266)) | ~sum(X264,X265,X266)). % 280.50/35.53 cnf(a266, assumption, % 280.50/35.53 X261 = X264). % 280.50/35.53 cnf(a267, assumption, % 280.50/35.53 X262 = s(X265)). % 280.50/35.53 cnf(a268, assumption, % 280.50/35.53 X263 = s(X266)). % 280.50/35.53 cnf(c270, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a266, a267, a268])], [c268, c269])). % 280.50/35.53 cnf(c271, plain, % 280.50/35.53 ~sum(X264,X265,X266), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a266, a267, a268])], [c268, c269])). % 280.50/35.53 % 280.50/35.53 cnf(c272, axiom, % 280.50/35.53 sum(X267,s(X268),s(X269)) | ~sum(X267,X268,X269)). % 280.50/35.53 cnf(a269, assumption, % 280.50/35.53 X264 = X267). % 280.50/35.53 cnf(a270, assumption, % 280.50/35.53 X265 = s(X268)). % 280.50/35.53 cnf(a271, assumption, % 280.50/35.53 X266 = s(X269)). % 280.50/35.53 cnf(c273, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a269, a270, a271])], [c271, c272])). % 280.50/35.53 cnf(c274, plain, % 280.50/35.53 ~sum(X267,X268,X269), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a269, a270, a271])], [c271, c272])). % 280.50/35.53 % 280.50/35.53 cnf(c275, axiom, % 280.50/35.53 sum(X270,s(X271),s(X272)) | ~sum(X270,X271,X272)). % 280.50/35.53 cnf(a272, assumption, % 280.50/35.53 X267 = X270). % 280.50/35.53 cnf(a273, assumption, % 280.50/35.53 X268 = s(X271)). % 280.50/35.53 cnf(a274, assumption, % 280.50/35.53 X269 = s(X272)). % 280.50/35.53 cnf(c276, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a272, a273, a274])], [c274, c275])). % 280.50/35.53 cnf(c277, plain, % 280.50/35.53 ~sum(X270,X271,X272), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a272, a273, a274])], [c274, c275])). % 280.50/35.53 % 280.50/35.53 cnf(c278, axiom, % 280.50/35.53 sum(X273,s(X274),s(X275)) | ~sum(X273,X274,X275)). % 280.50/35.53 cnf(a275, assumption, % 280.50/35.53 X270 = X273). % 280.50/35.53 cnf(a276, assumption, % 280.50/35.53 X271 = s(X274)). % 280.50/35.53 cnf(a277, assumption, % 280.50/35.53 X272 = s(X275)). % 280.50/35.53 cnf(c279, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a275, a276, a277])], [c277, c278])). % 280.50/35.53 cnf(c280, plain, % 280.50/35.53 ~sum(X273,X274,X275), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a275, a276, a277])], [c277, c278])). % 280.50/35.53 % 280.50/35.53 cnf(c281, axiom, % 280.50/35.53 sum(X276,s(X277),s(X278)) | ~sum(X276,X277,X278)). % 280.50/35.53 cnf(a278, assumption, % 280.50/35.53 X273 = X276). % 280.50/35.53 cnf(a279, assumption, % 280.50/35.53 X274 = s(X277)). % 280.50/35.53 cnf(a280, assumption, % 280.50/35.53 X275 = s(X278)). % 280.50/35.53 cnf(c282, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a278, a279, a280])], [c280, c281])). % 280.50/35.53 cnf(c283, plain, % 280.50/35.53 ~sum(X276,X277,X278), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a278, a279, a280])], [c280, c281])). % 280.50/35.53 % 280.50/35.53 cnf(c284, axiom, % 280.50/35.53 sum(X279,s(X280),s(X281)) | ~sum(X279,X280,X281)). % 280.50/35.53 cnf(a281, assumption, % 280.50/35.53 X276 = X279). % 280.50/35.53 cnf(a282, assumption, % 280.50/35.53 X277 = s(X280)). % 280.50/35.53 cnf(a283, assumption, % 280.50/35.53 X278 = s(X281)). % 280.50/35.53 cnf(c285, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a281, a282, a283])], [c283, c284])). % 280.50/35.53 cnf(c286, plain, % 280.50/35.53 ~sum(X279,X280,X281), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a281, a282, a283])], [c283, c284])). % 280.50/35.53 % 280.50/35.53 cnf(c287, axiom, % 280.50/35.53 sum(X282,s(X283),s(X284)) | ~sum(X282,X283,X284)). % 280.50/35.53 cnf(a284, assumption, % 280.50/35.53 X279 = X282). % 280.50/35.53 cnf(a285, assumption, % 280.50/35.53 X280 = s(X283)). % 280.50/35.53 cnf(a286, assumption, % 280.50/35.53 X281 = s(X284)). % 280.50/35.53 cnf(c288, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a284, a285, a286])], [c286, c287])). % 280.50/35.53 cnf(c289, plain, % 280.50/35.53 ~sum(X282,X283,X284), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a284, a285, a286])], [c286, c287])). % 280.50/35.53 % 280.50/35.53 cnf(c290, axiom, % 280.50/35.53 sum(X285,s(X286),s(X287)) | ~sum(X285,X286,X287)). % 280.50/35.53 cnf(a287, assumption, % 280.50/35.53 X282 = X285). % 280.50/35.53 cnf(a288, assumption, % 280.50/35.53 X283 = s(X286)). % 280.50/35.53 cnf(a289, assumption, % 280.50/35.53 X284 = s(X287)). % 280.50/35.53 cnf(c291, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a287, a288, a289])], [c289, c290])). % 280.50/35.53 cnf(c292, plain, % 280.50/35.53 ~sum(X285,X286,X287), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a287, a288, a289])], [c289, c290])). % 280.50/35.53 % 280.50/35.53 cnf(c293, axiom, % 280.50/35.53 sum(X288,s(X289),s(X290)) | ~sum(X288,X289,X290)). % 280.50/35.53 cnf(a290, assumption, % 280.50/35.53 X285 = X288). % 280.50/35.53 cnf(a291, assumption, % 280.50/35.53 X286 = s(X289)). % 280.50/35.53 cnf(a292, assumption, % 280.50/35.53 X287 = s(X290)). % 280.50/35.53 cnf(c294, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a290, a291, a292])], [c292, c293])). % 280.50/35.53 cnf(c295, plain, % 280.50/35.53 ~sum(X288,X289,X290), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a290, a291, a292])], [c292, c293])). % 280.50/35.53 % 280.50/35.53 cnf(c296, axiom, % 280.50/35.53 sum(X291,s(X292),s(X293)) | ~sum(X291,X292,X293)). % 280.50/35.53 cnf(a293, assumption, % 280.50/35.53 X288 = X291). % 280.50/35.53 cnf(a294, assumption, % 280.50/35.53 X289 = s(X292)). % 280.50/35.53 cnf(a295, assumption, % 280.50/35.53 X290 = s(X293)). % 280.50/35.53 cnf(c297, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a293, a294, a295])], [c295, c296])). % 280.50/35.53 cnf(c298, plain, % 280.50/35.53 ~sum(X291,X292,X293), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a293, a294, a295])], [c295, c296])). % 280.50/35.53 % 280.50/35.53 cnf(c299, axiom, % 280.50/35.53 sum(X294,s(X295),s(X296)) | ~sum(X294,X295,X296)). % 280.50/35.53 cnf(a296, assumption, % 280.50/35.53 X291 = X294). % 280.50/35.53 cnf(a297, assumption, % 280.50/35.53 X292 = s(X295)). % 280.50/35.53 cnf(a298, assumption, % 280.50/35.53 X293 = s(X296)). % 280.50/35.53 cnf(c300, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a296, a297, a298])], [c298, c299])). % 280.50/35.53 cnf(c301, plain, % 280.50/35.53 ~sum(X294,X295,X296), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a296, a297, a298])], [c298, c299])). % 280.50/35.53 % 280.50/35.53 cnf(c302, axiom, % 280.50/35.53 sum(X297,s(X298),s(X299)) | ~sum(X297,X298,X299)). % 280.50/35.53 cnf(a299, assumption, % 280.50/35.53 X294 = X297). % 280.50/35.53 cnf(a300, assumption, % 280.50/35.53 X295 = s(X298)). % 280.50/35.53 cnf(a301, assumption, % 280.50/35.53 X296 = s(X299)). % 280.50/35.53 cnf(c303, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a299, a300, a301])], [c301, c302])). % 280.50/35.53 cnf(c304, plain, % 280.50/35.53 ~sum(X297,X298,X299), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a299, a300, a301])], [c301, c302])). % 280.50/35.53 % 280.50/35.53 cnf(c305, axiom, % 280.50/35.53 sum(X300,s(X301),s(X302)) | ~sum(X300,X301,X302)). % 280.50/35.53 cnf(a302, assumption, % 280.50/35.53 X297 = X300). % 280.50/35.53 cnf(a303, assumption, % 280.50/35.53 X298 = s(X301)). % 280.50/35.53 cnf(a304, assumption, % 280.50/35.53 X299 = s(X302)). % 280.50/35.53 cnf(c306, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a302, a303, a304])], [c304, c305])). % 280.50/35.53 cnf(c307, plain, % 280.50/35.53 ~sum(X300,X301,X302), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a302, a303, a304])], [c304, c305])). % 280.50/35.53 % 280.50/35.53 cnf(c308, axiom, % 280.50/35.53 sum(X303,s(X304),s(X305)) | ~sum(X303,X304,X305)). % 280.50/35.53 cnf(a305, assumption, % 280.50/35.53 X300 = X303). % 280.50/35.53 cnf(a306, assumption, % 280.50/35.53 X301 = s(X304)). % 280.50/35.53 cnf(a307, assumption, % 280.50/35.53 X302 = s(X305)). % 280.50/35.53 cnf(c309, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a305, a306, a307])], [c307, c308])). % 280.50/35.53 cnf(c310, plain, % 280.50/35.53 ~sum(X303,X304,X305), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a305, a306, a307])], [c307, c308])). % 280.50/35.53 % 280.50/35.53 cnf(c311, axiom, % 280.50/35.53 sum(X306,s(X307),s(X308)) | ~sum(X306,X307,X308)). % 280.50/35.53 cnf(a308, assumption, % 280.50/35.53 X303 = X306). % 280.50/35.53 cnf(a309, assumption, % 280.50/35.53 X304 = s(X307)). % 280.50/35.53 cnf(a310, assumption, % 280.50/35.53 X305 = s(X308)). % 280.50/35.53 cnf(c312, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a308, a309, a310])], [c310, c311])). % 280.50/35.53 cnf(c313, plain, % 280.50/35.53 ~sum(X306,X307,X308), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a308, a309, a310])], [c310, c311])). % 280.50/35.53 % 280.50/35.53 cnf(c314, axiom, % 280.50/35.53 sum(X309,s(X310),s(X311)) | ~sum(X309,X310,X311)). % 280.50/35.53 cnf(a311, assumption, % 280.50/35.53 X306 = X309). % 280.50/35.53 cnf(a312, assumption, % 280.50/35.53 X307 = s(X310)). % 280.50/35.53 cnf(a313, assumption, % 280.50/35.53 X308 = s(X311)). % 280.50/35.53 cnf(c315, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a311, a312, a313])], [c313, c314])). % 280.50/35.53 cnf(c316, plain, % 280.50/35.53 ~sum(X309,X310,X311), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a311, a312, a313])], [c313, c314])). % 280.50/35.53 % 280.50/35.53 cnf(c317, axiom, % 280.50/35.53 sum(X312,n0,X312)). % 280.50/35.53 cnf(a314, assumption, % 280.50/35.53 X309 = X312). % 280.50/35.53 cnf(a315, assumption, % 280.50/35.53 X310 = n0). % 280.50/35.53 cnf(a316, assumption, % 280.50/35.53 X311 = X312). % 280.50/35.53 cnf(c318, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a314, a315, a316])], [c316, c317])). % 280.50/35.53 cnf(c319, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a314, a315, a316])], [c316, c317])). % 280.50/35.53 % 280.50/35.53 cnf(c320, axiom, % 280.50/35.53 factorial(s(X313),X314) | ~product(s(X313),X315,X314) | ~factorial(X313,X315)). % 280.50/35.53 cnf(a317, assumption, % 280.50/35.53 X1 = s(X313)). % 280.50/35.53 cnf(a318, assumption, % 280.50/35.53 X3 = X314). % 280.50/35.53 cnf(c321, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a317, a318])], [c6, c320])). % 280.50/35.53 cnf(c322, plain, % 280.50/35.53 ~product(s(X313),X315,X314) | ~factorial(X313,X315), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a317, a318])], [c6, c320])). % 280.50/35.53 % 280.50/35.53 cnf(c323, axiom, % 280.50/35.53 product(s(X316),X317,X318) | ~product(X316,X317,X319) | ~sum(X319,X317,X318)). % 280.50/35.53 cnf(a319, assumption, % 280.50/35.53 s(X313) = s(X316)). % 280.50/35.53 cnf(a320, assumption, % 280.50/35.53 X315 = X317). % 280.50/35.53 cnf(a321, assumption, % 280.50/35.53 X314 = X318). % 280.50/35.53 cnf(c324, plain, % 280.50/35.53 ~factorial(X313,X315), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a319, a320, a321])], [c322, c323])). % 280.50/35.53 cnf(c325, plain, % 280.50/35.53 ~product(X316,X317,X319) | ~sum(X319,X317,X318), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a319, a320, a321])], [c322, c323])). % 280.50/35.53 % 280.50/35.53 cnf(c326, axiom, % 280.50/35.53 product(s(X320),X321,X322) | ~product(X320,X321,X323) | ~sum(X323,X321,X322)). % 280.50/35.53 cnf(a322, assumption, % 280.50/35.53 X316 = s(X320)). % 280.50/35.53 cnf(a323, assumption, % 280.50/35.53 X317 = X321). % 280.50/35.53 cnf(a324, assumption, % 280.50/35.53 X319 = X322). % 280.50/35.53 cnf(c327, plain, % 280.50/35.53 ~sum(X319,X317,X318), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a322, a323, a324])], [c325, c326])). % 280.50/35.53 cnf(c328, plain, % 280.50/35.53 ~product(X320,X321,X323) | ~sum(X323,X321,X322), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a322, a323, a324])], [c325, c326])). % 280.50/35.53 % 280.50/35.53 cnf(c329, axiom, % 280.50/35.53 product(s(X324),X325,X326) | ~product(X324,X325,X327) | ~sum(X327,X325,X326)). % 280.50/35.53 cnf(a325, assumption, % 280.50/35.53 X320 = s(X324)). % 280.50/35.53 cnf(a326, assumption, % 280.50/35.53 X321 = X325). % 280.50/35.53 cnf(a327, assumption, % 280.50/35.53 X323 = X326). % 280.50/35.53 cnf(c330, plain, % 280.50/35.53 ~sum(X323,X321,X322), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a325, a326, a327])], [c328, c329])). % 280.50/35.53 cnf(c331, plain, % 280.50/35.53 ~product(X324,X325,X327) | ~sum(X327,X325,X326), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a325, a326, a327])], [c328, c329])). % 280.50/35.53 % 280.50/35.53 cnf(c332, axiom, % 280.50/35.53 product(s(n0),X328,X328)). % 280.50/35.53 cnf(a328, assumption, % 280.50/35.53 X324 = s(n0)). % 280.50/35.53 cnf(a329, assumption, % 280.50/35.53 X325 = X328). % 280.50/35.53 cnf(a330, assumption, % 280.50/35.53 X327 = X328). % 280.50/35.53 cnf(c333, plain, % 280.50/35.53 ~sum(X327,X325,X326), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a328, a329, a330])], [c331, c332])). % 280.50/35.53 cnf(c334, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a328, a329, a330])], [c331, c332])). % 280.50/35.53 % 280.50/35.53 cnf(c335, axiom, % 280.50/35.53 sum(X329,s(X330),s(X331)) | ~sum(X329,X330,X331)). % 280.50/35.53 cnf(a331, assumption, % 280.50/35.53 X327 = X329). % 280.50/35.53 cnf(a332, assumption, % 280.50/35.53 X325 = s(X330)). % 280.50/35.53 cnf(a333, assumption, % 280.50/35.53 X326 = s(X331)). % 280.50/35.53 cnf(c336, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a331, a332, a333])], [c333, c335])). % 280.50/35.53 cnf(c337, plain, % 280.50/35.53 ~sum(X329,X330,X331), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a331, a332, a333])], [c333, c335])). % 280.50/35.53 % 280.50/35.53 cnf(c338, axiom, % 280.50/35.53 sum(X332,s(X333),s(X334)) | ~sum(X332,X333,X334)). % 280.50/35.53 cnf(a334, assumption, % 280.50/35.53 X329 = X332). % 280.50/35.53 cnf(a335, assumption, % 280.50/35.53 X330 = s(X333)). % 280.50/35.53 cnf(a336, assumption, % 280.50/35.53 X331 = s(X334)). % 280.50/35.53 cnf(c339, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a334, a335, a336])], [c337, c338])). % 280.50/35.53 cnf(c340, plain, % 280.50/35.53 ~sum(X332,X333,X334), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a334, a335, a336])], [c337, c338])). % 280.50/35.53 % 280.50/35.53 cnf(c341, axiom, % 280.50/35.53 sum(X335,s(X336),s(X337)) | ~sum(X335,X336,X337)). % 280.50/35.53 cnf(a337, assumption, % 280.50/35.53 X332 = X335). % 280.50/35.53 cnf(a338, assumption, % 280.50/35.53 X333 = s(X336)). % 280.50/35.53 cnf(a339, assumption, % 280.50/35.53 X334 = s(X337)). % 280.50/35.53 cnf(c342, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a337, a338, a339])], [c340, c341])). % 280.50/35.53 cnf(c343, plain, % 280.50/35.53 ~sum(X335,X336,X337), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a337, a338, a339])], [c340, c341])). % 280.50/35.53 % 280.50/35.53 cnf(c344, axiom, % 280.50/35.53 sum(X338,s(X339),s(X340)) | ~sum(X338,X339,X340)). % 280.50/35.53 cnf(a340, assumption, % 280.50/35.53 X335 = X338). % 280.50/35.53 cnf(a341, assumption, % 280.50/35.53 X336 = s(X339)). % 280.50/35.53 cnf(a342, assumption, % 280.50/35.53 X337 = s(X340)). % 280.50/35.53 cnf(c345, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a340, a341, a342])], [c343, c344])). % 280.50/35.53 cnf(c346, plain, % 280.50/35.53 ~sum(X338,X339,X340), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a340, a341, a342])], [c343, c344])). % 280.50/35.53 % 280.50/35.53 cnf(c347, axiom, % 280.50/35.53 sum(X341,s(X342),s(X343)) | ~sum(X341,X342,X343)). % 280.50/35.53 cnf(a343, assumption, % 280.50/35.53 X338 = X341). % 280.50/35.53 cnf(a344, assumption, % 280.50/35.53 X339 = s(X342)). % 280.50/35.53 cnf(a345, assumption, % 280.50/35.53 X340 = s(X343)). % 280.50/35.53 cnf(c348, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a343, a344, a345])], [c346, c347])). % 280.50/35.53 cnf(c349, plain, % 280.50/35.53 ~sum(X341,X342,X343), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a343, a344, a345])], [c346, c347])). % 280.50/35.53 % 280.50/35.53 cnf(c350, axiom, % 280.50/35.53 sum(X344,s(X345),s(X346)) | ~sum(X344,X345,X346)). % 280.50/35.53 cnf(a346, assumption, % 280.50/35.53 X341 = X344). % 280.50/35.53 cnf(a347, assumption, % 280.50/35.53 X342 = s(X345)). % 280.50/35.53 cnf(a348, assumption, % 280.50/35.53 X343 = s(X346)). % 280.50/35.53 cnf(c351, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a346, a347, a348])], [c349, c350])). % 280.50/35.53 cnf(c352, plain, % 280.50/35.53 ~sum(X344,X345,X346), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a346, a347, a348])], [c349, c350])). % 280.50/35.53 % 280.50/35.53 cnf(c353, axiom, % 280.50/35.53 sum(X347,n0,X347)). % 280.50/35.53 cnf(a349, assumption, % 280.50/35.53 X344 = X347). % 280.50/35.53 cnf(a350, assumption, % 280.50/35.53 X345 = n0). % 280.50/35.53 cnf(a351, assumption, % 280.50/35.53 X346 = X347). % 280.50/35.53 cnf(c354, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a349, a350, a351])], [c352, c353])). % 280.50/35.53 cnf(c355, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a349, a350, a351])], [c352, c353])). % 280.50/35.53 % 280.50/35.53 cnf(c356, axiom, % 280.50/35.53 sum(X348,s(X349),s(X350)) | ~sum(X348,X349,X350)). % 280.50/35.53 cnf(a352, assumption, % 280.50/35.53 X323 = X348). % 280.50/35.53 cnf(a353, assumption, % 280.50/35.53 X321 = s(X349)). % 280.50/35.53 cnf(a354, assumption, % 280.50/35.53 X322 = s(X350)). % 280.50/35.53 cnf(c357, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a352, a353, a354])], [c330, c356])). % 280.50/35.53 cnf(c358, plain, % 280.50/35.53 ~sum(X348,X349,X350), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a352, a353, a354])], [c330, c356])). % 280.50/35.53 % 280.50/35.53 cnf(c359, axiom, % 280.50/35.53 sum(X351,s(X352),s(X353)) | ~sum(X351,X352,X353)). % 280.50/35.53 cnf(a355, assumption, % 280.50/35.53 X348 = X351). % 280.50/35.53 cnf(a356, assumption, % 280.50/35.53 X349 = s(X352)). % 280.50/35.53 cnf(a357, assumption, % 280.50/35.53 X350 = s(X353)). % 280.50/35.53 cnf(c360, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a355, a356, a357])], [c358, c359])). % 280.50/35.53 cnf(c361, plain, % 280.50/35.53 ~sum(X351,X352,X353), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a355, a356, a357])], [c358, c359])). % 280.50/35.53 % 280.50/35.53 cnf(c362, axiom, % 280.50/35.53 sum(X354,s(X355),s(X356)) | ~sum(X354,X355,X356)). % 280.50/35.53 cnf(a358, assumption, % 280.50/35.53 X351 = X354). % 280.50/35.53 cnf(a359, assumption, % 280.50/35.53 X352 = s(X355)). % 280.50/35.53 cnf(a360, assumption, % 280.50/35.53 X353 = s(X356)). % 280.50/35.53 cnf(c363, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a358, a359, a360])], [c361, c362])). % 280.50/35.53 cnf(c364, plain, % 280.50/35.53 ~sum(X354,X355,X356), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a358, a359, a360])], [c361, c362])). % 280.50/35.53 % 280.50/35.53 cnf(c365, axiom, % 280.50/35.53 sum(X357,s(X358),s(X359)) | ~sum(X357,X358,X359)). % 280.50/35.53 cnf(a361, assumption, % 280.50/35.53 X354 = X357). % 280.50/35.53 cnf(a362, assumption, % 280.50/35.53 X355 = s(X358)). % 280.50/35.53 cnf(a363, assumption, % 280.50/35.53 X356 = s(X359)). % 280.50/35.53 cnf(c366, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a361, a362, a363])], [c364, c365])). % 280.50/35.53 cnf(c367, plain, % 280.50/35.53 ~sum(X357,X358,X359), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a361, a362, a363])], [c364, c365])). % 280.50/35.53 % 280.50/35.53 cnf(c368, axiom, % 280.50/35.53 sum(X360,s(X361),s(X362)) | ~sum(X360,X361,X362)). % 280.50/35.53 cnf(a364, assumption, % 280.50/35.53 X357 = X360). % 280.50/35.53 cnf(a365, assumption, % 280.50/35.53 X358 = s(X361)). % 280.50/35.53 cnf(a366, assumption, % 280.50/35.53 X359 = s(X362)). % 280.50/35.53 cnf(c369, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a364, a365, a366])], [c367, c368])). % 280.50/35.53 cnf(c370, plain, % 280.50/35.53 ~sum(X360,X361,X362), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a364, a365, a366])], [c367, c368])). % 280.50/35.53 % 280.50/35.53 cnf(c371, axiom, % 280.50/35.53 sum(X363,s(X364),s(X365)) | ~sum(X363,X364,X365)). % 280.50/35.53 cnf(a367, assumption, % 280.50/35.53 X360 = X363). % 280.50/35.53 cnf(a368, assumption, % 280.50/35.53 X361 = s(X364)). % 280.50/35.53 cnf(a369, assumption, % 280.50/35.53 X362 = s(X365)). % 280.50/35.53 cnf(c372, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a367, a368, a369])], [c370, c371])). % 280.50/35.53 cnf(c373, plain, % 280.50/35.53 ~sum(X363,X364,X365), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a367, a368, a369])], [c370, c371])). % 280.50/35.53 % 280.50/35.53 cnf(c374, axiom, % 280.50/35.53 sum(X366,n0,X366)). % 280.50/35.53 cnf(a370, assumption, % 280.50/35.53 X363 = X366). % 280.50/35.53 cnf(a371, assumption, % 280.50/35.53 X364 = n0). % 280.50/35.53 cnf(a372, assumption, % 280.50/35.53 X365 = X366). % 280.50/35.53 cnf(c375, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a370, a371, a372])], [c373, c374])). % 280.50/35.53 cnf(c376, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a370, a371, a372])], [c373, c374])). % 280.50/35.53 % 280.50/35.53 cnf(c377, axiom, % 280.50/35.53 sum(X367,s(X368),s(X369)) | ~sum(X367,X368,X369)). % 280.50/35.53 cnf(a373, assumption, % 280.50/35.53 X319 = X367). % 280.50/35.53 cnf(a374, assumption, % 280.50/35.53 X317 = s(X368)). % 280.50/35.53 cnf(a375, assumption, % 280.50/35.53 X318 = s(X369)). % 280.50/35.53 cnf(c378, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a373, a374, a375])], [c327, c377])). % 280.50/35.53 cnf(c379, plain, % 280.50/35.53 ~sum(X367,X368,X369), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a373, a374, a375])], [c327, c377])). % 280.50/35.53 % 280.50/35.53 cnf(c380, axiom, % 280.50/35.53 sum(X370,s(X371),s(X372)) | ~sum(X370,X371,X372)). % 280.50/35.53 cnf(a376, assumption, % 280.50/35.53 X367 = X370). % 280.50/35.53 cnf(a377, assumption, % 280.50/35.53 X368 = s(X371)). % 280.50/35.53 cnf(a378, assumption, % 280.50/35.53 X369 = s(X372)). % 280.50/35.53 cnf(c381, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a376, a377, a378])], [c379, c380])). % 280.50/35.53 cnf(c382, plain, % 280.50/35.53 ~sum(X370,X371,X372), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a376, a377, a378])], [c379, c380])). % 280.50/35.53 % 280.50/35.53 cnf(c383, axiom, % 280.50/35.53 sum(X373,s(X374),s(X375)) | ~sum(X373,X374,X375)). % 280.50/35.53 cnf(a379, assumption, % 280.50/35.53 X370 = X373). % 280.50/35.53 cnf(a380, assumption, % 280.50/35.53 X371 = s(X374)). % 280.50/35.53 cnf(a381, assumption, % 280.50/35.53 X372 = s(X375)). % 280.50/35.53 cnf(c384, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a379, a380, a381])], [c382, c383])). % 280.50/35.53 cnf(c385, plain, % 280.50/35.53 ~sum(X373,X374,X375), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a379, a380, a381])], [c382, c383])). % 280.50/35.53 % 280.50/35.53 cnf(c386, axiom, % 280.50/35.53 sum(X376,s(X377),s(X378)) | ~sum(X376,X377,X378)). % 280.50/35.53 cnf(a382, assumption, % 280.50/35.53 X373 = X376). % 280.50/35.53 cnf(a383, assumption, % 280.50/35.53 X374 = s(X377)). % 280.50/35.53 cnf(a384, assumption, % 280.50/35.53 X375 = s(X378)). % 280.50/35.53 cnf(c387, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a382, a383, a384])], [c385, c386])). % 280.50/35.53 cnf(c388, plain, % 280.50/35.53 ~sum(X376,X377,X378), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a382, a383, a384])], [c385, c386])). % 280.50/35.53 % 280.50/35.53 cnf(c389, axiom, % 280.50/35.53 sum(X379,s(X380),s(X381)) | ~sum(X379,X380,X381)). % 280.50/35.53 cnf(a385, assumption, % 280.50/35.53 X376 = X379). % 280.50/35.53 cnf(a386, assumption, % 280.50/35.53 X377 = s(X380)). % 280.50/35.53 cnf(a387, assumption, % 280.50/35.53 X378 = s(X381)). % 280.50/35.53 cnf(c390, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a385, a386, a387])], [c388, c389])). % 280.50/35.53 cnf(c391, plain, % 280.50/35.53 ~sum(X379,X380,X381), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a385, a386, a387])], [c388, c389])). % 280.50/35.53 % 280.50/35.53 cnf(c392, axiom, % 280.50/35.53 sum(X382,s(X383),s(X384)) | ~sum(X382,X383,X384)). % 280.50/35.53 cnf(a388, assumption, % 280.50/35.53 X379 = X382). % 280.50/35.53 cnf(a389, assumption, % 280.50/35.53 X380 = s(X383)). % 280.50/35.53 cnf(a390, assumption, % 280.50/35.53 X381 = s(X384)). % 280.50/35.53 cnf(c393, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a388, a389, a390])], [c391, c392])). % 280.50/35.53 cnf(c394, plain, % 280.50/35.53 ~sum(X382,X383,X384), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a388, a389, a390])], [c391, c392])). % 280.50/35.53 % 280.50/35.53 cnf(c395, axiom, % 280.50/35.53 sum(X385,n0,X385)). % 280.50/35.53 cnf(a391, assumption, % 280.50/35.53 X382 = X385). % 280.50/35.53 cnf(a392, assumption, % 280.50/35.53 X383 = n0). % 280.50/35.53 cnf(a393, assumption, % 280.50/35.53 X384 = X385). % 280.50/35.53 cnf(c396, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a391, a392, a393])], [c394, c395])). % 280.50/35.53 cnf(c397, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a391, a392, a393])], [c394, c395])). % 280.50/35.53 % 280.50/35.53 cnf(c398, axiom, % 280.50/35.53 factorial(s(X386),X387) | ~product(s(X386),X388,X387) | ~factorial(X386,X388)). % 280.50/35.53 cnf(a394, assumption, % 280.50/35.53 X313 = s(X386)). % 280.50/35.53 cnf(a395, assumption, % 280.50/35.53 X315 = X387). % 280.50/35.53 cnf(c399, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a394, a395])], [c324, c398])). % 280.50/35.53 cnf(c400, plain, % 280.50/35.53 ~product(s(X386),X388,X387) | ~factorial(X386,X388), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a394, a395])], [c324, c398])). % 280.50/35.53 % 280.50/35.53 cnf(c401, axiom, % 280.50/35.53 product(s(X389),X390,X391) | ~product(X389,X390,X392) | ~sum(X392,X390,X391)). % 280.50/35.53 cnf(a396, assumption, % 280.50/35.53 s(X386) = s(X389)). % 280.50/35.53 cnf(a397, assumption, % 280.50/35.53 X388 = X390). % 280.50/35.53 cnf(a398, assumption, % 280.50/35.53 X387 = X391). % 280.50/35.53 cnf(c402, plain, % 280.50/35.53 ~factorial(X386,X388), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a396, a397, a398])], [c400, c401])). % 280.50/35.53 cnf(c403, plain, % 280.50/35.53 ~product(X389,X390,X392) | ~sum(X392,X390,X391), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a396, a397, a398])], [c400, c401])). % 280.50/35.53 % 280.50/35.53 cnf(c404, axiom, % 280.50/35.53 product(s(X393),X394,X395) | ~product(X393,X394,X396) | ~sum(X396,X394,X395)). % 280.50/35.53 cnf(a399, assumption, % 280.50/35.53 X389 = s(X393)). % 280.50/35.53 cnf(a400, assumption, % 280.50/35.53 X390 = X394). % 280.50/35.53 cnf(a401, assumption, % 280.50/35.53 X392 = X395). % 280.50/35.53 cnf(c405, plain, % 280.50/35.53 ~sum(X392,X390,X391), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a399, a400, a401])], [c403, c404])). % 280.50/35.53 cnf(c406, plain, % 280.50/35.53 ~product(X393,X394,X396) | ~sum(X396,X394,X395), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a399, a400, a401])], [c403, c404])). % 280.50/35.53 % 280.50/35.53 cnf(c407, axiom, % 280.50/35.53 product(s(n0),X397,X397)). % 280.50/35.53 cnf(a402, assumption, % 280.50/35.53 X393 = s(n0)). % 280.50/35.53 cnf(a403, assumption, % 280.50/35.53 X394 = X397). % 280.50/35.53 cnf(a404, assumption, % 280.50/35.53 X396 = X397). % 280.50/35.53 cnf(c408, plain, % 280.50/35.53 ~sum(X396,X394,X395), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a402, a403, a404])], [c406, c407])). % 280.50/35.53 cnf(c409, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a402, a403, a404])], [c406, c407])). % 280.50/35.53 % 280.50/35.53 cnf(c410, axiom, % 280.50/35.53 sum(X398,s(X399),s(X400)) | ~sum(X398,X399,X400)). % 280.50/35.53 cnf(a405, assumption, % 280.50/35.53 X396 = X398). % 280.50/35.53 cnf(a406, assumption, % 280.50/35.53 X394 = s(X399)). % 280.50/35.53 cnf(a407, assumption, % 280.50/35.53 X395 = s(X400)). % 280.50/35.53 cnf(c411, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a405, a406, a407])], [c408, c410])). % 280.50/35.53 cnf(c412, plain, % 280.50/35.53 ~sum(X398,X399,X400), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a405, a406, a407])], [c408, c410])). % 280.50/35.53 % 280.50/35.53 cnf(c413, axiom, % 280.50/35.53 sum(X401,s(X402),s(X403)) | ~sum(X401,X402,X403)). % 280.50/35.53 cnf(a408, assumption, % 280.50/35.53 X398 = X401). % 280.50/35.53 cnf(a409, assumption, % 280.50/35.53 X399 = s(X402)). % 280.50/35.53 cnf(a410, assumption, % 280.50/35.53 X400 = s(X403)). % 280.50/35.53 cnf(c414, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a408, a409, a410])], [c412, c413])). % 280.50/35.53 cnf(c415, plain, % 280.50/35.53 ~sum(X401,X402,X403), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a408, a409, a410])], [c412, c413])). % 280.50/35.53 % 280.50/35.53 cnf(c416, axiom, % 280.50/35.53 sum(X404,n0,X404)). % 280.50/35.53 cnf(a411, assumption, % 280.50/35.53 X401 = X404). % 280.50/35.53 cnf(a412, assumption, % 280.50/35.53 X402 = n0). % 280.50/35.53 cnf(a413, assumption, % 280.50/35.53 X403 = X404). % 280.50/35.53 cnf(c417, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a411, a412, a413])], [c415, c416])). % 280.50/35.53 cnf(c418, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a411, a412, a413])], [c415, c416])). % 280.50/35.53 % 280.50/35.53 cnf(c419, axiom, % 280.50/35.53 sum(X405,s(X406),s(X407)) | ~sum(X405,X406,X407)). % 280.50/35.53 cnf(a414, assumption, % 280.50/35.53 X392 = X405). % 280.50/35.53 cnf(a415, assumption, % 280.50/35.53 X390 = s(X406)). % 280.50/35.53 cnf(a416, assumption, % 280.50/35.53 X391 = s(X407)). % 280.50/35.53 cnf(c420, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a414, a415, a416])], [c405, c419])). % 280.50/35.53 cnf(c421, plain, % 280.50/35.53 ~sum(X405,X406,X407), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a414, a415, a416])], [c405, c419])). % 280.50/35.53 % 280.50/35.53 cnf(c422, axiom, % 280.50/35.53 sum(X408,s(X409),s(X410)) | ~sum(X408,X409,X410)). % 280.50/35.53 cnf(a417, assumption, % 280.50/35.53 X405 = X408). % 280.50/35.53 cnf(a418, assumption, % 280.50/35.53 X406 = s(X409)). % 280.50/35.53 cnf(a419, assumption, % 280.50/35.53 X407 = s(X410)). % 280.50/35.53 cnf(c423, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a417, a418, a419])], [c421, c422])). % 280.50/35.53 cnf(c424, plain, % 280.50/35.53 ~sum(X408,X409,X410), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a417, a418, a419])], [c421, c422])). % 280.50/35.53 % 280.50/35.53 cnf(c425, axiom, % 280.50/35.53 sum(X411,n0,X411)). % 280.50/35.53 cnf(a420, assumption, % 280.50/35.53 X408 = X411). % 280.50/35.53 cnf(a421, assumption, % 280.50/35.53 X409 = n0). % 280.50/35.53 cnf(a422, assumption, % 280.50/35.53 X410 = X411). % 280.50/35.53 cnf(c426, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a420, a421, a422])], [c424, c425])). % 280.50/35.53 cnf(c427, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a420, a421, a422])], [c424, c425])). % 280.50/35.53 % 280.50/35.53 cnf(c428, axiom, % 280.50/35.53 factorial(s(X412),X413) | ~product(s(X412),X414,X413) | ~factorial(X412,X414)). % 280.50/35.53 cnf(a423, assumption, % 280.50/35.53 X386 = s(X412)). % 280.50/35.53 cnf(a424, assumption, % 280.50/35.53 X388 = X413). % 280.50/35.53 cnf(c429, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a423, a424])], [c402, c428])). % 280.50/35.53 cnf(c430, plain, % 280.50/35.53 ~product(s(X412),X414,X413) | ~factorial(X412,X414), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a423, a424])], [c402, c428])). % 280.50/35.53 % 280.50/35.53 cnf(c431, axiom, % 280.50/35.53 product(s(X415),X416,X417) | ~product(X415,X416,X418) | ~sum(X418,X416,X417)). % 280.50/35.53 cnf(a425, assumption, % 280.50/35.53 s(X412) = s(X415)). % 280.50/35.53 cnf(a426, assumption, % 280.50/35.53 X414 = X416). % 280.50/35.53 cnf(a427, assumption, % 280.50/35.53 X413 = X417). % 280.50/35.53 cnf(c432, plain, % 280.50/35.53 ~factorial(X412,X414), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a425, a426, a427])], [c430, c431])). % 280.50/35.53 cnf(c433, plain, % 280.50/35.53 ~product(X415,X416,X418) | ~sum(X418,X416,X417), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a425, a426, a427])], [c430, c431])). % 280.50/35.53 % 280.50/35.53 cnf(c434, axiom, % 280.50/35.53 product(s(n0),X419,X419)). % 280.50/35.53 cnf(a428, assumption, % 280.50/35.53 X415 = s(n0)). % 280.50/35.53 cnf(a429, assumption, % 280.50/35.53 X416 = X419). % 280.50/35.53 cnf(a430, assumption, % 280.50/35.53 X418 = X419). % 280.50/35.53 cnf(c435, plain, % 280.50/35.53 ~sum(X418,X416,X417), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a428, a429, a430])], [c433, c434])). % 280.50/35.53 cnf(c436, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a428, a429, a430])], [c433, c434])). % 280.50/35.53 % 280.50/35.53 cnf(c437, axiom, % 280.50/35.53 sum(X420,s(X421),s(X422)) | ~sum(X420,X421,X422)). % 280.50/35.53 cnf(a431, assumption, % 280.50/35.53 X418 = X420). % 280.50/35.53 cnf(a432, assumption, % 280.50/35.53 X416 = s(X421)). % 280.50/35.53 cnf(a433, assumption, % 280.50/35.53 X417 = s(X422)). % 280.50/35.53 cnf(c438, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a431, a432, a433])], [c435, c437])). % 280.50/35.53 cnf(c439, plain, % 280.50/35.53 ~sum(X420,X421,X422), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a431, a432, a433])], [c435, c437])). % 280.50/35.53 % 280.50/35.53 cnf(c440, axiom, % 280.50/35.53 sum(X423,n0,X423)). % 280.50/35.53 cnf(a434, assumption, % 280.50/35.53 X420 = X423). % 280.50/35.53 cnf(a435, assumption, % 280.50/35.53 X421 = n0). % 280.50/35.53 cnf(a436, assumption, % 280.50/35.53 X422 = X423). % 280.50/35.53 cnf(c441, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a434, a435, a436])], [c439, c440])). % 280.50/35.53 cnf(c442, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a434, a435, a436])], [c439, c440])). % 280.50/35.53 % 280.50/35.53 cnf(c443, axiom, % 280.50/35.53 factorial(s(X424),X425) | ~product(s(X424),X426,X425) | ~factorial(X424,X426)). % 280.50/35.53 cnf(a437, assumption, % 280.50/35.53 X412 = s(X424)). % 280.50/35.53 cnf(a438, assumption, % 280.50/35.53 X414 = X425). % 280.50/35.53 cnf(c444, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a437, a438])], [c432, c443])). % 280.50/35.53 cnf(c445, plain, % 280.50/35.53 ~product(s(X424),X426,X425) | ~factorial(X424,X426), % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a437, a438])], [c432, c443])). % 280.50/35.53 % 280.50/35.53 cnf(c446, plain, % 280.50/35.53 product(X415,X416,X418)). % 280.50/35.53 cnf(a439, assumption, % 280.50/35.53 s(X424) = X415). % 280.50/35.53 cnf(a440, assumption, % 280.50/35.53 X426 = X416). % 280.50/35.53 cnf(a441, assumption, % 280.50/35.53 X425 = X418). % 280.50/35.53 cnf(c447, plain, % 280.50/35.53 ~factorial(X424,X426), % 280.50/35.53 inference(predicate_reduction, [assumptions([a439, a440, a441])], [c445, c446])). % 280.50/35.53 % 280.50/35.53 cnf(c448, axiom, % 280.50/35.53 factorial(n0,s(n0))). % 280.50/35.53 cnf(a442, assumption, % 280.50/35.53 X424 = n0). % 280.50/35.53 cnf(a443, assumption, % 280.50/35.53 X426 = s(n0)). % 280.50/35.53 cnf(c449, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a442, a443])], [c447, c448])). % 280.50/35.53 cnf(c450, plain, % 280.50/35.53 $false, % 280.50/35.53 inference(strict_predicate_extension, [assumptions([a442, a443])], [c447, c448])). % 280.50/35.53 % 280.50/35.54 cnf(c451, plain, % 280.50/35.54 $false, % 280.50/35.54 inference(constraint_solving, [ % 280.50/35.54 bind(X0, s(X242)), % 280.50/35.54 bind(X1, s(s(s(s(n0))))), % 280.50/35.54 bind(X2, s(X242)), % 280.50/35.54 bind(X3, s(X22)), % 280.50/35.54 bind(X4, s(s(s(s(n0))))), % 280.50/35.54 bind(X5, s(X22)), % 280.50/35.54 bind(X6, s(X242)), % 280.50/35.54 bind(X7, s(X169)), % 280.50/35.54 bind(X8, s(s(s(n0)))), % 280.50/35.54 bind(X9, s(X22)), % 280.50/35.54 bind(X10, s(X169)), % 280.50/35.54 bind(X11, s(X96)), % 280.50/35.54 bind(X12, s(s(n0))), % 280.50/35.54 bind(X13, s(X22)), % 280.50/35.54 bind(X14, s(X96)), % 280.50/35.54 bind(X15, s(X23)), % 280.50/35.54 bind(X16, s(n0)), % 280.50/35.54 bind(X17, s(X22)), % 280.50/35.54 bind(X18, s(X23)), % 280.50/35.54 bind(X19, s(X22)), % 280.50/35.54 bind(X20, s(X22)), % 280.50/35.54 bind(X21, s(X22)), % 280.50/35.54 bind(X22, s(X25)), % 280.50/35.54 bind(X23, s(X26)), % 280.50/35.54 bind(X24, s(X22)), % 280.50/35.54 bind(X25, s(X28)), % 280.50/35.54 bind(X26, s(X29)), % 280.50/35.54 bind(X27, s(X22)), % 280.50/35.54 bind(X28, s(X31)), % 280.50/35.54 bind(X29, s(X32)), % 280.50/35.54 bind(X30, s(X22)), % 280.50/35.54 bind(X31, s(X34)), % 280.50/35.54 bind(X32, s(X35)), % 280.50/35.54 bind(X33, s(X22)), % 280.50/35.54 bind(X34, s(X37)), % 280.50/35.54 bind(X35, s(X38)), % 280.50/35.54 bind(X36, s(X22)), % 280.50/35.54 bind(X37, s(X40)), % 280.50/35.54 bind(X38, s(X41)), % 280.50/35.54 bind(X39, s(X22)), % 280.50/35.54 bind(X40, s(X43)), % 280.50/35.54 bind(X41, s(X44)), % 280.50/35.54 bind(X42, s(X22)), % 280.50/35.54 bind(X43, s(X46)), % 280.50/35.54 bind(X44, s(X47)), % 280.50/35.54 bind(X45, s(X22)), % 280.50/35.54 bind(X46, s(X49)), % 280.50/35.54 bind(X47, s(X50)), % 280.50/35.54 bind(X48, s(X22)), % 280.50/35.54 bind(X49, s(X52)), % 280.50/35.54 bind(X50, s(X53)), % 280.50/35.54 bind(X51, s(X22)), % 280.50/35.54 bind(X52, s(X55)), % 280.50/35.54 bind(X53, s(X56)), % 280.50/35.54 bind(X54, s(X22)), % 280.50/35.54 bind(X55, s(X58)), % 280.50/35.54 bind(X56, s(X59)), % 280.50/35.54 bind(X57, s(X22)), % 280.50/35.54 bind(X58, s(X61)), % 280.50/35.54 bind(X59, s(X62)), % 280.50/35.54 bind(X60, s(X22)), % 280.50/35.54 bind(X61, s(X64)), % 280.50/35.54 bind(X62, s(X65)), % 280.50/35.54 bind(X63, s(X22)), % 280.50/35.54 bind(X64, s(X67)), % 280.50/35.54 bind(X65, s(X68)), % 280.50/35.54 bind(X66, s(X22)), % 280.50/35.54 bind(X67, s(X70)), % 280.50/35.54 bind(X68, s(X71)), % 280.50/35.54 bind(X69, s(X22)), % 280.50/35.54 bind(X70, s(X73)), % 280.50/35.54 bind(X71, s(X74)), % 280.50/35.54 bind(X72, s(X22)), % 280.50/35.54 bind(X73, s(X76)), % 280.50/35.54 bind(X74, s(X77)), % 280.50/35.54 bind(X75, s(X22)), % 280.50/35.54 bind(X76, s(X79)), % 280.50/35.54 bind(X77, s(X80)), % 280.50/35.54 bind(X78, s(X22)), % 280.50/35.54 bind(X79, s(X82)), % 280.50/35.54 bind(X80, s(X83)), % 280.50/35.54 bind(X81, s(X22)), % 280.50/35.54 bind(X82, s(X85)), % 280.50/35.54 bind(X83, s(X86)), % 280.50/35.54 bind(X84, s(X22)), % 280.50/35.54 bind(X85, s(X88)), % 280.50/35.54 bind(X86, s(X89)), % 280.50/35.54 bind(X87, s(X22)), % 280.50/35.54 bind(X88, s(X91)), % 280.50/35.54 bind(X89, s(X92)), % 280.50/35.54 bind(X90, s(X22)), % 280.50/35.54 bind(X91, n0), % 280.50/35.54 bind(X92, s(X22)), % 280.50/35.54 bind(X93, s(X22)), % 280.50/35.54 bind(X94, s(X23)), % 280.50/35.54 bind(X95, s(X25)), % 280.50/35.54 bind(X96, s(X99)), % 280.50/35.54 bind(X97, s(X23)), % 280.50/35.54 bind(X98, s(X28)), % 280.50/35.54 bind(X99, s(X102)), % 280.50/35.54 bind(X100, s(X23)), % 280.50/35.54 bind(X101, s(X31)), % 280.50/35.54 bind(X102, s(X105)), % 280.50/35.54 bind(X103, s(X23)), % 280.50/35.54 bind(X104, s(X34)), % 280.50/35.54 bind(X105, s(X108)), % 280.50/35.54 bind(X106, s(X23)), % 280.50/35.54 bind(X107, s(X37)), % 280.50/35.54 bind(X108, s(X111)), % 280.50/35.54 bind(X109, s(X23)), % 280.50/35.54 bind(X110, s(X40)), % 280.50/35.54 bind(X111, s(X114)), % 280.50/35.54 bind(X112, s(X23)), % 280.50/35.54 bind(X113, s(X43)), % 280.50/35.54 bind(X114, s(X117)), % 280.50/35.54 bind(X115, s(X23)), % 280.50/35.54 bind(X116, s(X46)), % 280.50/35.54 bind(X117, s(X120)), % 280.50/35.54 bind(X118, s(X23)), % 280.50/35.54 bind(X119, s(X49)), % 280.50/35.54 bind(X120, s(X123)), % 280.50/35.54 bind(X121, s(X23)), % 280.50/35.54 bind(X122, s(X52)), % 280.50/35.54 bind(X123, s(X126)), % 280.50/35.54 bind(X124, s(X23)), % 280.50/35.54 bind(X125, s(X55)), % 280.50/35.54 bind(X126, s(X129)), % 280.50/35.54 bind(X127, s(X23)), % 280.50/35.54 bind(X128, s(X58)), % 280.50/35.54 bind(X129, s(X132)), % 280.50/35.54 bind(X130, s(X23)), % 280.50/35.54 bind(X131, s(X61)), % 280.50/35.54 bind(X132, s(X135)), % 280.50/35.54 bind(X133, s(X23)), % 280.50/35.54 bind(X134, s(X64)), % 280.50/35.54 bind(X135, s(X138)), % 280.50/35.54 bind(X136, s(X23)), % 280.50/35.54 bind(X137, s(X67)), % 280.50/35.54 bind(X138, s(X141)), % 280.50/35.54 bind(X139, s(X23)), % 280.50/35.54 bind(X140, s(X70)), % 280.50/35.54 bind(X141, s(X144)), % 280.50/35.54 bind(X142, s(X23)), % 280.50/35.54 bind(X143, s(X73)), % 280.50/35.54 bind(X144, s(X147)), % 280.50/35.54 bind(X145, s(X23)), % 280.50/35.54 bind(X146, s(X76)), % 280.50/35.54 bind(X147, s(X150)), % 280.50/35.54 bind(X148, s(X23)), % 280.50/35.54 bind(X149, s(X79)), % 280.50/35.54 bind(X150, s(X153)), % 280.50/35.54 bind(X151, s(X23)), % 280.50/35.54 bind(X152, s(X82)), % 280.50/35.54 bind(X153, s(X156)), % 280.50/35.54 bind(X154, s(X23)), % 280.50/35.54 bind(X155, s(X85)), % 280.50/35.54 bind(X156, s(X159)), % 280.50/35.54 bind(X157, s(X23)), % 280.50/35.54 bind(X158, s(X88)), % 280.50/35.54 bind(X159, s(X162)), % 280.50/35.54 bind(X160, s(X23)), % 280.50/35.54 bind(X161, s(X91)), % 280.50/35.54 bind(X162, s(X165)), % 280.50/35.54 bind(X163, s(X23)), % 280.50/35.54 bind(X164, n0), % 280.50/35.54 bind(X165, s(X23)), % 280.50/35.54 bind(X166, s(X23)), % 280.50/35.54 bind(X167, s(X96)), % 280.50/35.54 bind(X168, s(X25)), % 280.50/35.54 bind(X169, s(X172)), % 280.50/35.54 bind(X170, s(X96)), % 280.50/35.54 bind(X171, s(X28)), % 280.50/35.54 bind(X172, s(X175)), % 280.50/35.54 bind(X173, s(X96)), % 280.50/35.54 bind(X174, s(X31)), % 280.50/35.54 bind(X175, s(X178)), % 280.50/35.54 bind(X176, s(X96)), % 280.50/35.54 bind(X177, s(X34)), % 280.50/35.54 bind(X178, s(X181)), % 280.50/35.54 bind(X179, s(X96)), % 280.50/35.54 bind(X180, s(X37)), % 280.50/35.54 bind(X181, s(X184)), % 280.50/35.54 bind(X182, s(X96)), % 280.50/35.54 bind(X183, s(X40)), % 280.50/35.54 bind(X184, s(X187)), % 280.50/35.54 bind(X185, s(X96)), % 280.50/35.54 bind(X186, s(X43)), % 280.50/35.54 bind(X187, s(X190)), % 280.50/35.54 bind(X188, s(X96)), % 280.50/35.54 bind(X189, s(X46)), % 280.50/35.54 bind(X190, s(X193)), % 280.50/35.54 bind(X191, s(X96)), % 280.50/35.54 bind(X192, s(X49)), % 280.50/35.54 bind(X193, s(X196)), % 280.50/35.54 bind(X194, s(X96)), % 280.50/35.54 bind(X195, s(X52)), % 280.50/35.54 bind(X196, s(X199)), % 280.50/35.54 bind(X197, s(X96)), % 280.50/35.54 bind(X198, s(X55)), % 280.50/35.54 bind(X199, s(X202)), % 280.50/35.54 bind(X200, s(X96)), % 280.50/35.54 bind(X201, s(X58)), % 280.50/35.54 bind(X202, s(X205)), % 280.50/35.54 bind(X203, s(X96)), % 280.50/35.54 bind(X204, s(X61)), % 280.50/35.54 bind(X205, s(X208)), % 280.50/35.54 bind(X206, s(X96)), % 280.50/35.54 bind(X207, s(X64)), % 280.50/35.54 bind(X208, s(X211)), % 280.50/35.54 bind(X209, s(X96)), % 280.50/35.54 bind(X210, s(X67)), % 280.50/35.54 bind(X211, s(X214)), % 280.50/35.54 bind(X212, s(X96)), % 280.50/35.54 bind(X213, s(X70)), % 280.50/35.54 bind(X214, s(X217)), % 280.50/35.54 bind(X215, s(X96)), % 280.50/35.54 bind(X216, s(X73)), % 280.50/35.54 bind(X217, s(X220)), % 280.50/35.54 bind(X218, s(X96)), % 280.50/35.54 bind(X219, s(X76)), % 280.50/35.54 bind(X220, s(X223)), % 280.50/35.54 bind(X221, s(X96)), % 280.50/35.54 bind(X222, s(X79)), % 280.50/35.54 bind(X223, s(X226)), % 280.50/35.54 bind(X224, s(X96)), % 280.50/35.54 bind(X225, s(X82)), % 280.50/35.54 bind(X226, s(X229)), % 280.50/35.54 bind(X227, s(X96)), % 280.50/35.54 bind(X228, s(X85)), % 280.50/35.54 bind(X229, s(X232)), % 280.50/35.54 bind(X230, s(X96)), % 280.50/35.54 bind(X231, s(X88)), % 280.50/35.54 bind(X232, s(X235)), % 280.50/35.54 bind(X233, s(X96)), % 280.50/35.54 bind(X234, s(X91)), % 280.50/35.54 bind(X235, s(X238)), % 280.50/35.54 bind(X236, s(X96)), % 280.50/35.54 bind(X237, n0), % 280.50/35.54 bind(X238, s(X96)), % 280.50/35.54 bind(X239, s(X96)), % 280.50/35.54 bind(X240, s(X169)), % 280.50/35.54 bind(X241, s(X25)), % 280.50/35.54 bind(X242, s(X245)), % 280.50/35.54 bind(X243, s(X169)), % 280.50/35.54 bind(X244, s(X28)), % 280.50/35.54 bind(X245, s(X248)), % 280.50/35.54 bind(X246, s(X169)), % 280.50/35.54 bind(X247, s(X31)), % 280.50/35.54 bind(X248, s(X251)), % 280.50/35.54 bind(X249, s(X169)), % 280.50/35.54 bind(X250, s(X34)), % 280.50/35.54 bind(X251, s(X254)), % 280.50/35.54 bind(X252, s(X169)), % 280.50/35.54 bind(X253, s(X37)), % 280.50/35.54 bind(X254, s(X257)), % 280.50/35.54 bind(X255, s(X169)), % 280.50/35.54 bind(X256, s(X40)), % 280.50/35.54 bind(X257, s(X260)), % 280.50/35.54 bind(X258, s(X169)), % 280.50/35.54 bind(X259, s(X43)), % 280.50/35.54 bind(X260, s(X263)), % 280.50/35.54 bind(X261, s(X169)), % 280.50/35.54 bind(X262, s(X46)), % 280.50/35.54 bind(X263, s(X266)), % 280.50/35.54 bind(X264, s(X169)), % 280.50/35.54 bind(X265, s(X49)), % 280.50/35.54 bind(X266, s(X269)), % 280.50/35.54 bind(X267, s(X169)), % 280.50/35.54 bind(X268, s(X52)), % 280.50/35.54 bind(X269, s(X272)), % 280.50/35.54 bind(X270, s(X169)), % 280.50/35.54 bind(X271, s(X55)), % 280.50/35.54 bind(X272, s(X275)), % 280.50/35.54 bind(X273, s(X169)), % 280.50/35.54 bind(X274, s(X58)), % 280.50/35.54 bind(X275, s(X278)), % 280.50/35.54 bind(X276, s(X169)), % 280.50/35.54 bind(X277, s(X61)), % 280.50/35.54 bind(X278, s(X281)), % 280.50/35.54 bind(X279, s(X169)), % 280.50/35.54 bind(X280, s(X64)), % 280.50/35.54 bind(X281, s(X284)), % 280.50/35.54 bind(X282, s(X169)), % 280.50/35.54 bind(X283, s(X67)), % 280.50/35.54 bind(X284, s(X287)), % 280.50/35.54 bind(X285, s(X169)), % 280.50/35.54 bind(X286, s(X70)), % 280.50/35.54 bind(X287, s(X290)), % 280.50/35.54 bind(X288, s(X169)), % 280.50/35.54 bind(X289, s(X73)), % 280.50/35.54 bind(X290, s(X293)), % 280.50/35.54 bind(X291, s(X169)), % 280.50/35.54 bind(X292, s(X76)), % 280.50/35.54 bind(X293, s(X296)), % 280.50/35.54 bind(X294, s(X169)), % 280.50/35.54 bind(X295, s(X79)), % 280.50/35.54 bind(X296, s(X299)), % 280.50/35.54 bind(X297, s(X169)), % 280.50/35.54 bind(X298, s(X82)), % 280.50/35.54 bind(X299, s(X302)), % 280.50/35.54 bind(X300, s(X169)), % 280.50/35.54 bind(X301, s(X85)), % 280.50/35.54 bind(X302, s(X305)), % 280.50/35.54 bind(X303, s(X169)), % 280.50/35.54 bind(X304, s(X88)), % 280.50/35.54 bind(X305, s(X308)), % 280.50/35.54 bind(X306, s(X169)), % 280.50/35.54 bind(X307, s(X91)), % 280.50/35.54 bind(X308, s(X311)), % 280.50/35.54 bind(X309, s(X169)), % 280.50/35.54 bind(X310, n0), % 280.50/35.54 bind(X311, s(X169)), % 280.50/35.54 bind(X312, s(X169)), % 280.50/35.54 bind(X313, s(s(s(n0)))), % 280.50/35.54 bind(X314, s(X22)), % 280.50/35.54 bind(X315, s(X330)), % 280.50/35.54 bind(X316, s(s(s(n0)))), % 280.50/35.54 bind(X317, s(X330)), % 280.50/35.54 bind(X318, s(X22)), % 280.50/35.54 bind(X319, s(X350)), % 280.50/35.54 bind(X320, s(s(n0))), % 280.50/35.54 bind(X321, s(X330)), % 280.50/35.54 bind(X322, s(X350)), % 280.50/35.54 bind(X323, s(X331)), % 280.50/35.54 bind(X324, s(n0)), % 280.50/35.54 bind(X325, s(X330)), % 280.50/35.54 bind(X326, s(X331)), % 280.50/35.54 bind(X327, s(X330)), % 280.50/35.54 bind(X328, s(X330)), % 280.50/35.54 bind(X329, s(X330)), % 280.50/35.54 bind(X330, s(X333)), % 280.50/35.54 bind(X331, s(X334)), % 280.50/35.54 bind(X332, s(X330)), % 280.50/35.54 bind(X333, s(X336)), % 280.50/35.54 bind(X334, s(X337)), % 280.50/35.54 bind(X335, s(X330)), % 280.50/35.54 bind(X336, s(X339)), % 280.50/35.54 bind(X337, s(X340)), % 280.50/35.54 bind(X338, s(X330)), % 280.50/35.54 bind(X339, s(X342)), % 280.50/35.54 bind(X340, s(X343)), % 280.50/35.54 bind(X341, s(X330)), % 280.50/35.54 bind(X342, s(X345)), % 280.50/35.54 bind(X343, s(X346)), % 280.50/35.54 bind(X344, s(X330)), % 280.50/35.54 bind(X345, n0), % 280.50/35.54 bind(X346, s(X330)), % 280.50/35.54 bind(X347, s(X330)), % 280.50/35.54 bind(X348, s(X331)), % 280.50/35.54 bind(X349, s(X333)), % 280.50/35.54 bind(X350, s(X353)), % 280.50/35.54 bind(X351, s(X331)), % 280.50/35.54 bind(X352, s(X336)), % 280.50/35.54 bind(X353, s(X356)), % 280.50/35.54 bind(X354, s(X331)), % 280.50/35.54 bind(X355, s(X339)), % 280.50/35.54 bind(X356, s(X359)), % 280.50/35.54 bind(X357, s(X331)), % 280.50/35.54 bind(X358, s(X342)), % 280.50/35.54 bind(X359, s(X362)), % 280.50/35.54 bind(X360, s(X331)), % 280.50/35.54 bind(X361, s(X345)), % 280.50/35.54 bind(X362, s(X365)), % 280.50/35.54 bind(X363, s(X331)), % 280.50/35.54 bind(X364, n0), % 280.50/35.54 bind(X365, s(X331)), % 280.50/35.54 bind(X366, s(X331)), % 280.50/35.54 bind(X367, s(X350)), % 280.50/35.54 bind(X368, s(X333)), % 280.50/35.54 bind(X369, s(X25)), % 280.50/35.54 bind(X370, s(X350)), % 280.50/35.54 bind(X371, s(X336)), % 280.50/35.54 bind(X372, s(X28)), % 280.50/35.54 bind(X373, s(X350)), % 280.50/35.54 bind(X374, s(X339)), % 280.50/35.54 bind(X375, s(X31)), % 280.50/35.54 bind(X376, s(X350)), % 280.50/35.54 bind(X377, s(X342)), % 280.50/35.54 bind(X378, s(X34)), % 280.50/35.54 bind(X379, s(X350)), % 280.50/35.54 bind(X380, s(X345)), % 280.50/35.54 bind(X381, s(X37)), % 280.50/35.54 bind(X382, s(X350)), % 280.50/35.54 bind(X383, n0), % 280.50/35.54 bind(X384, s(X40)), % 280.50/35.54 bind(X385, s(X350)), % 280.50/35.54 bind(X386, s(s(n0))), % 280.50/35.54 bind(X387, s(X330)), % 280.50/35.54 bind(X388, s(X399)), % 280.50/35.54 bind(X389, s(s(n0))), % 280.50/35.54 bind(X390, s(X399)), % 280.50/35.54 bind(X391, s(X330)), % 280.50/35.54 bind(X392, s(X400)), % 280.50/35.54 bind(X393, s(n0)), % 280.50/35.54 bind(X394, s(X399)), % 280.50/35.54 bind(X395, s(X400)), % 280.50/35.54 bind(X396, s(X399)), % 280.50/35.54 bind(X397, s(X399)), % 280.50/35.54 bind(X398, s(X399)), % 280.50/35.54 bind(X399, s(X402)), % 280.50/35.54 bind(X400, s(X403)), % 280.50/35.54 bind(X401, s(X399)), % 280.50/35.54 bind(X402, n0), % 280.50/35.54 bind(X403, s(X399)), % 280.50/35.54 bind(X404, s(X399)), % 280.50/35.54 bind(X405, s(X400)), % 280.50/35.54 bind(X406, s(X402)), % 280.50/35.54 bind(X407, s(X333)), % 280.50/35.54 bind(X408, s(X400)), % 280.50/35.54 bind(X409, n0), % 280.50/35.54 bind(X410, s(X336)), % 280.50/35.54 bind(X411, s(X400)), % 280.50/35.54 bind(X412, s(n0)), % 280.50/35.54 bind(X413, s(X399)), % 280.50/35.54 bind(X414, s(X421)), % 280.50/35.54 bind(X415, s(n0)), % 280.50/35.54 bind(X416, s(X421)), % 280.50/35.54 bind(X417, s(X399)), % 280.50/35.54 bind(X418, s(X421)), % 280.50/35.54 bind(X419, s(X421)), % 280.50/35.54 bind(X420, s(X421)), % 280.50/35.54 bind(X421, n0), % 280.50/35.54 bind(X422, s(X402)), % 280.50/35.54 bind(X423, s(X421)), % 280.50/35.54 bind(X424, n0), % 280.50/35.54 bind(X425, s(X421)), % 280.50/35.54 bind(X426, s(X421)) % 280.50/35.54 ], % 280.50/35.54 [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, a324, a325, a326, a327, a328, a329, a330, a331, a332, a333, a334, a335, a336, a337, a338, a339, a340, a341, a342, a343, a344, a345, a346, a347, a348, a349, a350, a351, a352, a353, a354, a355, a356, a357, a358, a359, a360, a361, a362, a363, a364, a365, a366, a367, a368, a369, a370, a371, a372, a373, a374, a375, a376, a377, a378, a379, a380, a381, a382, a383, a384, a385, a386, a387, a388, a389, a390, a391, a392, a393, a394, a395, a396, a397, a398, a399, a400, a401, a402, a403, a404, a405, a406, a407, a408, a409, a410, a411, a412, a413, a414, a415, a416, a417, a418, a419, a420, a421, a422, a423, a424, a425, a426, a427, a428, a429, a430, a431, a432, a433, a434, a435, a436, a437, a438, a439, a440, a441, a442, a443])). % 280.50/35.54 % 280.50/35.54 % SZS output end IncompleteProof %------------------------------------------------------------------------------