%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:35:31 PM UTC 2026
% Result : Unsatisfiable 37.52s 6.01s
% Output : CNFRefutation 37.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 15
% Syntax : Number of clauses : 29 ( 29 unt; 0 nHn; 19 RR)
% Number of literals : 29 ( 28 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 6 con; 0-4 aty)
% Number of variables : 22 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t237,axiom,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi27,negated_conjecture,
ifeq2(p10(X25,X26),true,p16(f19(X25),f19(X26)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi61,negated_conjecture,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h53,plain,
p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(hyper_resolution,[status(thm)],[hi27,hi61]) ).
cnf(hi31,negated_conjecture,
ifeq2(p38(X27),true,p16(f19(f15(X27)),f28(f19(X27))),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi0,negated_conjecture,
p38(c56) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h0,plain,
p16(f19(f15(c56)),f28(f19(c56))) = true,
inference(hyper_resolution,[status(thm)],[hi31,hi0]) ).
cnf(hi10,negated_conjecture,
ifeq2(p38(X27),true,p38(f15(X27)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h1,plain,
p38(f15(c56)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi0]) ).
cnf(hi32,negated_conjecture,
ifeq2(p10(X0,X2),true,ifeq2(p10(X0,X1),true,p10(X1,X2),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi1,negated_conjecture,
p10(X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h51,plain,
p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48) = true,
inference(hyper_resolution,[status(thm)],[hi32,hi1,hi61]) ).
cnf(hi14,negated_conjecture,
ifeq2(p10(X98,X97),true,ifeq2(p38(X98),true,p38(X97),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi59,negated_conjecture,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h2437,plain,
p38(c48) = true,
inference(hyper_resolution,[status(thm)],[hi14,h51,hi59]) ).
cnf(hi49,negated_conjecture,
ifeq2(p37(X91,X92),true,ifeq2(p38(X92),true,ifeq2(p38(X91),true,p39(f19(X91),f19(X92)),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi9,negated_conjecture,
p37(f15(c56),c48) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h2438,plain,
p39(f19(f15(c56)),f19(c48)) = true,
inference(hyper_resolution,[status(thm)],[hi49,hi9,h2437,h1]) ).
cnf(hi47,negated_conjecture,
ifeq2(p39(X101,X102),true,ifeq2(p16(X101,X99),true,ifeq2(p16(X102,X100),true,p39(X99,X100),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t235,plain,
p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(hyper_resolution,[status(thm)],[hi47,h2438,h0,h53]) ).
cnf(t754,plain,
p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(orient,[status(thm)],[t235]) ).
cnf(t776,plain,
ifeq(true,true,a,b) = b,
inference(step,[status(thm)],[t237,t754]) ).
cnf(t25,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t257,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t777,plain,
a = b,
inference(step,[status(thm)],[t776,t257]) ).
cnf(t775,plain,
a = b,
inference(orient,[status(thm)],[t777]) ).
cnf(goal_0,negated_conjecture,
b != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
b != b,
inference(rw,[status(thm)],[goal_0,t775]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 02:07:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 37.52/6.01 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 37.52/6.01 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------