%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYN616-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 : n015.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:45 PM UTC 2026
% Result : Unsatisfiable 49.32s 25.67s
% Output : CNFRefutation 49.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 32
% Syntax : Number of clauses : 124 ( 57 unt; 0 nHn; 97 RR)
% Number of literals : 264 ( 0 equ; 154 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 226 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p14_30,negated_conjecture,
~ p14(f7(c22,f12(f8(c21,f3(f5(c20))),c28)),f3(f5(c20)),f6(c21)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p14_30) ).
cnf(p14_29,negated_conjecture,
p14(f7(c22,f12(f8(c21,f3(f5(c20))),c25)),f3(f5(c20)),f6(c21)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_29) ).
cnf(p2_32,negated_conjecture,
( p2(f11(X1,X2,X3),f11(X4,X5,X6))
| ~ p2(X3,X6)
| ~ p9(X1,X4)
| ~ p10(X2,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_32) ).
cnf(p14_31,negated_conjecture,
( p14(X1,X2,X3)
| ~ p2(X4,X3)
| ~ p2(X5,X2)
| ~ p2(X6,X1)
| ~ p14(X6,X5,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_31) ).
cnf(p14_25,negated_conjecture,
p14(f7(c22,f8(c21,f3(f5(c20)))),f3(f5(c20)),f6(c21)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14_25) ).
cnf(p2_19,negated_conjecture,
p2(f11(c23,c24,f3(f5(c20))),f8(c21,f3(f5(c20)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_19) ).
cnf(p15_20,negated_conjecture,
( p15(X1,c24)
| ~ p17(X1)
| ~ p16(X1,f8(c21,f3(f5(c20)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15_20) ).
cnf(p2_27,negated_conjecture,
( p2(f12(X1,X2),f12(X3,X4))
| ~ p2(X1,X3)
| ~ p2(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_27) ).
cnf(p2_28,negated_conjecture,
( p2(f7(X1,X2),f7(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_28) ).
cnf(p2_26,negated_conjecture,
( p2(f8(X1,X2),f8(X3,X4))
| ~ p2(X1,X3)
| ~ p2(X2,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_26) ).
cnf(p16_23,negated_conjecture,
( p16(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X4,X2)
| ~ p16(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16_23) ).
cnf(p13_21,negated_conjecture,
( p13(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X4,X2)
| ~ p13(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p13_21) ).
cnf(p15_24,negated_conjecture,
( p15(X1,X2)
| ~ p15(X3,X4)
| ~ p2(X3,X1)
| ~ p10(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15_24) ).
cnf(p19_22,negated_conjecture,
( p19(X1,X2)
| ~ p18(X3,X1)
| ~ p19(X3,X4)
| ~ p10(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_22) ).
cnf(p18_18,negated_conjecture,
( p18(X1,X2)
| ~ p18(X3,X1)
| ~ p18(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p18_18) ).
cnf(p2_17,negated_conjecture,
( p2(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_17) ).
cnf(p9_16,negated_conjecture,
( p9(X1,X2)
| ~ p9(X3,X1)
| ~ p9(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_16) ).
cnf(p10_15,negated_conjecture,
( p10(X1,X2)
| ~ p10(X3,X1)
| ~ p10(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p10_15) ).
cnf(p2_11,negated_conjecture,
( p2(f6(X1),f6(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_11) ).
cnf(p2_12,negated_conjecture,
( p2(f3(X1),f3(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_12) ).
cnf(p2_13,negated_conjecture,
( p2(f4(X1),f4(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_13) ).
cnf(p2_14,negated_conjecture,
( p2(f5(X1),f5(X2))
| ~ p2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_14) ).
cnf(p13_9,negated_conjecture,
p13(f3(f4(f5(c20))),c21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p13_9) ).
cnf(p17_10,negated_conjecture,
( p17(X1)
| ~ p17(X2)
| ~ p2(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17_10) ).
cnf(not_p15_8,negated_conjecture,
~ p15(c25,c27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p15_8) ).
cnf(p18_5,negated_conjecture,
p18(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p18_5) ).
cnf(p2_4,negated_conjecture,
p2(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_4) ).
cnf(p9_3,negated_conjecture,
p9(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9_3) ).
cnf(p10_2,negated_conjecture,
p10(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p10_2) ).
cnf(p19_6,negated_conjecture,
p19(c26,c27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19_6) ).
cnf(p2_7,negated_conjecture,
p2(c25,c28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_7) ).
cnf(c28_is_p17_1,negated_conjecture,
p17(c28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c28_is_p17_1) ).
cnf(i_0_32,negated_conjecture,
~ p14(f7(c22,f12(f8(c21,f3(f5(c20))),c28)),f3(f5(c20)),f6(c21)),
not_p14_30,
[final] ).
cnf(i_0_33,negated_conjecture,
p14(f7(c22,f12(f8(c21,f3(f5(c20))),c25)),f3(f5(c20)),f6(c21)),
p14_29,
[final] ).
cnf(i_0_34,negated_conjecture,
( p2(f11(X1,X2,X3),f11(X4,X5,X6))
| ~ p2(X3,X6)
| ~ p9(X1,X4)
| ~ p10(X2,X5) ),
p2_32,
[final] ).
cnf(i_0_35,negated_conjecture,
( p14(X1,X2,X3)
| ~ p2(X4,X3)
| ~ p2(X5,X2)
| ~ p2(X6,X1)
| ~ p14(X6,X5,X4) ),
p14_31,
[final] ).
cnf(i_0_36,negated_conjecture,
p14(f7(c22,f8(c21,f3(f5(c20)))),f3(f5(c20)),f6(c21)),
p14_25,
[final] ).
cnf(i_0_37,negated_conjecture,
p2(f11(c23,c24,f3(f5(c20))),f8(c21,f3(f5(c20)))),
p2_19,
[final] ).
cnf(i_0_38,negated_conjecture,
( p15(X1,c24)
| ~ p17(X1)
| ~ p16(X1,f8(c21,f3(f5(c20)))) ),
p15_20,
[final] ).
cnf(i_0_39,negated_conjecture,
( p2(f12(X1,X2),f12(X3,X4))
| ~ p2(X1,X3)
| ~ p2(X2,X4) ),
p2_27,
[final] ).
cnf(i_0_40,negated_conjecture,
( p2(f7(X1,X2),f7(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3) ),
p2_28,
[final] ).
cnf(i_0_41,negated_conjecture,
( p2(f8(X1,X2),f8(X3,X4))
| ~ p2(X1,X3)
| ~ p2(X2,X4) ),
p2_26,
[final] ).
cnf(i_0_42,negated_conjecture,
( p16(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X4,X2)
| ~ p16(X3,X4) ),
p16_23,
[final] ).
cnf(i_0_43,negated_conjecture,
( p13(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X4,X2)
| ~ p13(X3,X4) ),
p13_21,
[final] ).
cnf(i_0_44,negated_conjecture,
( p15(X1,X2)
| ~ p15(X3,X4)
| ~ p2(X3,X1)
| ~ p10(X4,X2) ),
p15_24,
[final] ).
cnf(i_0_45,negated_conjecture,
( p19(X1,X2)
| ~ p18(X3,X1)
| ~ p19(X3,X4)
| ~ p10(X4,X2) ),
p19_22,
[final] ).
cnf(i_0_46,negated_conjecture,
( p18(X1,X2)
| ~ p18(X3,X1)
| ~ p18(X3,X2) ),
p18_18,
[final] ).
cnf(i_0_47,negated_conjecture,
( p2(X1,X2)
| ~ p2(X3,X1)
| ~ p2(X3,X2) ),
p2_17,
[final] ).
cnf(i_0_48,negated_conjecture,
( p9(X1,X2)
| ~ p9(X3,X1)
| ~ p9(X3,X2) ),
p9_16,
[final] ).
cnf(i_0_49,negated_conjecture,
( p10(X1,X2)
| ~ p10(X3,X1)
| ~ p10(X3,X2) ),
p10_15,
[final] ).
cnf(i_0_50,negated_conjecture,
( p2(f6(X1),f6(X2))
| ~ p2(X1,X2) ),
p2_11,
[final] ).
cnf(i_0_51,negated_conjecture,
( p2(f3(X1),f3(X2))
| ~ p2(X1,X2) ),
p2_12,
[final] ).
cnf(i_0_52,negated_conjecture,
( p2(f4(X1),f4(X2))
| ~ p2(X1,X2) ),
p2_13,
[final] ).
cnf(i_0_53,negated_conjecture,
( p2(f5(X1),f5(X2))
| ~ p2(X1,X2) ),
p2_14,
[final] ).
cnf(i_0_54,negated_conjecture,
p13(f3(f4(f5(c20))),c21),
p13_9,
[final] ).
cnf(i_0_55,negated_conjecture,
( p17(X1)
| ~ p17(X2)
| ~ p2(X2,X1) ),
p17_10,
[final] ).
cnf(i_0_56,negated_conjecture,
~ p15(c25,c27),
not_p15_8,
[final] ).
cnf(i_0_57,negated_conjecture,
p18(X1,X1),
p18_5,
[final] ).
cnf(i_0_58,negated_conjecture,
p2(X1,X1),
p2_4,
[final] ).
cnf(i_0_59,negated_conjecture,
p9(X1,X1),
p9_3,
[final] ).
cnf(i_0_60,negated_conjecture,
p10(X1,X1),
p10_2,
[final] ).
cnf(i_0_61,negated_conjecture,
p19(c26,c27),
p19_6,
[final] ).
cnf(i_0_62,negated_conjecture,
p2(c25,c28),
p2_7,
[final] ).
cnf(i_0_63,negated_conjecture,
p17(c28),
c28_is_p17_1,
[final] ).
cnf(i_0_64,plain,
( p17(f8(c21,f3(f5(c20))))
| ~ p17(f11(c23,c24,f3(f5(c20)))) ),
inference(scs_inference,[],[i_0_37,i_0_55]) ).
cnf(i_0_65,plain,
( ~ p2(X1,X2)
| p17(X2)
| ~ p17(X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_66,plain,
( p13(f3(f4(f5(c20))),X1)
| ~ p2(c21,X1) ),
inference(scs_inference,[],[i_0_58,i_0_37,i_0_54,i_0_55,i_0_43]) ).
cnf(i_0_67,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_68,plain,
( ~ p13(X1,X2)
| p13(X3,X4)
| ~ p2(X1,X3)
| ~ p2(X2,X4) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_69,plain,
( p15(c28,X1)
| ~ p15(c25,X1) ),
inference(scs_inference,[],[i_0_58,i_0_60,i_0_62,i_0_37,i_0_54,i_0_55,i_0_43,i_0_44]) ).
cnf(i_0_70,plain,
( ~ p2(X1,X2)
| ~ p10(X3,X4)
| p15(X2,X4)
| ~ p15(X1,X3) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_71,plain,
( p15(f8(c21,f3(f5(c20))),X1)
| ~ p15(f11(c23,c24,f3(f5(c20))),X1) ),
inference(scs_inference,[],[i_0_60,i_0_37,i_0_44]) ).
cnf(i_0_72,plain,
( ~ p2(X1,X2)
| ~ p10(X3,X4)
| p15(X2,X4)
| ~ p15(X1,X3) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_73,plain,
p2(c28,c25),
inference(scs_inference,[],[i_0_62,i_0_58,i_0_47]) ).
cnf(i_0_74,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_75,plain,
( ~ p2(X1,X2)
| p2(X3,X2)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_76,plain,
p17(c25),
inference(scs_inference,[],[i_0_62,i_0_58,i_0_63,i_0_47,i_0_55]) ).
cnf(i_0_77,plain,
( ~ p2(X1,X2)
| p17(X2)
| ~ p17(X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_78,plain,
~ p15(c28,c27),
inference(scs_inference,[],[i_0_62,i_0_58,i_0_60,i_0_56,i_0_63,i_0_47,i_0_55,i_0_44]) ).
cnf(i_0_79,plain,
p10(X1,X1),
inference(rename_variables,[],[i_0_60]) ).
cnf(i_0_80,plain,
( ~ p2(X1,X2)
| ~ p10(X3,X4)
| p15(X2,X4)
| ~ p15(X1,X3) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_81,plain,
p2(f8(c21,f3(f5(c20))),f11(c23,c24,f3(f5(c20)))),
inference(scs_inference,[],[i_0_37,i_0_58,i_0_47]) ).
cnf(i_0_82,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_83,plain,
( ~ p2(X1,X2)
| p2(X3,X2)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_84,plain,
( p17(f11(c23,c24,f3(f5(c20))))
| ~ p17(f8(c21,f3(f5(c20)))) ),
inference(scs_inference,[],[i_0_37,i_0_58,i_0_47,i_0_55]) ).
cnf(i_0_85,plain,
( ~ p2(X1,X2)
| p17(X2)
| ~ p17(X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_86,plain,
( p17(f8(c21,f3(f5(c20))))
| ~ p17(f8(c21,f3(f5(c20)))) ),
inference(scs_inference,[],[i_0_37,i_0_58,i_0_47,i_0_55,i_0_85]) ).
cnf(i_0_87,plain,
( ~ p2(X1,X2)
| p17(X2)
| ~ p17(X1) ),
inference(rename_variables,[],[i_0_55]) ).
cnf(i_0_88,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_90,plain,
( p15(f11(c23,c24,f3(f5(c20))),X1)
| ~ p15(f8(c21,f3(f5(c20))),X1) ),
inference(scs_inference,[],[i_0_81,i_0_60,i_0_44]) ).
cnf(i_0_91,plain,
( ~ p2(X1,X2)
| ~ p10(X3,X4)
| p15(X2,X4)
| ~ p15(X1,X3) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_92,plain,
( p15(f8(c21,f3(f5(c20))),X1)
| ~ p15(f8(c21,f3(f5(c20))),X1) ),
inference(scs_inference,[],[i_0_37,i_0_81,i_0_60,i_0_44,i_0_91]) ).
cnf(i_0_93,plain,
( ~ p2(X1,X2)
| ~ p10(X3,X4)
| p15(X2,X4)
| ~ p15(X1,X3) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_94,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_96,plain,
( ~ p2(f3(f5(c20)),f3(f5(c20)))
| ~ p2(f7(c22,f8(c21,f3(f5(c20)))),f7(c22,f12(f8(c21,f3(f5(c20))),c28))) ),
inference(scs_inference,[],[i_0_32,i_0_58,i_0_36,i_0_35]) ).
cnf(i_0_97,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_98,plain,
( ~ p14(X1,X2,X3)
| p14(X4,X5,X6)
| ~ p2(X3,X6)
| ~ p2(X2,X5)
| ~ p2(X1,X4) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_99,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_100,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_101,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_103,plain,
~ p2(f7(c22,f8(c21,f3(f5(c20)))),f7(c22,f12(f8(c21,f3(f5(c20))),c28))),
inference(scs_inference,[],[i_0_58,i_0_96]) ).
cnf(i_0_104,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_105,plain,
~ p2(f8(c21,f3(f5(c20))),f12(f8(c21,f3(f5(c20))),c28)),
inference(scs_inference,[],[i_0_58,i_0_104,i_0_96,i_0_40]) ).
cnf(i_0_106,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_107,plain,
( p2(f7(X1,X2),f7(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_108,plain,
~ p2(f7(c22,f12(f8(c21,f3(f5(c20))),c28)),f7(c22,f8(c21,f3(f5(c20))))),
inference(scs_inference,[],[i_0_58,i_0_104,i_0_106,i_0_96,i_0_40,i_0_47]) ).
cnf(i_0_109,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_110,plain,
( ~ p2(X1,X2)
| p2(X3,X2)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_111,plain,
( ~ p2(f3(f5(c20)),f3(f5(c20)))
| ~ p2(f7(c22,f12(f8(c21,f3(f5(c20))),c25)),f7(c22,f12(f8(c21,f3(f5(c20))),c28))) ),
inference(scs_inference,[],[i_0_32,i_0_58,i_0_104,i_0_106,i_0_109,i_0_33,i_0_96,i_0_40,i_0_47,i_0_35]) ).
cnf(i_0_112,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_113,plain,
( ~ p14(X1,X2,X3)
| p14(X4,X5,X6)
| ~ p2(X3,X6)
| ~ p2(X2,X5)
| ~ p2(X1,X4) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_114,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_115,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_117,plain,
~ p2(f7(c22,f12(f8(c21,f3(f5(c20))),c25)),f7(c22,f12(f8(c21,f3(f5(c20))),c28))),
inference(scs_inference,[],[i_0_58,i_0_111]) ).
cnf(i_0_118,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_119,plain,
~ p2(f12(f8(c21,f3(f5(c20))),c28),f8(c21,f3(f5(c20)))),
inference(scs_inference,[],[i_0_58,i_0_118,i_0_108,i_0_111,i_0_40]) ).
cnf(i_0_120,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_121,plain,
( p2(f7(X1,X2),f7(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_122,plain,
~ p2(f11(c23,c24,f3(f5(c20))),f12(f8(c21,f3(f5(c20))),c28)),
inference(scs_inference,[],[i_0_37,i_0_58,i_0_118,i_0_108,i_0_111,i_0_40,i_0_47]) ).
cnf(i_0_123,plain,
( ~ p2(X1,X2)
| p2(X3,X2)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_124,plain,
~ p2(f12(f8(c21,f3(f5(c20))),c25),f12(f8(c21,f3(f5(c20))),c28)),
inference(scs_inference,[],[i_0_117,i_0_58,i_0_40]) ).
cnf(i_0_125,plain,
p2(X1,X1),
inference(rename_variables,[],[i_0_58]) ).
cnf(i_0_126,plain,
( p2(f7(X1,X2),f7(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_127,plain,
$false,
inference(scs_inference,[],[i_0_117,i_0_62,i_0_58,i_0_125,i_0_40,i_0_39]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN616-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 : n015.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:41:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 49.32/25.67 % Version : CSE_E---1.7
% 49.32/25.67 % Problem : theBenchmark.p
% 49.32/25.67 % SZS status Unsatisfiable for theBenchmark.p
% 49.32/25.67 % SZS output start CNFRefutation
% See solution above
% 49.45/25.76 % Total time : 25.321s
%------------------------------------------------------------------------------