%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG072+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 : Theorem 30.96s 5.54s
% Output : CNFRefutation 30.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 7
% Syntax : Number of formulae : 83 ( 45 unt; 0 def)
% Number of atoms : 203 ( 103 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 198 ( 78 ~; 63 |; 33 &)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 67 ( 0 sgn 36 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2,axiom,
( ? [V] :
( unit1 = V
& sorti1(V) )
& ! [U] :
( sorti1(U)
=> ( op1(U,unit1) = U
& op1(unit1,U) = U ) ) ),
file('theBenchmark.p',ax2) ).
fof(ax4,axiom,
( ? [V] :
( unit2 = V
& sorti2(V) )
& ! [U] :
( sorti2(U)
=> ( op2(U,unit2) = U
& op2(unit2,U) = U ) ) ),
file('theBenchmark.p',ax4) ).
fof(ax7,axiom,
? [U] :
( ! [V] :
( sorti1(V)
=> ! [W] :
( sorti1(W)
=> ( ( U != unit1
& op1(V,U) = W )
| op1(V,W) != U ) ) )
& sorti1(U) ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
~ ? [U] :
( ! [V] :
( sorti2(V)
=> ! [W] :
( sorti2(W)
=> ( ( U != unit2
& op2(V,U) = W )
| op2(V,W) != U ) ) )
& sorti2(U) ),
file('theBenchmark.p',ax8) ).
fof(co1,conjecture,
( ( ! [V] :
( sorti2(V)
=> sorti1(j(V)) )
& ! [U] :
( sorti1(U)
=> sorti2(h(U)) ) )
=> ~ ( ! [X2] :
( sorti1(X2)
=> j(h(X2)) = X2 )
& ! [X1] :
( sorti2(X1)
=> h(j(X1)) = X1 )
& ! [Y] :
( sorti2(Y)
=> ! [Z] :
( sorti2(Z)
=> j(op2(Y,Z)) = op1(j(Y),j(Z)) ) )
& ! [W] :
( sorti1(W)
=> ! [X] :
( sorti1(X)
=> h(op1(W,X)) = op2(h(W),h(X)) ) ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ! [V] :
( sorti2(V)
=> sorti1(j(V)) )
& ! [U] :
( sorti1(U)
=> sorti2(h(U)) ) )
=> ~ ( ! [X2] :
( sorti1(X2)
=> j(h(X2)) = X2 )
& ! [X1] :
( sorti2(X1)
=> h(j(X1)) = X1 )
& ! [Y] :
( sorti2(Y)
=> ! [Z] :
( sorti2(Z)
=> j(op2(Y,Z)) = op1(j(Y),j(Z)) ) )
& ! [W] :
( sorti1(W)
=> ! [X] :
( sorti1(X)
=> h(op1(W,X)) = op2(h(W),h(X)) ) ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
fof(ax1,axiom,
sorti1(unit1),
file('theBenchmark.p',ax1) ).
cnf(c_8,plain,
sorti1(unit1),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_9,plain,
( op1(unit1,A) = A
| ~ sorti1(A) ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_10,plain,
( op1(A,unit1) = A
| ~ sorti1(A) ),
inference(clausify,[status(thm)],[ax2]) ).
fof(ax3,axiom,
sorti2(unit2),
file('theBenchmark.p',ax3) ).
cnf(c_13,plain,
sorti2(unit2),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_14,plain,
( op2(unit2,A) = A
| ~ sorti2(A) ),
inference(clausify,[status(thm)],[ax4]) ).
fof(nnf_5,plain,
? [U] :
( ! [V] :
( ! [W] :
( ( U != unit1
& op1(V,U) = W )
| op1(V,W) != U
| ~ sorti1(W) )
| ~ sorti1(V) )
& sorti1(U) ),
inference(fof_nnf,[status(thm)],[ax7]) ).
fof(sk_ax7_sk,plain,
( ! [V] :
( ! [W] :
( ( sK0 != unit1
& op1(V,sK0) = W )
| op1(V,W) != sK0
| ~ sorti1(W) )
| ~ sorti1(V) )
& sorti1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(U,sK0)],[nnf_5]) ).
fof(sk_ax7,plain,
( ! [VAR_0,VAR_1] :
( sK0 != unit1
| op1(VAR_0,VAR_1) != sK0
| ~ sorti1(VAR_1)
| ~ sorti1(VAR_0) )
& ! [VAR_0,VAR_1] :
( op1(VAR_0,sK0) = VAR_1
| op1(VAR_0,VAR_1) != sK0
| ~ sorti1(VAR_1)
| ~ sorti1(VAR_0) )
& sorti1(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_ax7_sk]) ).
cnf(c_21,plain,
sorti1(sK0),
inference(split_conjunct,[status(thm)],[sk_ax7]) ).
cnf(c_22,plain,
( op1(A,sK0) = B
| op1(A,B) != sK0
| ~ sorti1(B)
| ~ sorti1(A) ),
inference(split_conjunct,[status(thm)],[sk_ax7]) ).
cnf(c_23,plain,
( sK0 != unit1
| op1(A,B) != sK0
| ~ sorti1(B)
| ~ sorti1(A) ),
inference(split_conjunct,[status(thm)],[sk_ax7]) ).
fof(nnf_6,plain,
! [U] :
( ? [V] :
( ? [W] :
( ( unit2 = U
| op2(V,U) != W )
& op2(V,W) = U
& sorti2(W) )
& sorti2(V) )
| ~ sorti2(U) ),
inference(fof_nnf,[status(thm)],[ax8]) ).
fof(sk_ax8_sk,plain,
! [U] :
( ( ( unit2 = U
| op2(sK1(U),U) != sK2(U) )
& op2(sK1(U),sK2(U)) = U
& sorti2(sK2(U))
& sorti2(sK1(U)) )
| ~ sorti2(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(V,sK1(U)),skolemize(W,sK2(U))],[nnf_6]) ).
fof(sk_ax8,plain,
( ! [VAR_0] :
( unit2 = VAR_0
| op2(sK1(VAR_0),VAR_0) != sK2(VAR_0)
| ~ sorti2(VAR_0) )
& ! [VAR_0] :
( op2(sK1(VAR_0),sK2(VAR_0)) = VAR_0
| ~ sorti2(VAR_0) )
& ! [VAR_0] :
( sorti2(sK2(VAR_0))
| ~ sorti2(VAR_0) )
& ! [VAR_0] :
( sorti2(sK1(VAR_0))
| ~ sorti2(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_ax8_sk]) ).
cnf(c_24,plain,
( sorti2(sK1(A))
| ~ sorti2(A) ),
inference(split_conjunct,[status(thm)],[sk_ax8]) ).
cnf(c_25,plain,
( sorti2(sK2(A))
| ~ sorti2(A) ),
inference(split_conjunct,[status(thm)],[sk_ax8]) ).
cnf(c_26,plain,
( op2(sK1(A),sK2(A)) = A
| ~ sorti2(A) ),
inference(split_conjunct,[status(thm)],[sk_ax8]) ).
cnf(c_27,plain,
( unit2 = A
| op2(sK1(A),A) != sK2(A)
| ~ sorti2(A) ),
inference(split_conjunct,[status(thm)],[sk_ax8]) ).
cnf(c_28,plain,
( unit2 = A
| sK2(A) != op2(sK1(A),A)
| ~ sorti2(A) ),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_29,negated_conjecture,
( sorti2(h(A))
| ~ sorti1(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_30,negated_conjecture,
( sorti1(j(A))
| ~ sorti2(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_31,negated_conjecture,
( h(op1(A,B)) = op2(h(A),h(B))
| ~ sorti1(B)
| ~ sorti1(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_32,negated_conjecture,
( j(op2(A,B)) = op1(j(A),j(B))
| ~ sorti2(B)
| ~ sorti2(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_33,negated_conjecture,
( h(j(A)) = A
| ~ sorti2(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_34,negated_conjecture,
( j(h(A)) = A
| ~ sorti1(A) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_35,plain,
op1(unit1,unit1) = unit1,
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_45,negated_conjecture,
sorti2(h(sK0)),
inference(resolve,[status(thm)],[c_29,c_21]) ).
cnf(c_46,negated_conjecture,
sorti2(h(unit1)),
inference(resolve,[status(thm)],[c_29,c_8]) ).
cnf(c_47,negated_conjecture,
sorti1(j(unit2)),
inference(resolve,[status(thm)],[c_30,c_13]) ).
cnf(c_54,negated_conjecture,
j(h(sK0)) = sK0,
inference(resolve,[status(thm)],[c_34,c_21]) ).
cnf(c_55,negated_conjecture,
j(h(unit1)) = unit1,
inference(resolve,[status(thm)],[c_34,c_8]) ).
cnf(c_21055,plain,
( sK0 != unit1
| unit1 != sK0
| ~ sorti1(unit1)
| ~ sorti1(unit1) ),
inference(paramod,[status(thm)],[c_35,c_23]) ).
cnf(c_21056,plain,
( sK0 != unit1
| sK0 != unit1
| ~ sorti1(unit1)
| ~ sorti1(unit1) ),
inference(copy,[status(thm)],[c_21055]) ).
cnf(c_21057,plain,
( sK0 != unit1
| sK0 != unit1
| ~ sorti1(unit1) ),
inference(copy,[status(thm)],[c_21056]) ).
cnf(c_21058,plain,
( sK0 != unit1
| ~ sorti1(unit1) ),
inference(copy,[status(thm)],[c_21057]) ).
cnf(c_56,plain,
sK0 != unit1,
inference(resolve,[status(thm)],[c_8,c_21058]) ).
cnf(c_97,plain,
op2(sK1(h(sK0)),sK2(h(sK0))) = h(sK0),
inference(resolve,[status(thm)],[c_26,c_45]) ).
cnf(c_98,plain,
sorti2(sK2(h(sK0))),
inference(resolve,[status(thm)],[c_25,c_45]) ).
cnf(c_99,plain,
sorti2(sK1(h(sK0))),
inference(resolve,[status(thm)],[c_24,c_45]) ).
cnf(c_21059,negated_conjecture,
( j(op2(unit2,A)) = op1(j(unit2),j(A))
| ~ sorti2(A) ),
inference(resolve,[status(thm)],[c_32,c_13]) ).
cnf(c_21060,negated_conjecture,
j(op2(unit2,h(unit1))) = op1(j(unit2),j(h(unit1))),
inference(resolve,[status(thm)],[c_21059,c_46]) ).
cnf(c_113,negated_conjecture,
j(op2(unit2,h(unit1))) = op1(j(unit2),unit1),
inference(paramod,[status(thm)],[c_55,c_21060]) ).
cnf(c_127,plain,
op2(unit2,h(unit1)) = h(unit1),
inference(resolve,[status(thm)],[c_14,c_46]) ).
cnf(c_21061,negated_conjecture,
j(h(unit1)) = op1(j(unit2),unit1),
inference(paramod,[status(thm)],[c_127,c_113]) ).
cnf(c_21062,negated_conjecture,
unit1 = op1(j(unit2),unit1),
inference(paramod,[status(thm)],[c_55,c_21061]) ).
cnf(c_129,negated_conjecture,
op1(j(unit2),unit1) = unit1,
inference(copy,[status(thm)],[c_21062]) ).
cnf(c_21063,plain,
op1(j(unit2),unit1) = j(unit2),
inference(resolve,[status(thm)],[c_10,c_47]) ).
cnf(c_21064,plain,
unit1 = j(unit2),
inference(paramod,[status(thm)],[c_129,c_21063]) ).
cnf(c_130,plain,
j(unit2) = unit1,
inference(copy,[status(thm)],[c_21064]) ).
cnf(c_227,negated_conjecture,
h(j(sK2(h(sK0)))) = sK2(h(sK0)),
inference(resolve,[status(thm)],[c_33,c_98]) ).
cnf(c_241,negated_conjecture,
sorti1(j(sK2(h(sK0)))),
inference(resolve,[status(thm)],[c_30,c_98]) ).
cnf(c_262,negated_conjecture,
h(j(sK1(h(sK0)))) = sK1(h(sK0)),
inference(resolve,[status(thm)],[c_33,c_99]) ).
cnf(c_21065,negated_conjecture,
( j(op2(sK1(h(sK0)),A)) = op1(j(sK1(h(sK0))),j(A))
| ~ sorti2(A) ),
inference(resolve,[status(thm)],[c_32,c_99]) ).
cnf(c_21066,negated_conjecture,
j(op2(sK1(h(sK0)),sK2(h(sK0)))) = op1(j(sK1(h(sK0))),j(sK2(h(sK0)))),
inference(resolve,[status(thm)],[c_21065,c_98]) ).
cnf(c_21067,negated_conjecture,
j(h(sK0)) = op1(j(sK1(h(sK0))),j(sK2(h(sK0)))),
inference(paramod,[status(thm)],[c_97,c_21066]) ).
cnf(c_21068,negated_conjecture,
sK0 = op1(j(sK1(h(sK0))),j(sK2(h(sK0)))),
inference(paramod,[status(thm)],[c_54,c_21067]) ).
cnf(c_271,negated_conjecture,
op1(j(sK1(h(sK0))),j(sK2(h(sK0)))) = sK0,
inference(copy,[status(thm)],[c_21068]) ).
cnf(c_278,negated_conjecture,
sorti1(j(sK1(h(sK0)))),
inference(resolve,[status(thm)],[c_30,c_99]) ).
cnf(c_21069,negated_conjecture,
( h(op1(j(sK1(h(sK0))),A)) = op2(h(j(sK1(h(sK0)))),h(A))
| ~ sorti1(A) ),
inference(resolve,[status(thm)],[c_31,c_278]) ).
cnf(c_21070,negated_conjecture,
h(op1(j(sK1(h(sK0))),sK0)) = op2(h(j(sK1(h(sK0)))),h(sK0)),
inference(resolve,[status(thm)],[c_21069,c_21]) ).
cnf(c_835,negated_conjecture,
h(op1(j(sK1(h(sK0))),sK0)) = op2(sK1(h(sK0)),h(sK0)),
inference(paramod,[status(thm)],[c_262,c_21070]) ).
cnf(c_21071,plain,
( op1(j(sK1(h(sK0))),sK0) = A
| op1(j(sK1(h(sK0))),A) != sK0
| ~ sorti1(A) ),
inference(resolve,[status(thm)],[c_22,c_278]) ).
cnf(c_21072,plain,
( op1(j(sK1(h(sK0))),sK0) = j(sK2(h(sK0)))
| op1(j(sK1(h(sK0))),j(sK2(h(sK0)))) != sK0 ),
inference(resolve,[status(thm)],[c_21071,c_241]) ).
cnf(c_21073,plain,
op1(j(sK1(h(sK0))),sK0) = j(sK2(h(sK0))),
inference(resolve,[status(thm)],[c_21072,c_271]) ).
cnf(c_15728,plain,
j(sK2(h(sK0))) = op1(j(sK1(h(sK0))),sK0),
inference(copy,[status(thm)],[c_21073]) ).
cnf(c_21074,negated_conjecture,
h(op1(j(sK1(h(sK0))),sK0)) = sK2(h(sK0)),
inference(paramod,[status(thm)],[c_15728,c_227]) ).
cnf(c_21075,negated_conjecture,
op2(sK1(h(sK0)),h(sK0)) = sK2(h(sK0)),
inference(paramod,[status(thm)],[c_835,c_21074]) ).
cnf(c_15730,negated_conjecture,
sK2(h(sK0)) = op2(sK1(h(sK0)),h(sK0)),
inference(copy,[status(thm)],[c_21075]) ).
cnf(c_21076,plain,
( unit2 = h(sK0)
| sK2(h(sK0)) != op2(sK1(h(sK0)),h(sK0)) ),
inference(resolve,[status(thm)],[c_28,c_45]) ).
cnf(c_21077,plain,
unit2 = h(sK0),
inference(resolve,[status(thm)],[c_21076,c_15730]) ).
cnf(c_20961,plain,
h(sK0) = unit2,
inference(copy,[status(thm)],[c_21077]) ).
cnf(c_21078,negated_conjecture,
j(unit2) = sK0,
inference(paramod,[status(thm)],[c_20961,c_54]) ).
cnf(c_21079,negated_conjecture,
unit1 = sK0,
inference(paramod,[status(thm)],[c_130,c_21078]) ).
cnf(c_21080,negated_conjecture,
sK0 = unit1,
inference(copy,[status(thm)],[c_21079]) ).
cnf(c_21054,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_56,c_21080]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG072+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/1.05 % Computer : n010.cluster.edu
% 0.17/1.05 % Model : x86_64 x86_64
% 0.17/1.05 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/1.05 % Memory : 8046.5625MB
% 0.17/1.05 % OS : Linux 6.8.0-71-generic
% 0.17/1.05 % CPULimit : 300
% 0.17/1.05 % WCLimit : 300
% 0.17/1.05 % DateTime : Sat Sep 26 21:06:17 UTC 2026
% 0.17/1.06 % CPUTime :
% 0.17/1.06 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/1.06 % Process 25757 was started by sandbox2 on n010,
% 0.17/1.06 % Sat Sep 26 21:06:17 2026
% 0.17/1.06 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/1.06
% 0.17/1.06 % From the command line: assign(max_seconds, 300).
% 30.96/5.54
% 30.96/5.54 % SZS status Theorem for theBenchmark
% 30.96/5.54
% 30.96/5.54 % Proof 1 at 3.15 (+ 1.25) seconds.
% 30.96/5.54 % Length of proof is 48.
% 30.96/5.54 % Level of proof is 8.
% 30.96/5.54 % Maximum clause weight is 26.000.
% 30.96/5.54 % Given clauses 386.
% 30.96/5.54
% 30.96/5.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------