%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU444+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:52:08 PM UTC 2026
% Result : Theorem 3.91s 3.10s
% Output : Proof 3.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of formulae : 45 ( 14 unt; 0 def)
% Number of atoms : 87 ( 45 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 78 ( 36 ~; 26 |; 9 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-4 aty)
% Number of variables : 78 ( 0 sgn 54 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m2_relset_1(k6_relset_1(A,B,C),B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f42_nnf,plain,
! [A,B,C] :
( m2_relset_1(k6_relset_1(A,B,C),B,A)
| ~ m1_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [C,A,B] :
( m2_relset_1(k6_relset_1(A,B,C),B,A)
| ~ m1_relset_1(C,A,B) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c54,plain,
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f38,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f38_nnf,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [C,A,B] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c49,plain,
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f0,conjecture,
! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_relset_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B,C] :
( ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) != k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
| k1_funct_5(C) != k10_relset_1(A,B,k6_relset_1(B,A,C),A) )
& m2_relset_1(C,B,A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ( k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k10_relset_1(sk1,sk0,sk2,sk1)) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),sk0) )
& m2_relset_1(sk2,sk1,sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c0,plain,
m2_relset_1(sk2,sk1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p140,plain,
m1_relset_1(sk2,sk1,sk0),
inference(resolution,[status(thm)],[c49,c0]) ).
cnf(p161,plain,
m2_relset_1(k4_relat_1(sk2),sk0,sk1),
inference(resolution,[status(thm)],[c54,p140]) ).
cnf(p163,plain,
m1_relset_1(k4_relat_1(sk2),sk0,sk1),
inference(resolution,[status(thm)],[p161,c49]) ).
fof(f36,axiom,
! [A,B,C,D] :
( m1_relset_1(C,A,B)
=> k10_relset_1(A,B,C,D) = k9_relat_1(C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f36_nnf,plain,
! [A,B,C,D] :
( k10_relset_1(A,B,C,D) = k9_relat_1(C,D)
| ~ m1_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [C,A,B,D] :
( k10_relset_1(A,B,C,D) = k9_relat_1(C,D)
| ~ m1_relset_1(C,A,B) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c47,plain,
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p165,plain,
k10_relset_1(sk0,sk1,k4_relat_1(sk2),X0) = k9_relat_1(k4_relat_1(sk2),X0),
inference(resolution,[status(thm)],[p163,c47]) ).
fof(f44,axiom,
! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_relset_2) ).
fof(f44_nnf,plain,
! [A,B,C] :
( ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) )
| ~ m2_relset_1(C,B,A) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [C,B,A] :
( ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) )
| ~ m2_relset_1(C,B,A) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c56,plain,
( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p194,plain,
k1_funct_5(sk2) = k10_relset_1(sk0,sk1,k4_relat_1(sk2),sk0),
inference(resolution,[status(thm)],[c56,c0]) ).
cnf(p230,plain,
k1_funct_5(sk2) = k9_relat_1(k4_relat_1(sk2),sk0),
inference(superposition,[status(thm)],[p165,p194]) ).
cnf(p232,plain,
k9_relat_1(k4_relat_1(sk2),sk0) = k1_funct_5(sk2),
inference(superposition,[status(thm)],[p230,p165]) ).
cnf(c57,plain,
( k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p201,plain,
k2_funct_5(sk2) = k9_relat_1(sk2,sk1),
inference(resolution,[status(thm)],[c57,c0]) ).
cnf(p143,plain,
k10_relset_1(sk1,sk0,sk2,X0) = k9_relat_1(sk2,X0),
inference(resolution,[status(thm)],[p140,c47]) ).
cnf(p206,plain,
k9_relat_1(sk2,sk1) = k2_funct_5(sk2),
inference(superposition,[status(thm)],[p201,p143]) ).
fof(f37,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k6_relset_1(A,B,C) = k4_relat_1(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f37_nnf,plain,
! [A,B,C] :
( k6_relset_1(A,B,C) = k4_relat_1(C)
| ~ m1_relset_1(C,A,B) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [C,A,B] :
( k6_relset_1(A,B,C) = k4_relat_1(C)
| ~ m1_relset_1(C,A,B) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c48,plain,
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p145,plain,
k6_relset_1(sk1,sk0,sk2) = k4_relat_1(sk2),
inference(resolution,[status(thm)],[p140,c48]) ).
cnf(c1,plain,
( k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k10_relset_1(sk1,sk0,sk2,sk1)) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),sk0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p144,plain,
( k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k9_relat_1(sk2,sk1)) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k10_relset_1(sk0,sk1,k6_relset_1(sk1,sk0,sk2),sk0) ),
inference(demodulation,[status(thm)],[p143,c1]) ).
cnf(p147,plain,
( k10_relset_1(sk0,sk1,k4_relat_1(sk2),k9_relat_1(sk2,sk1)) != k10_relset_1(sk0,sk1,k4_relat_1(sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k10_relset_1(sk0,sk1,k4_relat_1(sk2),sk0) ),
inference(demodulation,[status(thm)],[p145,p144]) ).
cnf(p166,plain,
( k9_relat_1(k4_relat_1(sk2),k9_relat_1(sk2,sk1)) != k9_relat_1(k4_relat_1(sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k9_relat_1(k4_relat_1(sk2),sk0) ),
inference(demodulation,[status(thm)],[p165,p147]) ).
cnf(p207,plain,
( k9_relat_1(k4_relat_1(sk2),k2_funct_5(sk2)) != k9_relat_1(k4_relat_1(sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k9_relat_1(k4_relat_1(sk2),sk0) ),
inference(demodulation,[status(thm)],[p206,p166]) ).
cnf(p233,plain,
( k9_relat_1(k4_relat_1(sk2),k2_funct_5(sk2)) != k9_relat_1(k4_relat_1(sk2),k2_funct_5(sk2))
| k1_funct_5(sk2) != k1_funct_5(sk2) ),
inference(demodulation,[status(thm)],[p232,p207]) ).
cnf(p276,plain,
k1_funct_5(sk2) != k1_funct_5(sk2),
inference(equality_resolution,[status(thm)],[p233]) ).
cnf(p277,plain,
$false,
inference(equality_resolution,[status(thm)],[p276]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU444+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.39 % Computer : n016.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Thu Sep 24 14:22:42 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.91/3.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.91/3.10 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------