%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG069-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 : Sun Sep 27 06:49:24 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.38s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 58 ( 58 unt; 0 def)
% Number of atoms : 58 ( 57 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-4 aty)
% Number of variables : 44 ( 2 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c_2,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_001]) ).
fof(ax3_1,axiom,
! [VAR_0] : ifeq(sorti1(VAR_0),true,sorti1(sK2_ax3_V(VAR_0)),true) = true,
file('theBenchmark.p',ax3_1) ).
cnf(c_5,plain,
ifeq(sorti1(A),true,sorti1(sK2_ax3_V(A)),true) = true,
inference(clausify,[status(thm)],[ax3_1]) ).
fof(ax3,axiom,
! [VAR_0] : ifeq2(sorti1(VAR_0),true,op1(sK2_ax3_V(VAR_0),sK2_ax3_V(VAR_0)),VAR_0) = VAR_0,
file('theBenchmark.p',ax3) ).
cnf(c_6,plain,
ifeq2(sorti1(A),true,op1(sK2_ax3_V(A),sK2_ax3_V(A)),A) = A,
inference(clausify,[status(thm)],[ax3]) ).
fof(ax4_1,axiom,
! [VAR_0] : tuple(op2(VAR_0,VAR_0),sorti2(VAR_0)) != tuple(sK1_ax4_U,true),
file('theBenchmark.p',ax4_1) ).
cnf(c_7,plain,
tuple(op2(A,A),sorti2(A)) != tuple(sK1_ax4_U,true),
inference(clausify,[status(thm)],[ax4_1]) ).
fof(ax4,axiom,
sorti2(sK1_ax4_U) = true,
file('theBenchmark.p',ax4) ).
cnf(c_8,plain,
sorti2(sK1_ax4_U) = true,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_9,plain,
true = sorti2(sK1_ax4_U),
inference(copy,[status(thm)],[c_8]) ).
fof(co1,axiom,
! [VAR_0] : ifeq(sorti1(VAR_0),true,sorti2(h(VAR_0)),true) = true,
file('theBenchmark.p',co1) ).
cnf(c_10,plain,
ifeq(sorti1(A),true,sorti2(h(A)),true) = true,
inference(clausify,[status(thm)],[co1]) ).
cnf(c_78,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti2(h(A)),true) = true,
inference(paramod,[status(thm)],[c_9,c_10]) ).
cnf(c_79,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti2(h(A)),sorti2(sK1_ax4_U)) = true,
inference(paramod,[status(thm)],[c_9,c_78]) ).
cnf(c_11,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti2(h(A)),sorti2(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_9,c_79]) ).
fof(co1_1,axiom,
! [VAR_0,VAR_1] : ifeq2(sorti1(VAR_0),true,ifeq2(sorti1(VAR_1),true,op2(h(VAR_1),h(VAR_0)),h(op1(VAR_1,VAR_0))),h(op1(VAR_1,VAR_0))) = h(op1(VAR_1,VAR_0)),
file('theBenchmark.p',co1_1) ).
cnf(c_12,plain,
ifeq2(sorti1(A),true,ifeq2(sorti1(B),true,op2(h(B),h(A)),h(op1(B,A))),h(op1(B,A))) = h(op1(B,A)),
inference(clausify,[status(thm)],[co1_1]) ).
cnf(c_80,plain,
ifeq2(sorti1(A),sorti2(sK1_ax4_U),ifeq2(sorti1(B),true,op2(h(B),h(A)),h(op1(B,A))),h(op1(B,A))) = h(op1(B,A)),
inference(paramod,[status(thm)],[c_9,c_12]) ).
cnf(c_13,plain,
ifeq2(sorti1(A),sorti2(sK1_ax4_U),ifeq2(sorti1(B),sorti2(sK1_ax4_U),op2(h(B),h(A)),h(op1(B,A))),h(op1(B,A))) = h(op1(B,A)),
inference(paramod,[status(thm)],[c_9,c_80]) ).
fof(co1_3,axiom,
! [VAR_0] : ifeq(sorti2(VAR_0),true,sorti1(j(VAR_0)),true) = true,
file('theBenchmark.p',co1_3) ).
cnf(c_16,plain,
ifeq(sorti2(A),true,sorti1(j(A)),true) = true,
inference(clausify,[status(thm)],[co1_3]) ).
cnf(c_81,plain,
ifeq(sorti2(A),sorti2(sK1_ax4_U),sorti1(j(A)),true) = true,
inference(paramod,[status(thm)],[c_9,c_16]) ).
cnf(c_82,plain,
ifeq(sorti2(A),sorti2(sK1_ax4_U),sorti1(j(A)),sorti2(sK1_ax4_U)) = true,
inference(paramod,[status(thm)],[c_9,c_81]) ).
cnf(c_17,plain,
ifeq(sorti2(A),sorti2(sK1_ax4_U),sorti1(j(A)),sorti2(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_9,c_82]) ).
fof(co1_5,axiom,
! [VAR_0] : ifeq2(sorti2(VAR_0),true,h(j(VAR_0)),VAR_0) = VAR_0,
file('theBenchmark.p',co1_5) ).
cnf(c_20,plain,
ifeq2(sorti2(A),true,h(j(A)),A) = A,
inference(clausify,[status(thm)],[co1_5]) ).
cnf(c_21,plain,
ifeq2(sorti2(A),sorti2(sK1_ax4_U),h(j(A)),A) = A,
inference(paramod,[status(thm)],[c_9,c_20]) ).
cnf(c_22,plain,
tuple(op2(A,A),sorti2(A)) != tuple(sK1_ax4_U,sorti2(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_9,c_7]) ).
cnf(c_23,plain,
ifeq2(sorti1(A),sorti2(sK1_ax4_U),op1(sK2_ax3_V(A),sK2_ax3_V(A)),A) = A,
inference(paramod,[status(thm)],[c_9,c_6]) ).
cnf(c_83,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti1(sK2_ax3_V(A)),true) = true,
inference(paramod,[status(thm)],[c_9,c_5]) ).
cnf(c_84,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti1(sK2_ax3_V(A)),sorti2(sK1_ax4_U)) = true,
inference(paramod,[status(thm)],[c_9,c_83]) ).
cnf(c_24,plain,
ifeq(sorti1(A),sorti2(sK1_ax4_U),sorti1(sK2_ax3_V(A)),sorti2(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_9,c_84]) ).
cnf(c_85,plain,
sorti2(sK1_ax4_U) = sorti1(j(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_27,plain,
sorti1(j(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_86,plain,
sK1_ax4_U = h(j(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_21,c_1]) ).
cnf(c_30,plain,
h(j(sK1_ax4_U)) = sK1_ax4_U,
inference(copy,[status(thm)],[c_86]) ).
cnf(c_87,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))),j(sK1_ax4_U)) = j(sK1_ax4_U),
inference(paramod,[status(thm)],[c_27,c_23]) ).
cnf(c_35,plain,
op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))) = j(sK1_ax4_U),
inference(paramod,[status(thm)],[c_1,c_87]) ).
cnf(c_88,plain,
ifeq(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),sorti1(sK2_ax3_V(j(sK1_ax4_U))),sorti2(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_27,c_24]) ).
cnf(c_36,plain,
sorti1(sK2_ax3_V(j(sK1_ax4_U))) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_2,c_88]) ).
cnf(c_89,plain,
ifeq(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),sorti2(h(sK2_ax3_V(j(sK1_ax4_U)))),sorti2(sK1_ax4_U)) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_36,c_11]) ).
cnf(c_39,plain,
sorti2(h(sK2_ax3_V(j(sK1_ax4_U)))) = sorti2(sK1_ax4_U),
inference(paramod,[status(thm)],[c_2,c_89]) ).
cnf(c_49,plain,
tuple(op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),sorti2(sK1_ax4_U)) != tuple(sK1_ax4_U,sorti2(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_39,c_22]) ).
cnf(c_90,plain,
ifeq2(sorti1(sK2_ax3_V(j(sK1_ax4_U))),sorti2(sK1_ax4_U),ifeq2(sorti1(sK2_ax3_V(j(sK1_ax4_U))),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),h(j(sK1_ax4_U))),h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_35,c_13]) ).
cnf(c_91,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),ifeq2(sorti1(sK2_ax3_V(j(sK1_ax4_U))),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),h(j(sK1_ax4_U))),h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_36,c_90]) ).
cnf(c_92,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),h(j(sK1_ax4_U))),h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_36,c_91]) ).
cnf(c_93,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),sK1_ax4_U),h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_30,c_92]) ).
cnf(c_94,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U))))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_1,c_93]) ).
cnf(c_95,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),h(j(sK1_ax4_U))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_35,c_94]) ).
cnf(c_96,plain,
ifeq2(sorti2(sK1_ax4_U),sorti2(sK1_ax4_U),op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))),sK1_ax4_U) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_30,c_95]) ).
cnf(c_97,plain,
op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))) = h(op1(sK2_ax3_V(j(sK1_ax4_U)),sK2_ax3_V(j(sK1_ax4_U)))),
inference(paramod,[status(thm)],[c_1,c_96]) ).
cnf(c_98,plain,
op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))) = h(j(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_35,c_97]) ).
cnf(c_76,plain,
op2(h(sK2_ax3_V(j(sK1_ax4_U))),h(sK2_ax3_V(j(sK1_ax4_U)))) = sK1_ax4_U,
inference(paramod,[status(thm)],[c_30,c_98]) ).
cnf(c_99,plain,
tuple(sK1_ax4_U,sorti2(sK1_ax4_U)) != tuple(sK1_ax4_U,sorti2(sK1_ax4_U)),
inference(paramod,[status(thm)],[c_76,c_49]) ).
cnf(c_77,plain,
$false,
inference(copy,[status(thm)],[c_99]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG069-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 21:10:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1722744 was started by sandbox2 on n016,
% 0.08/0.36 % Sat Sep 26 21:10:18 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 0.14/0.38
% 0.14/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.38
% 0.14/0.38 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.14/0.38 % Length of proof is 26.
% 0.14/0.38 % Level of proof is 7.
% 0.14/0.38 % Maximum clause weight is 28.000.
% 0.14/0.38 % Given clauses 25.
% 0.14/0.38
% 0.14/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------