%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n018.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:34:49 PM UTC 2026
% Result : Unsatisfiable 114.84s 59.40s
% Output : CNFRefutation 115.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 26
% Syntax : Number of clauses : 88 ( 83 unt; 0 nHn; 18 RR)
% Number of literals : 93 ( 92 equ; 20 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 4 con; 0-8 aty)
% Number of variables : 285 ( 27 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_029,axiom,
unifyoccurs(X1,var(X2)) = eq2(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
cnf(axiom_071,axiom,
apply1(lam3,X1) = var(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
cnf(axiom_034,axiom,
unifyloop(X1,cons(app(X2,X3),X4),cons(app(X5,X6),X7)) = aux3(X1,X4,X2,X3,X7,X5,X6,eq2(X2,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_034) ).
cnf(axiom_056,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
cnf(goal,negated_conjecture,
eq4(prop_unify_makes_equal(X1,X2),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
cnf(axiom_043,axiom,
prop_unify_makes_equal(X1,X2) = eq4(unificationOK(X1,X2),btrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
cnf(axiom_042,axiom,
unificationOK(X1,X2) = aux6(X1,X2,unify2(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
cnf(axiom_041,axiom,
unify2(X1,X2) = unifyloop(lam3,cons(X1,nil),cons(X2,nil)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
cnf(axiom_004,axiom,
aux3(X1,X2,X3,X4,X5,X6,X7,btrue) = unifyloop(X1,append(X4,X2),append(X7,X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_004) ).
cnf(axiom_047,axiom,
append(cons(X1,X2),X3) = cons(X1,append(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
cnf(axiom_046,axiom,
append(nil,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_046) ).
cnf(axiom_016,axiom,
fail(X1,cons(var(X2),X3),X4,X5) = unifyvar(X1,X2,X4,X5,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
cnf(axiom_065,axiom,
( eq3(app(X1,X3),app(X2,X4)) = eq(X3,X4)
| eq2(X1,X2) != btrue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
cnf(axiom_039,axiom,
unifyvar(X1,X2,var(X3),X4,X5) = aux5(X1,X2,X4,X5,X3,eq2(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
cnf(axiom_037,axiom,
unifyloop(X1,cons(var(X2),X3),cons(X4,X5)) = unifyvar(X1,X2,X4,X3,X5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
cnf(axiom_018,axiom,
subst(X1,app(X2,X3)) = app(X2,substList(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
cnf(axiom_008,axiom,
aux5(X1,X2,X3,X4,X5,btrue) = unifyloop(X1,X3,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
cnf(axiom_011,axiom,
aux6(X1,X2,just(X3)) = eq3(subst(X3,X1),subst(X3,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
cnf(axiom_031,axiom,
unifyloop(X1,nil,nil) = just(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
cnf(axiom_021,axiom,
substList(X1,cons(X2,X3)) = cons(subst(X1,X2),substList(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
cnf(axiom_020,axiom,
substList(X1,nil) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_020) ).
cnf(axiom_019,axiom,
subst(X1,var(X2)) = apply1(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_019) ).
cnf(axiom_060,axiom,
( eq(cons(X1,X3),cons(X2,X4)) = bfalse
| eq3(X1,X2) != bfalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_060) ).
cnf(axiom_054,axiom,
eq4(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_054) ).
cnf(axiom_058,axiom,
eq4(X1,X1) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_058) ).
cnf(axiom_063,axiom,
eq(cons(X1,X2),nil) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_063) ).
cnf(c_0_26,axiom,
unifyoccurs(X1,var(X2)) = eq2(X1,X2),
axiom_029 ).
cnf(c_0_27,axiom,
apply1(lam3,X1) = var(X1),
axiom_071 ).
cnf(c_0_28,axiom,
unifyloop(X1,cons(app(X2,X3),X4),cons(app(X5,X6),X7)) = aux3(X1,X4,X2,X3,X7,X5,X6,eq2(X2,X5)),
axiom_034 ).
cnf(c_0_29,plain,
unifyoccurs(X1,apply1(lam3,X2)) = eq2(X1,X2),
inference(rw,[status(thm)],[c_0_26,c_0_27]) ).
cnf(c_0_30,axiom,
eq2(X1,X1) = btrue,
axiom_056 ).
cnf(c_0_31,negated_conjecture,
eq4(prop_unify_makes_equal(X1,X2),bfalse) != btrue,
goal ).
cnf(c_0_32,axiom,
prop_unify_makes_equal(X1,X2) = eq4(unificationOK(X1,X2),btrue),
axiom_043 ).
cnf(c_0_33,axiom,
unificationOK(X1,X2) = aux6(X1,X2,unify2(X1,X2)),
axiom_042 ).
cnf(c_0_34,axiom,
unify2(X1,X2) = unifyloop(lam3,cons(X1,nil),cons(X2,nil)),
axiom_041 ).
cnf(c_0_35,plain,
unifyloop(X1,cons(app(X2,X3),X4),cons(app(X5,X6),X7)) = aux3(X1,X4,X2,X3,X7,X5,X6,unifyoccurs(X2,apply1(lam3,X5))),
inference(rw,[status(thm)],[c_0_28,c_0_29]) ).
cnf(c_0_36,plain,
unifyoccurs(X1,apply1(lam3,X1)) = btrue,
inference(rw,[status(thm)],[c_0_30,c_0_29]) ).
cnf(c_0_37,negated_conjecture,
eq4(eq4(aux6(X1,X2,unifyloop(lam3,cons(X1,nil),cons(X2,nil))),btrue),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_32]),c_0_33]),c_0_34]) ).
cnf(c_0_38,plain,
unifyloop(X1,cons(app(X2,X3),X4),cons(app(X2,X5),X6)) = aux3(X1,X4,X2,X3,X6,X2,X5,btrue),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_39,axiom,
aux3(X1,X2,X3,X4,X5,X6,X7,btrue) = unifyloop(X1,append(X4,X2),append(X7,X5)),
axiom_004 ).
cnf(c_0_40,axiom,
append(cons(X1,X2),X3) = cons(X1,append(X2,X3)),
axiom_047 ).
cnf(c_0_41,negated_conjecture,
eq4(eq4(aux6(app(X1,X2),app(X1,X3),aux3(lam3,nil,X1,X2,nil,X1,X3,btrue)),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_42,plain,
aux3(X1,X2,X3,cons(X4,X5),X6,X7,X8,btrue) = unifyloop(X1,cons(X4,append(X5,X2)),append(X8,X6)),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_43,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(X2,X3)),app(X1,X4),unifyloop(lam3,cons(X2,append(X3,nil)),append(X4,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_44,axiom,
append(nil,X1) = X1,
axiom_046 ).
cnf(c_0_45,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(X2,nil)),app(X1,X3),unifyloop(lam3,cons(X2,nil),append(X3,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_46,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(X2,nil)),app(X1,cons(X3,X4)),unifyloop(lam3,cons(X2,nil),cons(X3,append(X4,nil)))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_45,c_0_40]) ).
cnf(c_0_47,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,X3),nil)),app(X1,cons(app(X2,X4),X5)),aux3(lam3,nil,X2,X3,append(X5,nil),X2,X4,btrue)),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_46,c_0_38]) ).
cnf(c_0_48,plain,
aux3(X1,X2,X3,X4,X5,X6,nil,btrue) = unifyloop(X1,append(X4,X2),X5),
inference(spm,[status(thm)],[c_0_39,c_0_44]) ).
cnf(c_0_49,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,X3),nil)),app(X1,cons(app(X2,nil),X4)),unifyloop(lam3,append(X3,nil),append(X4,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_50,axiom,
fail(X1,cons(var(X2),X3),X4,X5) = unifyvar(X1,X2,X4,X5,X3),
axiom_016 ).
cnf(c_0_51,axiom,
( eq3(app(X1,X3),app(X2,X4)) = eq(X3,X4)
| eq2(X1,X2) != btrue ),
axiom_065 ).
cnf(c_0_52,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,X3),nil)),app(X1,cons(app(X2,nil),cons(X4,X5))),unifyloop(lam3,append(X3,nil),cons(X4,append(X5,nil)))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_49,c_0_40]) ).
cnf(c_0_53,axiom,
unifyvar(X1,X2,var(X3),X4,X5) = aux5(X1,X2,X4,X5,X3,eq2(X2,X3)),
axiom_039 ).
cnf(c_0_54,plain,
fail(X1,cons(apply1(lam3,X2),X3),X4,X5) = unifyvar(X1,X2,X4,X5,X3),
inference(rw,[status(thm)],[c_0_50,c_0_27]) ).
cnf(c_0_55,axiom,
unifyloop(X1,cons(var(X2),X3),cons(X4,X5)) = unifyvar(X1,X2,X4,X3,X5),
axiom_037 ).
cnf(c_0_56,plain,
( eq3(app(X1,X3),app(X2,X4)) = eq(X3,X4)
| unifyoccurs(X1,apply1(lam3,X2)) != btrue ),
inference(rw,[status(thm)],[c_0_51,c_0_29]) ).
cnf(c_0_57,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,X3),nil)),app(X1,cons(app(X2,nil),cons(X4,nil))),unifyloop(lam3,append(X3,nil),cons(X4,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_52,c_0_44]) ).
cnf(c_0_58,plain,
fail(X1,cons(apply1(lam3,X2),X5),apply1(lam3,X3),X4) = aux5(X1,X2,X4,X5,X3,unifyoccurs(X2,apply1(lam3,X3))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53,c_0_27]),c_0_29]),c_0_54]) ).
cnf(c_0_59,plain,
unifyloop(X1,cons(apply1(lam3,X2),X3),cons(X4,X5)) = fail(X1,cons(apply1(lam3,X2),X5),X4,X3),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_55,c_0_27]),c_0_54]) ).
cnf(c_0_60,plain,
eq3(app(X1,X2),app(X1,X3)) = eq(X2,X3),
inference(spm,[status(thm)],[c_0_56,c_0_36]) ).
cnf(c_0_61,axiom,
subst(X1,app(X2,X3)) = app(X2,substList(X1,X3)),
axiom_018 ).
cnf(c_0_62,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,cons(X3,X4)),nil)),app(X1,cons(app(X2,nil),cons(X5,nil))),unifyloop(lam3,cons(X3,append(X4,nil)),cons(X5,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_57,c_0_40]) ).
cnf(c_0_63,plain,
aux5(X1,X2,X3,X4,X5,unifyoccurs(X2,apply1(lam3,X5))) = unifyloop(X1,cons(apply1(lam3,X2),X3),cons(apply1(lam3,X5),X4)),
inference(rw,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_64,axiom,
aux5(X1,X2,X3,X4,X5,btrue) = unifyloop(X1,X3,X4),
axiom_008 ).
cnf(c_0_65,axiom,
aux6(X1,X2,just(X3)) = eq3(subst(X3,X1),subst(X3,X2)),
axiom_011 ).
cnf(c_0_66,axiom,
unifyloop(X1,nil,nil) = just(X1),
axiom_031 ).
cnf(c_0_67,plain,
eq3(app(X1,X2),subst(X3,app(X1,X4))) = eq(X2,substList(X3,X4)),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
cnf(c_0_68,axiom,
substList(X1,cons(X2,X3)) = cons(subst(X1,X2),substList(X1,X3)),
axiom_021 ).
cnf(c_0_69,axiom,
substList(X1,nil) = nil,
axiom_020 ).
cnf(c_0_70,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,cons(X3,nil)),nil)),app(X1,cons(app(X2,nil),cons(X4,nil))),unifyloop(lam3,cons(X3,nil),cons(X4,nil))),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_62,c_0_44]) ).
cnf(c_0_71,plain,
unifyloop(X1,cons(apply1(lam3,X2),X3),cons(apply1(lam3,X2),X4)) = unifyloop(X1,X3,X4),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_36]),c_0_64]) ).
cnf(c_0_72,plain,
aux6(X1,X2,unifyloop(X3,nil,nil)) = eq3(subst(X3,X1),subst(X3,X2)),
inference(rw,[status(thm)],[c_0_65,c_0_66]) ).
cnf(c_0_73,plain,
eq3(subst(X1,app(X2,X3)),subst(X4,app(X2,X5))) = eq(substList(X1,X3),substList(X4,X5)),
inference(spm,[status(thm)],[c_0_67,c_0_61]) ).
cnf(c_0_74,plain,
substList(X1,cons(X2,nil)) = cons(subst(X1,X2),nil),
inference(spm,[status(thm)],[c_0_68,c_0_69]) ).
cnf(c_0_75,axiom,
subst(X1,var(X2)) = apply1(X1,X2),
axiom_019 ).
cnf(c_0_76,plain,
subst(X1,app(X2,nil)) = app(X2,nil),
inference(spm,[status(thm)],[c_0_61,c_0_69]) ).
cnf(c_0_77,negated_conjecture,
eq4(eq4(aux6(app(X1,cons(app(X2,cons(apply1(lam3,X3),nil)),nil)),app(X1,cons(app(X2,nil),cons(apply1(lam3,X3),nil))),unifyloop(lam3,nil,nil)),btrue),bfalse) != btrue,
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_78,plain,
eq(substList(X1,X2),substList(X1,X3)) = aux6(app(X4,X2),app(X4,X3),unifyloop(X1,nil,nil)),
inference(spm,[status(thm)],[c_0_72,c_0_73]) ).
cnf(c_0_79,plain,
subst(X1,app(X2,cons(X3,nil))) = app(X2,cons(subst(X1,X3),nil)),
inference(spm,[status(thm)],[c_0_61,c_0_74]) ).
cnf(c_0_80,plain,
subst(X1,apply1(lam3,X2)) = apply1(X1,X2),
inference(rw,[status(thm)],[c_0_75,c_0_27]) ).
cnf(c_0_81,plain,
substList(X1,cons(app(X2,nil),X3)) = cons(app(X2,nil),substList(X1,X3)),
inference(spm,[status(thm)],[c_0_68,c_0_76]) ).
cnf(c_0_82,negated_conjecture,
eq4(eq4(eq(cons(app(X1,cons(apply1(lam3,X2),nil)),nil),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse) != btrue,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_77,c_0_78]),c_0_74]),c_0_79]),c_0_80]),c_0_81]),c_0_74]),c_0_80]) ).
cnf(c_0_83,axiom,
( eq(cons(X1,X3),cons(X2,X4)) = bfalse
| eq3(X1,X2) != bfalse ),
axiom_060 ).
cnf(c_0_84,axiom,
eq4(bfalse,btrue) = bfalse,
axiom_054 ).
cnf(c_0_85,axiom,
eq4(X1,X1) = btrue,
axiom_058 ).
cnf(c_0_86,axiom,
eq(cons(X1,X2),nil) = bfalse,
axiom_063 ).
cnf(c_0_87,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_84]),c_0_85]),c_0_60]),c_0_86])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n018.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 08:01:32 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 114.84/59.40 % Version : CSE_E---1.7
% 114.84/59.40 % Problem : theBenchmark.p
% 114.84/59.40 % SZS status Unsatisfiable for theBenchmark.p
% 114.84/59.40 % SZS output start CNFRefutation
% See solution above
% 115.15/59.79 % Total time : 45.038s
%------------------------------------------------------------------------------