%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG030-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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 12:51:13 PM UTC 2026
% Result : Unsatisfiable 5.76s 1.21s
% Output : CNFRefutation 5.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of clauses : 65 ( 65 unt; 0 nHn; 51 RR)
% Number of literals : 65 ( 64 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 28 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = op1(sK2_ax3_U,sK1_ax3_V),
introduced(definition) ).
cnf(t44,plain,
op1(sK2_ax3_U,sK1_ax3_V) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t6,axiom,
ifeq2(sorti1(X1),true,j(h(X1)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
ifeq2(sorti1(X1),true,j(h(X1)),X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t8,axiom,
ifeq(sorti1(X1),true,ifeq(sorti1(X2),true,sorti1(op1(X2,X1)),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
ifeq(sorti1(X1),true,ifeq(sorti1(X2),true,sorti1(op1(X2,X1)),true),true) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t45,plain,
true = ifeq(sorti1(sK1_ax3_V),true,ifeq(sorti1(sK2_ax3_U),true,sorti1(sFlat0),true),true),
inference(cp,[status(thm)],[t26,t44]) ).
cnf(t0,axiom,
sorti1(sK1_ax3_V) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
sorti1(sK1_ax3_V) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t129,plain,
true = ifeq(true,true,ifeq(sorti1(sK2_ax3_U),true,sorti1(sFlat0),true),true),
inference(step,[status(thm)],[t45,t19]) ).
cnf(t2,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t130,plain,
true = ifeq(sorti1(sK2_ax3_U),true,sorti1(sFlat0),true),
inference(step,[status(thm)],[t129,t18]) ).
cnf(t1,axiom,
sorti1(sK2_ax3_U) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
sorti1(sK2_ax3_U) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t131,plain,
true = ifeq(true,true,sorti1(sFlat0),true),
inference(step,[status(thm)],[t130,t21]) ).
cnf(t132,plain,
true = sorti1(sFlat0),
inference(step,[status(thm)],[t131,t18]) ).
cnf(t55,plain,
sorti1(sFlat0) = true,
inference(orient,[status(thm)],[t132]) ).
cnf(t56,plain,
sFlat0 = ifeq2(true,true,j(h(sFlat0)),sFlat0),
inference(cp,[status(thm)],[t16,t55]) ).
cnf(t3,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t139,plain,
sFlat0 = j(h(sFlat0)),
inference(step,[status(thm)],[t56,t15]) ).
cnf(t98,plain,
j(h(sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t139]) ).
cnf(t14,axiom,
sFlat1 = op1(sK1_ax3_V,sK2_ax3_U),
introduced(definition) ).
cnf(t40,plain,
op1(sK1_ax3_V,sK2_ax3_U) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t10,axiom,
ifeq2(sorti2(X1),true,ifeq2(sorti2(X2),true,op2(X2,X1),op2(X1,X2)),op2(X1,X2)) = op2(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
ifeq2(sorti2(X1),true,ifeq2(sorti2(X2),true,op2(X2,X1),op2(X1,X2)),op2(X1,X2)) = op2(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
ifeq2(sorti1(X1),true,ifeq2(sorti1(X2),true,op2(h(X2),h(X1)),h(op1(X2,X1))),h(op1(X2,X1))) = h(op1(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
ifeq2(sorti1(X1),true,ifeq2(sorti1(X2),true,op2(h(X2),h(X1)),h(op1(X2,X1))),h(op1(X2,X1))) = h(op1(X2,X1)),
inference(orient,[status(thm)],[t11]) ).
cnf(t46,plain,
h(op1(sK2_ax3_U,sK1_ax3_V)) = ifeq2(sorti1(sK1_ax3_V),true,ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sFlat0)),h(op1(sK2_ax3_U,sK1_ax3_V))),
inference(cp,[status(thm)],[t34,t44]) ).
cnf(t146,plain,
h(sFlat0) = ifeq2(sorti1(sK1_ax3_V),true,ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sFlat0)),h(op1(sK2_ax3_U,sK1_ax3_V))),
inference(step,[status(thm)],[t46,t44]) ).
cnf(t147,plain,
h(sFlat0) = ifeq2(true,true,ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sFlat0)),h(op1(sK2_ax3_U,sK1_ax3_V))),
inference(step,[status(thm)],[t146,t19]) ).
cnf(t148,plain,
h(sFlat0) = ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sFlat0)),
inference(step,[status(thm)],[t147,t15]) ).
cnf(t149,plain,
h(sFlat0) = ifeq2(true,true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sFlat0)),
inference(step,[status(thm)],[t148,t21]) ).
cnf(t150,plain,
h(sFlat0) = op2(h(sK2_ax3_U),h(sK1_ax3_V)),
inference(step,[status(thm)],[t149,t15]) ).
cnf(t114,plain,
op2(h(sK2_ax3_U),h(sK1_ax3_V)) = h(sFlat0),
inference(orient,[status(thm)],[t150]) ).
cnf(t115,plain,
op2(h(sK1_ax3_V),h(sK2_ax3_U)) = ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sFlat0),op2(h(sK1_ax3_V),h(sK2_ax3_U))),op2(h(sK1_ax3_V),h(sK2_ax3_U))),
inference(cp,[status(thm)],[t33,t114]) ).
cnf(t42,plain,
h(op1(sK1_ax3_V,sK2_ax3_U)) = ifeq2(sorti1(sK2_ax3_U),true,ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sFlat1)),h(op1(sK1_ax3_V,sK2_ax3_U))),
inference(cp,[status(thm)],[t34,t40]) ).
cnf(t141,plain,
h(sFlat1) = ifeq2(sorti1(sK2_ax3_U),true,ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sFlat1)),h(op1(sK1_ax3_V,sK2_ax3_U))),
inference(step,[status(thm)],[t42,t40]) ).
cnf(t142,plain,
h(sFlat1) = ifeq2(true,true,ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sFlat1)),h(op1(sK1_ax3_V,sK2_ax3_U))),
inference(step,[status(thm)],[t141,t21]) ).
cnf(t143,plain,
h(sFlat1) = ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sFlat1)),
inference(step,[status(thm)],[t142,t15]) ).
cnf(t144,plain,
h(sFlat1) = ifeq2(true,true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sFlat1)),
inference(step,[status(thm)],[t143,t19]) ).
cnf(t145,plain,
h(sFlat1) = op2(h(sK1_ax3_V),h(sK2_ax3_U)),
inference(step,[status(thm)],[t144,t15]) ).
cnf(t110,plain,
op2(h(sK1_ax3_V),h(sK2_ax3_U)) = h(sFlat1),
inference(orient,[status(thm)],[t145]) ).
cnf(t151,plain,
h(sFlat1) = ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sFlat0),op2(h(sK1_ax3_V),h(sK2_ax3_U))),op2(h(sK1_ax3_V),h(sK2_ax3_U))),
inference(step,[status(thm)],[t115,t110]) ).
cnf(t4,axiom,
ifeq(sorti1(X1),true,sorti2(h(X1)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
ifeq(sorti1(X1),true,sorti2(h(X1)),true) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t24,plain,
true = ifeq(true,true,sorti2(h(sK1_ax3_V)),true),
inference(cp,[status(thm)],[t23,t19]) ).
cnf(t135,plain,
true = sorti2(h(sK1_ax3_V)),
inference(step,[status(thm)],[t24,t18]) ).
cnf(t72,plain,
sorti2(h(sK1_ax3_V)) = true,
inference(orient,[status(thm)],[t135]) ).
cnf(t152,plain,
h(sFlat1) = ifeq2(true,true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sFlat0),op2(h(sK1_ax3_V),h(sK2_ax3_U))),op2(h(sK1_ax3_V),h(sK2_ax3_U))),
inference(step,[status(thm)],[t151,t72]) ).
cnf(t153,plain,
h(sFlat1) = ifeq2(sorti2(h(sK2_ax3_U)),true,h(sFlat0),op2(h(sK1_ax3_V),h(sK2_ax3_U))),
inference(step,[status(thm)],[t152,t15]) ).
cnf(t25,plain,
true = ifeq(true,true,sorti2(h(sK2_ax3_U)),true),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t136,plain,
true = sorti2(h(sK2_ax3_U)),
inference(step,[status(thm)],[t25,t18]) ).
cnf(t79,plain,
sorti2(h(sK2_ax3_U)) = true,
inference(orient,[status(thm)],[t136]) ).
cnf(t154,plain,
h(sFlat1) = ifeq2(true,true,h(sFlat0),op2(h(sK1_ax3_V),h(sK2_ax3_U))),
inference(step,[status(thm)],[t153,t79]) ).
cnf(t155,plain,
h(sFlat1) = h(sFlat0),
inference(step,[status(thm)],[t154,t15]) ).
cnf(t118,plain,
h(sFlat1) = h(sFlat0),
inference(orient,[status(thm)],[t155]) ).
cnf(goal_0,negated_conjecture,
op1(sK2_ax3_U,sK1_ax3_V) != op1(sK1_ax3_V,sK2_ax3_U),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
op1(sK2_ax3_U,sK1_ax3_V) != sFlat0,
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
op1(sK2_ax3_U,sK1_ax3_V) != j(h(sFlat0)),
inference(rw,[status(thm)],[g0_0,t98]) ).
cnf(g0_2,plain,
sFlat1 != j(h(sFlat0)),
inference(rw,[status(thm)],[g0_1,t40]) ).
cnf(g0_3,plain,
j(h(sFlat1)) != j(h(sFlat0)),
inference(rw,[status(thm)],[g0_2]) ).
cnf(g0_4,plain,
j(h(sFlat0)) != j(h(sFlat0)),
inference(rw,[status(thm)],[g0_3,t118]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG030-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 25 04:36:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.76/1.21 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.76/1.21 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------