%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYN711-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:39:57 PM UTC 2026
% Result : Unsatisfiable 0.55s 1.62s
% Output : CNFRefutation 0.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 89
% Syntax : Number of clauses : 247 ( 105 unt; 0 nHn; 217 RR)
% Number of literals : 510 ( 0 equ; 274 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 85 ( 9 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 43 ( 43 usr; 19 con; 0-4 aty)
% Number of variables : 422 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p42_89,negated_conjecture,
p42(f16(f7(c46)),f32(f10(f11(f12(c49))),f10(f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_89) ).
cnf(p5_88,negated_conjecture,
p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(f12(f12(f12(f15(f12(f15(f15(f15(f12(f15(f15(f12(f15(f12(f12(f15(f15(f15(f15(f15(f12(f15(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f15(f15(f15(f15(f12(f15(f12(f12(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_88) ).
cnf(p5_87,negated_conjecture,
p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f12(f12(f15(f12(f12(f12(f15(f12(f15(f15(f15(f15(f12(f12(f12(f12(f12(f12(f12(f15(f12(f15(f15(f15(f15(f15(f12(f12(f12(f15(f12(f15(f12(f15(f15(f12(f15(f12(f15(f15(f12(f12(f15(f12(f12(f12(f15(f15(f15(f12(f15(f12(f15(f12(f15(f12(f15(f15(f15(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c50),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_87) ).
cnf(p43_84,negated_conjecture,
p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c47)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p43_84) ).
cnf(p43_83,negated_conjecture,
p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c46)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p43_83) ).
cnf(p6_86,negated_conjecture,
p6(f35(f7(c46),f13(f35(f10(f11(f15(f12(c49)))),f35(f36(f10(f11(f12(c49))),c62),f35(f36(f10(f11(f12(c49))),c62),f38(f10(f11(f15(f12(c49)))))))))),c63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_86) ).
cnf(not_p42_78,negated_conjecture,
~ p42(f16(c62),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p42_78) ).
cnf(p41_80,negated_conjecture,
p41(f16(f7(c46)),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p41_80) ).
cnf(p42_77,negated_conjecture,
p42(f16(c60),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_77) ).
cnf(p42_76,negated_conjecture,
p42(f16(c61),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_76) ).
cnf(p42_75,negated_conjecture,
p42(f16(c59),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_75) ).
cnf(p6_85,negated_conjecture,
p6(f7(c58),f35(f7(c47),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f35(f36(f10(f11(f12(c49))),c60),f36(f10(f11(f12(c49))),c61)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_85) ).
cnf(p5_60,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56)),c57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_60) ).
cnf(p5_59,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54)),c55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_59) ).
cnf(p5_58,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54)),c58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_58) ).
cnf(p5_57,negated_conjecture,
p5(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),c56),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_57) ).
cnf(p22_81,negated_conjecture,
( p22(f25(X1,X2,X3,X4),f25(X5,X6,X7,X8))
| ~ p5(X3,X7)
| ~ p5(X4,X8)
| ~ p24(X1,X5)
| ~ p5(X2,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_81) ).
cnf(p22_82,negated_conjecture,
( p22(f31(X1,X2,X3,X4),f31(X5,X6,X7,X8))
| ~ p5(X3,X7)
| ~ p5(X4,X8)
| ~ p24(X1,X5)
| ~ p5(X2,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_82) ).
cnf(p6_79,negated_conjecture,
p6(f7(c57),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f36(f10(f11(f12(c49))),c60)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_79) ).
cnf(p6_74,negated_conjecture,
p6(f7(c55),f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_74) ).
cnf(p6_56,negated_conjecture,
p6(f7(c56),f37(f35(f7(c50),f7(c46)),f7(c55))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_56) ).
cnf(p19_73,negated_conjecture,
( p19(f21(X1,X2),f21(X3,X4))
| ~ p9(X1,X3)
| ~ p9(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_73) ).
cnf(p24_72,negated_conjecture,
( p24(f27(X1,X2),f27(X3,X4))
| ~ p2(X1,X3)
| ~ p26(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_72) ).
cnf(p6_71,negated_conjecture,
( p6(f14(X1,X2),f14(X3,X4))
| ~ p6(X1,X3)
| ~ p9(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_71) ).
cnf(p6_70,negated_conjecture,
( p6(f32(X1,X2),f32(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_70) ).
cnf(p6_68,negated_conjecture,
( p6(f36(X1,X2),f36(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_68) ).
cnf(p6_67,negated_conjecture,
( p6(f37(X1,X2),f37(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_67) ).
cnf(p6_69,negated_conjecture,
( p6(f35(X1,X2),f35(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_69) ).
cnf(p17_66,negated_conjecture,
( p17(f20(X1,X2),f20(X3,X4))
| ~ p19(X2,X4)
| ~ p9(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17_66) ).
cnf(p41_29,negated_conjecture,
p41(f8(f10(f11(f12(c49)))),f7(c46)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p41_29) ).
cnf(p43_63,negated_conjecture,
( p43(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p43(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p43_63) ).
cnf(p41_65,negated_conjecture,
( p41(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p41(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p41_65) ).
cnf(p42_64,negated_conjecture,
( p42(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p42(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_64) ).
cnf(p40_61,negated_conjecture,
( p40(X1,X2)
| ~ p40(X3,X4)
| ~ p6(X3,X1)
| ~ p3(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p40_61) ).
cnf(p44_62,negated_conjecture,
( p44(X1,X2)
| ~ p44(X3,X4)
| ~ p5(X3,X1)
| ~ p33(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p44_62) ).
cnf(p42_47,negated_conjecture,
( p42(X1,X2)
| ~ p42(X1,X3)
| ~ p42(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_47) ).
cnf(p19_55,negated_conjecture,
( p19(X1,X2)
| ~ p19(X3,X1)
| ~ p19(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_55) ).
cnf(p2_54,negated_conjecture,
( p2(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_54) ).
cnf(p22_53,negated_conjecture,
( p22(X1,X2)
| ~ p22(X3,X1)
| ~ p22(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_53) ).
cnf(p24_52,negated_conjecture,
( p24(X1,X2)
| ~ p24(X3,X1)
| ~ p24(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_52) ).
cnf(p26_51,negated_conjecture,
( p26(X1,X2)
| ~ p26(X3,X1)
| ~ p26(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p26_51) ).
cnf(p28_50,negated_conjecture,
( p28(X1,X2)
| ~ p28(X3,X1)
| ~ p28(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p28_50) ).
cnf(p3_49,negated_conjecture,
( p3(X1,X2)
| ~ p3(X3,X1)
| ~ p3(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_49) ).
cnf(p33_48,negated_conjecture,
( p33(X1,X2)
| ~ p33(X3,X1)
| ~ p33(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p33_48) ).
cnf(p5_46,negated_conjecture,
( p5(X1,X2)
| ~ p5(X3,X1)
| ~ p5(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_46) ).
cnf(p6_45,negated_conjecture,
( p6(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_45) ).
cnf(p9_44,negated_conjecture,
( p9(X1,X2)
| ~ p9(X3,X1)
| ~ p9(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_44) ).
cnf(p17_43,negated_conjecture,
( p17(X1,X2)
| ~ p17(X3,X1)
| ~ p17(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17_43) ).
cnf(p3_31,negated_conjecture,
( p3(f4(X1),f4(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_31) ).
cnf(p33_32,negated_conjecture,
( p33(f34(X1),f34(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p33_32) ).
cnf(p5_34,negated_conjecture,
( p5(f23(X1),f23(X2))
| ~ p22(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_34) ).
cnf(p5_33,negated_conjecture,
( p5(f18(X1),f18(X2))
| ~ p17(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_33) ).
cnf(p6_38,negated_conjecture,
( p6(f38(X1),f38(X2))
| ~ p6(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_38) ).
cnf(p6_36,negated_conjecture,
( p6(f13(X1),f13(X2))
| ~ p6(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_36) ).
cnf(p6_40,negated_conjecture,
( p6(f8(X1),f8(X2))
| ~ p6(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_40) ).
cnf(p6_35,negated_conjecture,
( p6(f10(X1),f10(X2))
| ~ p9(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_35) ).
cnf(p6_37,negated_conjecture,
( p6(f16(X1),f16(X2))
| ~ p6(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_37) ).
cnf(p6_39,negated_conjecture,
( p6(f7(X1),f7(X2))
| ~ p5(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_39) ).
cnf(p9_30,negated_conjecture,
( p9(f15(X1),f15(X2))
| ~ p9(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_30) ).
cnf(p9_41,negated_conjecture,
( p9(f11(X1),f11(X2))
| ~ p9(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_41) ).
cnf(p9_42,negated_conjecture,
( p9(f12(X1),f12(X2))
| ~ p9(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_42) ).
cnf(p42_26,negated_conjecture,
( p42(X1,X2)
| ~ p41(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_26) ).
cnf(p45_28,negated_conjecture,
( p45(X1)
| ~ p45(X2)
| ~ p5(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p45_28) ).
cnf(p39_27,negated_conjecture,
( p39(X1)
| ~ p39(X2)
| ~ p5(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p39_27) ).
cnf(p42_25,negated_conjecture,
p42(f16(c62),f16(f7(c46))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p42_25) ).
cnf(p40_24,negated_conjecture,
p40(f7(c47),f4(c48)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p40_24) ).
cnf(p40_23,negated_conjecture,
p40(f7(c46),f4(c48)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p40_23) ).
cnf(p44_22,negated_conjecture,
p44(c57,f34(c52)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p44_22) ).
cnf(p44_20,negated_conjecture,
p44(c55,f34(c52)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p44_20) ).
cnf(p44_19,negated_conjecture,
p44(c58,f34(c52)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p44_19) ).
cnf(p44_21,negated_conjecture,
p44(c56,f34(c52)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p44_21) ).
cnf(p19_18,negated_conjecture,
p19(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_18) ).
cnf(p2_17,negated_conjecture,
p2(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_17) ).
cnf(p22_16,negated_conjecture,
p22(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_16) ).
cnf(p24_15,negated_conjecture,
p24(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_15) ).
cnf(p26_14,negated_conjecture,
p26(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p26_14) ).
cnf(p28_13,negated_conjecture,
p28(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p28_13) ).
cnf(p3_12,negated_conjecture,
p3(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_12) ).
cnf(p33_11,negated_conjecture,
p33(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p33_11) ).
cnf(p5_10,negated_conjecture,
p5(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5_10) ).
cnf(p6_9,negated_conjecture,
p6(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6_9) ).
cnf(p9_8,negated_conjecture,
p9(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_8) ).
cnf(p17_7,negated_conjecture,
p17(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17_7) ).
cnf(c57_is_not_p45_6,negated_conjecture,
~ p45(c57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c57_is_not_p45_6) ).
cnf(c55_is_not_p45_5,negated_conjecture,
~ p45(c55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c55_is_not_p45_5) ).
cnf(c58_is_not_p45_4,negated_conjecture,
~ p45(c58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c58_is_not_p45_4) ).
cnf(c47_is_p39_3,negated_conjecture,
p39(c47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c47_is_p39_3) ).
cnf(c56_is_p39_2,negated_conjecture,
p39(c56),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c56_is_p39_2) ).
cnf(c46_is_p39_1,negated_conjecture,
p39(c46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c46_is_p39_1) ).
cnf(i_0_89,negated_conjecture,
p42(f16(f7(c46)),f32(f10(f11(f12(c49))),f10(f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
p42_89,
[final] ).
cnf(i_0_90,negated_conjecture,
p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(f12(f12(f12(f15(f12(f15(f15(f15(f12(f15(f15(f12(f15(f12(f12(f15(f15(f15(f15(f15(f12(f15(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f15(f15(f15(f15(f12(f15(f12(f12(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c51),
p5_88,
[final] ).
cnf(i_0_91,negated_conjecture,
p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f12(f12(f15(f12(f12(f12(f15(f12(f15(f15(f15(f15(f12(f12(f12(f12(f12(f12(f12(f15(f12(f15(f15(f15(f15(f15(f12(f12(f12(f15(f12(f15(f12(f15(f15(f12(f15(f12(f15(f15(f12(f12(f15(f12(f12(f12(f15(f15(f15(f12(f15(f12(f15(f12(f15(f12(f15(f15(f15(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c50),
p5_87,
[final] ).
cnf(i_0_92,negated_conjecture,
p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c47)),
p43_84,
[final] ).
cnf(i_0_93,negated_conjecture,
p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c46)),
p43_83,
[final] ).
cnf(i_0_94,negated_conjecture,
p6(f35(f7(c46),f13(f35(f10(f11(f15(f12(c49)))),f35(f36(f10(f11(f12(c49))),c62),f35(f36(f10(f11(f12(c49))),c62),f38(f10(f11(f15(f12(c49)))))))))),c63),
p6_86,
[final] ).
cnf(i_0_95,negated_conjecture,
~ p42(f16(c62),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))),
not_p42_78,
[final] ).
cnf(i_0_96,negated_conjecture,
p41(f16(f7(c46)),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))),
p41_80,
[final] ).
cnf(i_0_97,negated_conjecture,
p42(f16(c60),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
p42_77,
[final] ).
cnf(i_0_98,negated_conjecture,
p42(f16(c61),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
p42_76,
[final] ).
cnf(i_0_99,negated_conjecture,
p42(f16(c59),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))),
p42_75,
[final] ).
cnf(i_0_100,negated_conjecture,
p6(f7(c58),f35(f7(c47),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f35(f36(f10(f11(f12(c49))),c60),f36(f10(f11(f12(c49))),c61)))))),
p6_85,
[final] ).
cnf(i_0_101,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56)),c57),
p5_60,
[final] ).
cnf(i_0_102,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54)),c55),
p5_59,
[final] ).
cnf(i_0_103,negated_conjecture,
p5(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54)),c58),
p5_58,
[final] ).
cnf(i_0_104,negated_conjecture,
p5(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),c56),
p5_57,
[final] ).
cnf(i_0_105,negated_conjecture,
( p22(f25(X1,X2,X3,X4),f25(X5,X6,X7,X8))
| ~ p5(X3,X7)
| ~ p5(X4,X8)
| ~ p24(X1,X5)
| ~ p5(X2,X6) ),
p22_81,
[final] ).
cnf(i_0_106,negated_conjecture,
( p22(f31(X1,X2,X3,X4),f31(X5,X6,X7,X8))
| ~ p5(X3,X7)
| ~ p5(X4,X8)
| ~ p24(X1,X5)
| ~ p5(X2,X6) ),
p22_82,
[final] ).
cnf(i_0_107,negated_conjecture,
p6(f7(c57),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f36(f10(f11(f12(c49))),c60)))),
p6_79,
[final] ).
cnf(i_0_108,negated_conjecture,
p6(f7(c55),f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59)))),
p6_74,
[final] ).
cnf(i_0_109,negated_conjecture,
p6(f7(c56),f37(f35(f7(c50),f7(c46)),f7(c55))),
p6_56,
[final] ).
cnf(i_0_110,negated_conjecture,
( p19(f21(X1,X2),f21(X3,X4))
| ~ p9(X1,X3)
| ~ p9(X2,X4) ),
p19_73,
[final] ).
cnf(i_0_111,negated_conjecture,
( p24(f27(X1,X2),f27(X3,X4))
| ~ p2(X1,X3)
| ~ p26(X2,X4) ),
p24_72,
[final] ).
cnf(i_0_112,negated_conjecture,
( p6(f14(X1,X2),f14(X3,X4))
| ~ p6(X1,X3)
| ~ p9(X2,X4) ),
p6_71,
[final] ).
cnf(i_0_113,negated_conjecture,
( p6(f32(X1,X2),f32(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
p6_70,
[final] ).
cnf(i_0_114,negated_conjecture,
( p6(f36(X1,X2),f36(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
p6_68,
[final] ).
cnf(i_0_115,negated_conjecture,
( p6(f37(X1,X2),f37(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
p6_67,
[final] ).
cnf(i_0_116,negated_conjecture,
( p6(f35(X1,X2),f35(X3,X4))
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
p6_69,
[final] ).
cnf(i_0_117,negated_conjecture,
( p17(f20(X1,X2),f20(X3,X4))
| ~ p19(X2,X4)
| ~ p9(X1,X3) ),
p17_66,
[final] ).
cnf(i_0_118,negated_conjecture,
p41(f8(f10(f11(f12(c49)))),f7(c46)),
p41_29,
[final] ).
cnf(i_0_119,negated_conjecture,
( p43(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p43(X3,X4) ),
p43_63,
[final] ).
cnf(i_0_120,negated_conjecture,
( p41(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p41(X3,X4) ),
p41_65,
[final] ).
cnf(i_0_121,negated_conjecture,
( p42(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X4,X2)
| ~ p42(X3,X4) ),
p42_64,
[final] ).
cnf(i_0_122,negated_conjecture,
( p40(X1,X2)
| ~ p40(X3,X4)
| ~ p6(X3,X1)
| ~ p3(X4,X2) ),
p40_61,
[final] ).
cnf(i_0_123,negated_conjecture,
( p44(X1,X2)
| ~ p44(X3,X4)
| ~ p5(X3,X1)
| ~ p33(X4,X2) ),
p44_62,
[final] ).
cnf(i_0_124,negated_conjecture,
( p42(X1,X2)
| ~ p42(X1,X3)
| ~ p42(X3,X2) ),
p42_47,
[final] ).
cnf(i_0_125,negated_conjecture,
( p19(X1,X2)
| ~ p19(X3,X1)
| ~ p19(X3,X2) ),
p19_55,
[final] ).
cnf(i_0_126,negated_conjecture,
( p2(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X3,X2) ),
p2_54,
[final] ).
cnf(i_0_127,negated_conjecture,
( p22(X1,X2)
| ~ p22(X3,X1)
| ~ p22(X3,X2) ),
p22_53,
[final] ).
cnf(i_0_128,negated_conjecture,
( p24(X1,X2)
| ~ p24(X3,X1)
| ~ p24(X3,X2) ),
p24_52,
[final] ).
cnf(i_0_129,negated_conjecture,
( p26(X1,X2)
| ~ p26(X3,X1)
| ~ p26(X3,X2) ),
p26_51,
[final] ).
cnf(i_0_130,negated_conjecture,
( p28(X1,X2)
| ~ p28(X3,X1)
| ~ p28(X3,X2) ),
p28_50,
[final] ).
cnf(i_0_131,negated_conjecture,
( p3(X1,X2)
| ~ p3(X3,X1)
| ~ p3(X3,X2) ),
p3_49,
[final] ).
cnf(i_0_132,negated_conjecture,
( p33(X1,X2)
| ~ p33(X3,X1)
| ~ p33(X3,X2) ),
p33_48,
[final] ).
cnf(i_0_133,negated_conjecture,
( p5(X1,X2)
| ~ p5(X3,X1)
| ~ p5(X3,X2) ),
p5_46,
[final] ).
cnf(i_0_134,negated_conjecture,
( p6(X1,X2)
| ~ p6(X3,X1)
| ~ p6(X3,X2) ),
p6_45,
[final] ).
cnf(i_0_135,negated_conjecture,
( p9(X1,X2)
| ~ p9(X3,X1)
| ~ p9(X3,X2) ),
p9_44,
[final] ).
cnf(i_0_136,negated_conjecture,
( p17(X1,X2)
| ~ p17(X3,X1)
| ~ p17(X3,X2) ),
p17_43,
[final] ).
cnf(i_0_137,negated_conjecture,
( p3(f4(X1),f4(X2))
| ~ p2(X1,X2) ),
p3_31,
[final] ).
cnf(i_0_138,negated_conjecture,
( p33(f34(X1),f34(X2))
| ~ p2(X1,X2) ),
p33_32,
[final] ).
cnf(i_0_139,negated_conjecture,
( p5(f23(X1),f23(X2))
| ~ p22(X1,X2) ),
p5_34,
[final] ).
cnf(i_0_140,negated_conjecture,
( p5(f18(X1),f18(X2))
| ~ p17(X1,X2) ),
p5_33,
[final] ).
cnf(i_0_141,negated_conjecture,
( p6(f38(X1),f38(X2))
| ~ p6(X1,X2) ),
p6_38,
[final] ).
cnf(i_0_142,negated_conjecture,
( p6(f13(X1),f13(X2))
| ~ p6(X1,X2) ),
p6_36,
[final] ).
cnf(i_0_143,negated_conjecture,
( p6(f8(X1),f8(X2))
| ~ p6(X1,X2) ),
p6_40,
[final] ).
cnf(i_0_144,negated_conjecture,
( p6(f10(X1),f10(X2))
| ~ p9(X1,X2) ),
p6_35,
[final] ).
cnf(i_0_145,negated_conjecture,
( p6(f16(X1),f16(X2))
| ~ p6(X1,X2) ),
p6_37,
[final] ).
cnf(i_0_146,negated_conjecture,
( p6(f7(X1),f7(X2))
| ~ p5(X1,X2) ),
p6_39,
[final] ).
cnf(i_0_147,negated_conjecture,
( p9(f15(X1),f15(X2))
| ~ p9(X1,X2) ),
p9_30,
[final] ).
cnf(i_0_148,negated_conjecture,
( p9(f11(X1),f11(X2))
| ~ p9(X1,X2) ),
p9_41,
[final] ).
cnf(i_0_149,negated_conjecture,
( p9(f12(X1),f12(X2))
| ~ p9(X1,X2) ),
p9_42,
[final] ).
cnf(i_0_150,negated_conjecture,
( p42(X1,X2)
| ~ p41(X1,X2) ),
p42_26,
[final] ).
cnf(i_0_151,negated_conjecture,
( p45(X1)
| ~ p45(X2)
| ~ p5(X2,X1) ),
p45_28,
[final] ).
cnf(i_0_152,negated_conjecture,
( p39(X1)
| ~ p39(X2)
| ~ p5(X2,X1) ),
p39_27,
[final] ).
cnf(i_0_153,negated_conjecture,
p42(f16(c62),f16(f7(c46))),
p42_25,
[final] ).
cnf(i_0_154,negated_conjecture,
p40(f7(c47),f4(c48)),
p40_24,
[final] ).
cnf(i_0_155,negated_conjecture,
p40(f7(c46),f4(c48)),
p40_23,
[final] ).
cnf(i_0_156,negated_conjecture,
p44(c57,f34(c52)),
p44_22,
[final] ).
cnf(i_0_157,negated_conjecture,
p44(c55,f34(c52)),
p44_20,
[final] ).
cnf(i_0_158,negated_conjecture,
p44(c58,f34(c52)),
p44_19,
[final] ).
cnf(i_0_159,negated_conjecture,
p44(c56,f34(c52)),
p44_21,
[final] ).
cnf(i_0_160,negated_conjecture,
p19(X1,X1),
p19_18,
[final] ).
cnf(i_0_161,negated_conjecture,
p2(X1,X1),
p2_17,
[final] ).
cnf(i_0_162,negated_conjecture,
p22(X1,X1),
p22_16,
[final] ).
cnf(i_0_163,negated_conjecture,
p24(X1,X1),
p24_15,
[final] ).
cnf(i_0_164,negated_conjecture,
p26(X1,X1),
p26_14,
[final] ).
cnf(i_0_165,negated_conjecture,
p28(X1,X1),
p28_13,
[final] ).
cnf(i_0_166,negated_conjecture,
p3(X1,X1),
p3_12,
[final] ).
cnf(i_0_167,negated_conjecture,
p33(X1,X1),
p33_11,
[final] ).
cnf(i_0_168,negated_conjecture,
p5(X1,X1),
p5_10,
[final] ).
cnf(i_0_169,negated_conjecture,
p6(X1,X1),
p6_9,
[final] ).
cnf(i_0_170,negated_conjecture,
p9(X1,X1),
p9_8,
[final] ).
cnf(i_0_171,negated_conjecture,
p17(X1,X1),
p17_7,
[final] ).
cnf(i_0_172,negated_conjecture,
~ p45(c57),
c57_is_not_p45_6,
[final] ).
cnf(i_0_173,negated_conjecture,
~ p45(c55),
c55_is_not_p45_5,
[final] ).
cnf(i_0_174,negated_conjecture,
~ p45(c58),
c58_is_not_p45_4,
[final] ).
cnf(i_0_175,negated_conjecture,
p39(c47),
c47_is_p39_3,
[final] ).
cnf(i_0_176,negated_conjecture,
p39(c56),
c56_is_p39_2,
[final] ).
cnf(i_0_177,negated_conjecture,
p39(c46),
c46_is_p39_1,
[final] ).
cnf(i_0_178,plain,
p42(f8(f10(f11(f12(c49)))),f7(c46)),
inference(scs_inference,[],[i_0_118,i_0_150]) ).
cnf(i_0_179,plain,
( ~ p41(X1,X2)
| p42(X1,X2) ),
inference(rename_variables,[],[i_0_150]) ).
cnf(i_0_180,plain,
~ p45(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54))),
inference(scs_inference,[],[i_0_174,i_0_118,i_0_103,i_0_150,i_0_151]) ).
cnf(i_0_181,plain,
( ~ p5(X1,X2)
| p45(X2)
| ~ p45(X1) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_182,plain,
( p42(X1,f16(f7(c46)))
| ~ p42(X1,f16(c62)) ),
inference(scs_inference,[],[i_0_174,i_0_153,i_0_118,i_0_103,i_0_150,i_0_151,i_0_124]) ).
cnf(i_0_183,plain,
( ~ p42(X1,X2)
| p42(X3,X2)
| ~ p42(X3,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_184,plain,
( p39(c58)
| ~ p39(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54))) ),
inference(scs_inference,[],[i_0_174,i_0_153,i_0_118,i_0_103,i_0_150,i_0_151,i_0_124,i_0_152]) ).
cnf(i_0_185,plain,
( ~ p5(X1,X2)
| p39(X2)
| ~ p39(X1) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_186,plain,
( p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),X1)
| ~ p6(f7(c47),X1) ),
inference(scs_inference,[],[i_0_169,i_0_174,i_0_153,i_0_118,i_0_103,i_0_92,i_0_150,i_0_151,i_0_124,i_0_152,i_0_119]) ).
cnf(i_0_187,plain,
p6(X1,X1),
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_188,plain,
( ~ p43(X1,X2)
| p43(X3,X4)
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_189,plain,
( p41(f8(f10(f11(f12(c49)))),X1)
| ~ p6(f7(c46),X1) ),
inference(scs_inference,[],[i_0_169,i_0_187,i_0_174,i_0_153,i_0_118,i_0_103,i_0_92,i_0_150,i_0_151,i_0_124,i_0_152,i_0_119,i_0_120]) ).
cnf(i_0_190,plain,
p6(X1,X1),
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_191,plain,
( ~ p41(X1,X2)
| p41(X3,X4)
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_192,plain,
( p40(f37(f35(f7(c50),f7(c46)),f7(c55)),X1)
| ~ p40(f7(c56),X1) ),
inference(scs_inference,[],[i_0_166,i_0_169,i_0_187,i_0_174,i_0_109,i_0_153,i_0_118,i_0_103,i_0_92,i_0_150,i_0_151,i_0_124,i_0_152,i_0_119,i_0_120,i_0_122]) ).
cnf(i_0_193,plain,
( ~ p6(X1,X2)
| ~ p3(X3,X4)
| p40(X2,X4)
| ~ p40(X1,X3) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_194,plain,
( p44(c56,X1)
| ~ p44(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),X1) ),
inference(scs_inference,[],[i_0_166,i_0_167,i_0_169,i_0_187,i_0_174,i_0_109,i_0_153,i_0_118,i_0_104,i_0_103,i_0_92,i_0_150,i_0_151,i_0_124,i_0_152,i_0_119,i_0_120,i_0_122,i_0_123]) ).
cnf(i_0_195,plain,
( ~ p5(X1,X2)
| ~ p33(X3,X4)
| p44(X2,X4)
| ~ p44(X1,X3) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_196,plain,
~ p45(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54))),
inference(scs_inference,[],[i_0_102,i_0_173,i_0_151]) ).
cnf(i_0_197,plain,
( ~ p5(X1,X2)
| p45(X2)
| ~ p45(X1) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_198,plain,
( p42(X1,f7(c46))
| ~ p42(X1,f8(f10(f11(f12(c49))))) ),
inference(scs_inference,[],[i_0_178,i_0_102,i_0_173,i_0_151,i_0_124]) ).
cnf(i_0_199,plain,
( ~ p42(X1,X2)
| p42(X3,X2)
| ~ p42(X3,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_200,plain,
( p39(c55)
| ~ p39(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54))) ),
inference(scs_inference,[],[i_0_178,i_0_102,i_0_173,i_0_151,i_0_124,i_0_152]) ).
cnf(i_0_201,plain,
( ~ p5(X1,X2)
| p39(X2)
| ~ p39(X1) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_202,plain,
( p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),X1)
| ~ p6(f7(c46),X1) ),
inference(scs_inference,[],[i_0_178,i_0_169,i_0_102,i_0_173,i_0_93,i_0_151,i_0_124,i_0_152,i_0_119]) ).
cnf(i_0_203,plain,
p6(X1,X1),
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_204,plain,
( ~ p43(X1,X2)
| p43(X3,X4)
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
inference(rename_variables,[],[i_0_119]) ).
cnf(i_0_205,plain,
( p40(f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f36(f10(f11(f12(c49))),c60))),X1)
| ~ p40(f7(c57),X1) ),
inference(scs_inference,[],[i_0_178,i_0_169,i_0_102,i_0_107,i_0_166,i_0_173,i_0_93,i_0_151,i_0_124,i_0_152,i_0_119,i_0_122]) ).
cnf(i_0_206,plain,
( ~ p6(X1,X2)
| ~ p3(X3,X4)
| p40(X2,X4)
| ~ p40(X1,X3) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_207,plain,
( p44(c55,X1)
| ~ p44(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54)),X1) ),
inference(scs_inference,[],[i_0_178,i_0_169,i_0_102,i_0_107,i_0_166,i_0_167,i_0_173,i_0_93,i_0_151,i_0_124,i_0_152,i_0_119,i_0_122,i_0_123]) ).
cnf(i_0_208,plain,
( ~ p5(X1,X2)
| ~ p33(X3,X4)
| p44(X2,X4)
| ~ p44(X1,X3) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_209,plain,
~ p45(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56))),
inference(scs_inference,[],[i_0_101,i_0_172,i_0_151]) ).
cnf(i_0_210,plain,
( ~ p5(X1,X2)
| p45(X2)
| ~ p45(X1) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_211,plain,
( p39(c57)
| ~ p39(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56))) ),
inference(scs_inference,[],[i_0_101,i_0_172,i_0_151,i_0_152]) ).
cnf(i_0_212,plain,
( ~ p5(X1,X2)
| p39(X2)
| ~ p39(X1) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_213,plain,
( p40(f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59))),X1)
| ~ p40(f7(c55),X1) ),
inference(scs_inference,[],[i_0_101,i_0_108,i_0_166,i_0_172,i_0_151,i_0_152,i_0_122]) ).
cnf(i_0_214,plain,
( ~ p6(X1,X2)
| ~ p3(X3,X4)
| p40(X2,X4)
| ~ p40(X1,X3) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_215,plain,
( p44(c57,X1)
| ~ p44(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56)),X1) ),
inference(scs_inference,[],[i_0_101,i_0_108,i_0_166,i_0_167,i_0_172,i_0_151,i_0_152,i_0_122,i_0_123]) ).
cnf(i_0_216,plain,
( ~ p5(X1,X2)
| ~ p33(X3,X4)
| p44(X2,X4)
| ~ p44(X1,X3) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_217,plain,
( p45(c56)
| ~ p45(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55))) ),
inference(scs_inference,[],[i_0_104,i_0_151]) ).
cnf(i_0_218,plain,
( ~ p5(X1,X2)
| p45(X2)
| ~ p45(X1) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_219,plain,
( p40(f35(f7(c47),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f35(f36(f10(f11(f12(c49))),c60),f36(f10(f11(f12(c49))),c61))))),X1)
| ~ p40(f7(c58),X1) ),
inference(scs_inference,[],[i_0_104,i_0_100,i_0_166,i_0_151,i_0_122]) ).
cnf(i_0_220,plain,
( ~ p6(X1,X2)
| ~ p3(X3,X4)
| p40(X2,X4)
| ~ p40(X1,X3) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_221,plain,
( p44(c58,X1)
| ~ p44(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54)),X1) ),
inference(scs_inference,[],[i_0_104,i_0_100,i_0_103,i_0_166,i_0_167,i_0_151,i_0_122,i_0_123]) ).
cnf(i_0_222,plain,
( ~ p5(X1,X2)
| ~ p33(X3,X4)
| p44(X2,X4)
| ~ p44(X1,X3) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_223,plain,
p5(c56,f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55))),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_133]) ).
cnf(i_0_224,plain,
p5(X1,X1),
inference(rename_variables,[],[i_0_168]) ).
cnf(i_0_225,plain,
( ~ p5(X1,X2)
| p5(X3,X2)
| ~ p5(X1,X3) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_226,plain,
p39(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55))),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_176,i_0_133,i_0_152]) ).
cnf(i_0_227,plain,
( ~ p5(X1,X2)
| p39(X2)
| ~ p39(X1) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_228,plain,
p44(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),f34(c52)),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_167,i_0_176,i_0_159,i_0_133,i_0_152,i_0_123]) ).
cnf(i_0_229,plain,
p33(X1,X1),
inference(rename_variables,[],[i_0_167]) ).
cnf(i_0_230,plain,
( ~ p5(X1,X2)
| ~ p33(X3,X4)
| p44(X2,X4)
| ~ p44(X1,X3) ),
inference(rename_variables,[],[i_0_123]) ).
cnf(i_0_231,plain,
( p42(X1,f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))
| ~ p42(X1,f16(c60)) ),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_167,i_0_176,i_0_159,i_0_97,i_0_133,i_0_152,i_0_123,i_0_124]) ).
cnf(i_0_232,plain,
( ~ p42(X1,X2)
| p42(X3,X2)
| ~ p42(X3,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_233,plain,
( p45(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)))
| ~ p45(c56) ),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_167,i_0_176,i_0_159,i_0_97,i_0_133,i_0_152,i_0_123,i_0_124,i_0_151]) ).
cnf(i_0_234,plain,
( ~ p5(X1,X2)
| p45(X2)
| ~ p45(X1) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_235,plain,
( p41(f16(f7(c46)),X1)
| ~ p6(f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49)))))))))),X1) ),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_169,i_0_167,i_0_176,i_0_159,i_0_96,i_0_97,i_0_133,i_0_152,i_0_123,i_0_124,i_0_151,i_0_120]) ).
cnf(i_0_236,plain,
p6(X1,X1),
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_237,plain,
( ~ p41(X1,X2)
| p41(X3,X4)
| ~ p6(X1,X3)
| ~ p6(X2,X4) ),
inference(rename_variables,[],[i_0_120]) ).
cnf(i_0_238,plain,
( p40(c63,X1)
| ~ p40(f35(f7(c46),f13(f35(f10(f11(f15(f12(c49)))),f35(f36(f10(f11(f12(c49))),c62),f35(f36(f10(f11(f12(c49))),c62),f38(f10(f11(f15(f12(c49)))))))))),X1) ),
inference(scs_inference,[],[i_0_104,i_0_168,i_0_169,i_0_94,i_0_166,i_0_167,i_0_176,i_0_159,i_0_96,i_0_97,i_0_133,i_0_152,i_0_123,i_0_124,i_0_151,i_0_120,i_0_122]) ).
cnf(i_0_239,plain,
( ~ p6(X1,X2)
| ~ p3(X3,X4)
| p40(X2,X4)
| ~ p40(X1,X3) ),
inference(rename_variables,[],[i_0_122]) ).
cnf(i_0_240,plain,
( p42(X1,f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))
| ~ p42(X1,f16(c61)) ),
inference(scs_inference,[],[i_0_98,i_0_124]) ).
cnf(i_0_241,plain,
( ~ p42(X1,X2)
| p42(X3,X2)
| ~ p42(X3,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_242,plain,
( p42(X1,f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))
| ~ p42(X1,f16(c59)) ),
inference(scs_inference,[],[i_0_99,i_0_124]) ).
cnf(i_0_243,plain,
( ~ p42(X1,X2)
| p42(X3,X2)
| ~ p42(X3,X1) ),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_244,plain,
p42(f16(f7(c46)),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))),
inference(scs_inference,[],[i_0_96,i_0_150]) ).
cnf(i_0_245,plain,
( ~ p41(X1,X2)
| p42(X1,X2) ),
inference(rename_variables,[],[i_0_150]) ).
cnf(i_0_246,plain,
$false,
inference(scs_inference,[],[i_0_153,i_0_96,i_0_95,i_0_150,i_0_124]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN711-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n002.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 08:44:16 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.55/1.62 % Version : CSE_E---1.7
% 0.55/1.62 % Problem : theBenchmark.p
% 0.55/1.62 % SZS status Unsatisfiable for theBenchmark.p
% 0.55/1.62 % SZS output start CNFRefutation
% See solution above
% 0.65/1.77 % Total time : 1.273s
%------------------------------------------------------------------------------