%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU075+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 08:44:59 AM UTC 2026
% Result : Theorem 25.73s 4.91s
% Output : CNFRefutation 25.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 4
% Syntax : Number of formulae : 76 ( 23 unt; 0 def)
% Number of atoms : 353 ( 146 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 466 ( 189 ~; 202 |; 57 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 106 ( 0 sgn 52 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d5_funct_1,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( B = relation_rng(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( C = apply(A,D)
& in(D,relation_dom(A)) ) ) ) ),
file('theBenchmark.p',d5_funct_1) ).
fof(t23_funct_1,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( in(A,relation_dom(B))
=> apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ),
file('theBenchmark.p',t23_funct_1) ).
fof(t9_funct_1,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B] :
( ( function(B)
& relation(B) )
=> ( ( ! [C] :
( in(C,relation_dom(A))
=> apply(A,C) = apply(B,C) )
& relation_dom(A) = relation_dom(B) )
=> A = B ) ) ),
file('theBenchmark.p',t9_funct_1) ).
fof(t156_funct_1,conjecture,
! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ! [D] :
( ( function(D)
& relation(D) )
=> ( ( relation_composition(B,C) = relation_composition(B,D)
& relation_dom(D) = A
& relation_dom(C) = A
& A = relation_rng(B) )
=> C = D ) ) ) ),
file('theBenchmark.p',t156_funct_1) ).
fof(t156_funct_1_neg,negated_conjecture,
~ ! [A,B] :
( ( function(B)
& relation(B) )
=> ! [C] :
( ( function(C)
& relation(C) )
=> ! [D] :
( ( function(D)
& relation(D) )
=> ( ( relation_composition(B,C) = relation_composition(B,D)
& relation_dom(D) = A
& relation_dom(C) = A
& A = relation_rng(B) )
=> C = D ) ) ) ),
inference(assume_negation,[status(cth)],[t156_funct_1]) ).
fof(nnf_39,plain,
? [A,B] :
( ? [C] :
( ? [D] :
( D != C
& relation_composition(B,D) = relation_composition(B,C)
& relation_dom(D) = A
& relation_dom(C) = A
& relation_rng(B) = A
& function(D)
& relation(D) )
& function(C)
& relation(C) )
& function(B)
& relation(B) ),
inference(fof_nnf,[status(thm)],[t156_funct_1_neg]) ).
fof(sk_t156_funct_1_neg,plain,
( sK0 != sK1
& relation_composition(sK2,sK0) = relation_composition(sK2,sK1)
& relation_dom(sK0) = sK3
& relation_dom(sK1) = sK3
& relation_rng(sK2) = sK3
& function(sK0)
& relation(sK0)
& function(sK1)
& relation(sK1)
& function(sK2)
& relation(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK1,sK0,sK3]),skolemize(A,sK3),skolemize(B,sK2),skolemize(C,sK1),skolemize(D,sK0)],[nnf_39]) ).
cnf(c_44,negated_conjecture,
sK0 != sK1,
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_45,negated_conjecture,
relation_composition(sK2,sK0) = relation_composition(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_46,negated_conjecture,
relation_dom(sK0) = sK3,
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_47,negated_conjecture,
relation_dom(sK1) = sK3,
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_48,negated_conjecture,
relation_rng(sK2) = sK3,
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_49,negated_conjecture,
function(sK0),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_50,negated_conjecture,
relation(sK0),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_51,negated_conjecture,
function(sK1),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_52,negated_conjecture,
relation(sK1),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_53,negated_conjecture,
function(sK2),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
cnf(c_54,negated_conjecture,
relation(sK2),
inference(split_conjunct,[status(thm)],[sk_t156_funct_1_neg]) ).
fof(nnf_38,plain,
! [A] :
( ! [B] :
( B = A
| ? [C] :
( apply(B,C) != apply(A,C)
& in(C,relation_dom(A)) )
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[t9_funct_1]) ).
fof(sk_t9_funct_1_sk,plain,
! [A] :
( ! [B] :
( B = A
| ( apply(B,sK4(A,B)) != apply(A,sK4(A,B))
& in(sK4(A,B),relation_dom(A)) )
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(C,sK4(A,B))],[nnf_38]) ).
fof(sk_t9_funct_1,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| apply(VAR_1,sK4(VAR_0,VAR_1)) != apply(VAR_0,sK4(VAR_0,VAR_1))
| relation_dom(VAR_1) != relation_dom(VAR_0)
| ~ function(VAR_1)
| ~ relation(VAR_1)
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| in(sK4(VAR_0,VAR_1),relation_dom(VAR_0))
| relation_dom(VAR_1) != relation_dom(VAR_0)
| ~ function(VAR_1)
| ~ relation(VAR_1)
| ~ function(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t9_funct_1_sk]) ).
cnf(c_55,plain,
( B = A
| apply(B,sK4(A,B)) != apply(A,sK4(A,B))
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_t9_funct_1]) ).
cnf(c_56,plain,
( B = A
| in(sK4(A,B),relation_dom(A))
| relation_dom(B) != relation_dom(A)
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_t9_funct_1]) ).
cnf(c_63,plain,
( apply(relation_composition(A,B),C) = apply(B,apply(A,C))
| ~ in(C,relation_dom(A))
| ~ function(B)
| ~ relation(B)
| ~ function(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[t23_funct_1]) ).
fof(nnf_5,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ( ! [D] :
( apply(A,D) != C
| ~ in(D,relation_dom(A)) )
| ~ in(C,B) )
& ( ? [X3] :
( apply(A,X3) = C
& in(X3,relation_dom(A)) )
| in(C,B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] :
( apply(A,X2) != X0
| ~ in(X2,relation_dom(A)) )
| in(X0,B) )
& ( ? [X1] :
( apply(A,X1) = X0
& in(X1,relation_dom(A)) )
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ function(A)
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d5_funct_1]) ).
fof(sk_d5_funct_1_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ! [D] :
( apply(A,D) != sK6(A,B)
| ~ in(D,relation_dom(A)) )
| ~ in(sK6(A,B),B) )
& ( ( apply(A,sK7(A,B)) = sK6(A,B)
& in(sK7(A,B),relation_dom(A)) )
| in(sK6(A,B),B) ) )
| relation_rng(A) = B )
& ( ! [X0] :
( ( ! [X2] :
( apply(A,X2) != X0
| ~ in(X2,relation_dom(A)) )
| in(X0,B) )
& ( ( apply(A,sK5(A,B,X0)) = X0
& in(sK5(A,B,X0),relation_dom(A)) )
| ~ in(X0,B) ) )
| relation_rng(A) != B ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7]),skolemize(X1,sK5(A,B,X0)),skolemize(C,sK6(A,B)),skolemize(X3,sK7(A,B))],[nnf_5]) ).
fof(sk_d5_funct_1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( apply(VAR_0,VAR_2) != sK6(VAR_0,VAR_1)
| ~ in(VAR_2,relation_dom(VAR_0))
| ~ in(sK6(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( apply(VAR_0,sK7(VAR_0,VAR_1)) = sK6(VAR_0,VAR_1)
| in(sK6(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK7(VAR_0,VAR_1),relation_dom(VAR_0))
| in(sK6(VAR_0,VAR_1),VAR_1)
| relation_rng(VAR_0) = VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( apply(VAR_0,VAR_3) != VAR_2
| ~ in(VAR_3,relation_dom(VAR_0))
| in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( apply(VAR_0,sK5(VAR_0,VAR_1,VAR_2)) = VAR_2
| ~ in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK5(VAR_0,VAR_1,VAR_2),relation_dom(VAR_0))
| ~ in(VAR_2,VAR_1)
| relation_rng(VAR_0) != VAR_1
| ~ function(VAR_0)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d5_funct_1_sk]) ).
cnf(c_105,plain,
( apply(A,sK5(A,B,C)) = C
| ~ in(C,B)
| relation_rng(A) != B
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_funct_1]) ).
cnf(c_106,plain,
( in(sK5(A,B,C),relation_dom(A))
| ~ in(C,B)
| relation_rng(A) != B
| ~ function(A)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_funct_1]) ).
cnf(c_12251,negated_conjecture,
( A = sK1
| apply(A,sK4(sK1,A)) != apply(sK1,sK4(sK1,A))
| relation_dom(A) != relation_dom(sK1)
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_55,c_51]) ).
cnf(c_12252,negated_conjecture,
( A = sK1
| apply(A,sK4(sK1,A)) != apply(sK1,sK4(sK1,A))
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(paramod,[status(thm)],[c_47,c_12251]) ).
cnf(c_12253,negated_conjecture,
( A = sK1
| apply(sK1,sK4(sK1,A)) != apply(A,sK4(sK1,A))
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(copy,[status(thm)],[c_12252]) ).
cnf(c_12254,negated_conjecture,
( sK1 = A
| apply(sK1,sK4(sK1,A)) != apply(A,sK4(sK1,A))
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(copy,[status(thm)],[c_12253]) ).
cnf(c_117,negated_conjecture,
( sK1 = A
| apply(sK1,sK4(sK1,A)) != apply(A,sK4(sK1,A))
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_52,c_12254]) ).
cnf(c_12255,negated_conjecture,
( A = sK1
| in(sK4(sK1,A),relation_dom(sK1))
| relation_dom(A) != relation_dom(sK1)
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(resolve,[status(thm)],[c_56,c_51]) ).
cnf(c_12256,negated_conjecture,
( A = sK1
| in(sK4(sK1,A),relation_dom(sK1))
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(paramod,[status(thm)],[c_47,c_12255]) ).
cnf(c_12257,negated_conjecture,
( A = sK1
| in(sK4(sK1,A),sK3)
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(paramod,[status(thm)],[c_47,c_12256]) ).
cnf(c_12258,negated_conjecture,
( sK1 = A
| in(sK4(sK1,A),sK3)
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A)
| ~ relation(sK1) ),
inference(copy,[status(thm)],[c_12257]) ).
cnf(c_123,negated_conjecture,
( sK1 = A
| in(sK4(sK1,A),sK3)
| relation_dom(A) != sK3
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_52,c_12258]) ).
cnf(c_12259,negated_conjecture,
( sK1 = sK0
| apply(sK1,sK4(sK1,sK0)) != apply(sK0,sK4(sK1,sK0))
| relation_dom(sK0) != sK3
| ~ relation(sK0) ),
inference(resolve,[status(thm)],[c_117,c_49]) ).
cnf(c_12260,negated_conjecture,
( sK1 = sK0
| apply(sK1,sK4(sK1,sK0)) != apply(sK0,sK4(sK1,sK0))
| sK3 != sK3
| ~ relation(sK0) ),
inference(paramod,[status(thm)],[c_46,c_12259]) ).
cnf(c_12261,negated_conjecture,
( sK1 = sK0
| apply(sK0,sK4(sK1,sK0)) != apply(sK1,sK4(sK1,sK0))
| sK3 != sK3
| ~ relation(sK0) ),
inference(copy,[status(thm)],[c_12260]) ).
cnf(c_12262,negated_conjecture,
( sK0 = sK1
| apply(sK0,sK4(sK1,sK0)) != apply(sK1,sK4(sK1,sK0))
| sK3 != sK3
| ~ relation(sK0) ),
inference(copy,[status(thm)],[c_12261]) ).
cnf(c_12263,negated_conjecture,
( sK0 = sK1
| apply(sK0,sK4(sK1,sK0)) != apply(sK1,sK4(sK1,sK0))
| ~ relation(sK0) ),
inference(copy,[status(thm)],[c_12262]) ).
cnf(c_12264,negated_conjecture,
( sK0 = sK1
| apply(sK0,sK4(sK1,sK0)) != apply(sK1,sK4(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_50,c_12263]) ).
cnf(c_351,negated_conjecture,
apply(sK0,sK4(sK1,sK0)) != apply(sK1,sK4(sK1,sK0)),
inference(resolve,[status(thm)],[c_44,c_12264]) ).
cnf(c_12265,negated_conjecture,
( sK1 = sK0
| in(sK4(sK1,sK0),sK3)
| relation_dom(sK0) != sK3
| ~ relation(sK0) ),
inference(resolve,[status(thm)],[c_123,c_49]) ).
cnf(c_12266,negated_conjecture,
( sK1 = sK0
| in(sK4(sK1,sK0),sK3)
| sK3 != sK3
| ~ relation(sK0) ),
inference(paramod,[status(thm)],[c_46,c_12265]) ).
cnf(c_12267,negated_conjecture,
( sK0 = sK1
| in(sK4(sK1,sK0),sK3)
| sK3 != sK3
| ~ relation(sK0) ),
inference(copy,[status(thm)],[c_12266]) ).
cnf(c_12268,negated_conjecture,
( sK0 = sK1
| in(sK4(sK1,sK0),sK3)
| ~ relation(sK0) ),
inference(copy,[status(thm)],[c_12267]) ).
cnf(c_12269,negated_conjecture,
( sK0 = sK1
| in(sK4(sK1,sK0),sK3) ),
inference(resolve,[status(thm)],[c_50,c_12268]) ).
cnf(c_890,negated_conjecture,
in(sK4(sK1,sK0),sK3),
inference(resolve,[status(thm)],[c_44,c_12269]) ).
cnf(c_12270,negated_conjecture,
( in(sK5(sK2,A,B),relation_dom(sK2))
| ~ in(B,A)
| relation_rng(sK2) != A
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_106,c_54]) ).
cnf(c_12271,negated_conjecture,
( in(sK5(sK2,A,B),relation_dom(sK2))
| ~ in(B,A)
| relation_rng(sK2) != A ),
inference(resolve,[status(thm)],[c_12270,c_53]) ).
cnf(c_12272,negated_conjecture,
( in(sK5(sK2,sK3,A),relation_dom(sK2))
| ~ in(A,sK3) ),
inference(resolve,[status(thm)],[c_12271,c_48]) ).
cnf(c_5636,negated_conjecture,
in(sK5(sK2,sK3,sK4(sK1,sK0)),relation_dom(sK2)),
inference(resolve,[status(thm)],[c_12272,c_890]) ).
cnf(c_12273,negated_conjecture,
( apply(sK2,sK5(sK2,A,B)) = B
| ~ in(B,A)
| relation_rng(sK2) != A
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_105,c_54]) ).
cnf(c_12274,negated_conjecture,
( apply(sK2,sK5(sK2,A,B)) = B
| ~ in(B,A)
| relation_rng(sK2) != A ),
inference(resolve,[status(thm)],[c_12273,c_53]) ).
cnf(c_12275,negated_conjecture,
( apply(sK2,sK5(sK2,sK3,A)) = A
| ~ in(A,sK3) ),
inference(resolve,[status(thm)],[c_12274,c_48]) ).
cnf(c_5637,negated_conjecture,
apply(sK2,sK5(sK2,sK3,sK4(sK1,sK0))) = sK4(sK1,sK0),
inference(resolve,[status(thm)],[c_12275,c_890]) ).
cnf(c_12276,negated_conjecture,
( apply(relation_composition(sK2,A),B) = apply(A,apply(sK2,B))
| ~ in(B,relation_dom(sK2))
| ~ function(A)
| ~ relation(A)
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_63,c_54]) ).
cnf(c_12277,negated_conjecture,
( apply(relation_composition(sK2,A),B) = apply(A,apply(sK2,B))
| ~ in(B,relation_dom(sK2))
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_12276,c_53]) ).
cnf(c_12278,negated_conjecture,
( apply(relation_composition(sK2,sK1),A) = apply(sK1,apply(sK2,A))
| ~ in(A,relation_dom(sK2))
| ~ function(sK1) ),
inference(resolve,[status(thm)],[c_12277,c_52]) ).
cnf(c_12279,negated_conjecture,
( apply(relation_composition(sK2,sK1),A) = apply(sK1,apply(sK2,A))
| ~ in(A,relation_dom(sK2)) ),
inference(resolve,[status(thm)],[c_12278,c_51]) ).
cnf(c_12280,negated_conjecture,
apply(relation_composition(sK2,sK1),sK5(sK2,sK3,sK4(sK1,sK0))) = apply(sK1,apply(sK2,sK5(sK2,sK3,sK4(sK1,sK0)))),
inference(resolve,[status(thm)],[c_12279,c_5636]) ).
cnf(c_12249,negated_conjecture,
apply(relation_composition(sK2,sK1),sK5(sK2,sK3,sK4(sK1,sK0))) = apply(sK1,sK4(sK1,sK0)),
inference(paramod,[status(thm)],[c_5637,c_12280]) ).
cnf(c_12281,negated_conjecture,
( apply(relation_composition(sK2,A),B) = apply(A,apply(sK2,B))
| ~ in(B,relation_dom(sK2))
| ~ function(A)
| ~ relation(A)
| ~ function(sK2) ),
inference(resolve,[status(thm)],[c_63,c_54]) ).
cnf(c_12282,negated_conjecture,
( apply(relation_composition(sK2,A),B) = apply(A,apply(sK2,B))
| ~ in(B,relation_dom(sK2))
| ~ function(A)
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_12281,c_53]) ).
cnf(c_12283,negated_conjecture,
( apply(relation_composition(sK2,sK0),A) = apply(sK0,apply(sK2,A))
| ~ in(A,relation_dom(sK2))
| ~ function(sK0) ),
inference(resolve,[status(thm)],[c_12282,c_50]) ).
cnf(c_12284,negated_conjecture,
( apply(relation_composition(sK2,sK0),A) = apply(sK0,apply(sK2,A))
| ~ in(A,relation_dom(sK2)) ),
inference(resolve,[status(thm)],[c_12283,c_49]) ).
cnf(c_12285,negated_conjecture,
apply(relation_composition(sK2,sK0),sK5(sK2,sK3,sK4(sK1,sK0))) = apply(sK0,apply(sK2,sK5(sK2,sK3,sK4(sK1,sK0)))),
inference(resolve,[status(thm)],[c_12284,c_5636]) ).
cnf(c_12286,negated_conjecture,
apply(relation_composition(sK2,sK1),sK5(sK2,sK3,sK4(sK1,sK0))) = apply(sK0,apply(sK2,sK5(sK2,sK3,sK4(sK1,sK0)))),
inference(paramod,[status(thm)],[c_45,c_12285]) ).
cnf(c_12287,negated_conjecture,
apply(sK1,sK4(sK1,sK0)) = apply(sK0,apply(sK2,sK5(sK2,sK3,sK4(sK1,sK0)))),
inference(paramod,[status(thm)],[c_12249,c_12286]) ).
cnf(c_12288,negated_conjecture,
apply(sK1,sK4(sK1,sK0)) = apply(sK0,sK4(sK1,sK0)),
inference(paramod,[status(thm)],[c_5637,c_12287]) ).
cnf(c_12289,negated_conjecture,
apply(sK0,sK4(sK1,sK0)) = apply(sK1,sK4(sK1,sK0)),
inference(copy,[status(thm)],[c_12288]) ).
cnf(c_12250,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_351,c_12289]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU075+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n018.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Sat Sep 26 08:36:51 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.57 % Process 22692 was started by sandbox2 on n018,
% 0.09/0.57 % Sat Sep 26 08:36:51 2026
% 0.09/0.57 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.58
% 0.09/0.58 % From the command line: assign(max_seconds, 300).
% 25.73/4.91
% 25.73/4.91 % given #500 (F,wt=19): 7928 -empty(f5(relation_rng(c12))). [ur(77,a,7906,a)].
% 25.73/4.91
% 25.73/4.91 % SZS status Theorem for theBenchmark
% 25.73/4.91
% 25.73/4.91 % Proof 1 at 3.49 (+ 0.80) seconds.
% 25.73/4.91 % Length of proof is 28.
% 25.73/4.91 % Level of proof is 6.
% 25.73/4.91 % Maximum clause weight is 43.000.
% 25.73/4.91 % Given clauses 637.
% 25.73/4.91
% 25.73/4.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------