%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU435+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:06 PM UTC 2026
% Result : Theorem 9.76s 1.94s
% Output : Proof 9.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 45 ( 22 unt; 0 def)
% Number of atoms : 80 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 79 ( 44 ~; 18 |; 11 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-6 aty)
% Number of variables : 90 ( 5 sgn 54 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B))))
=> ! [D,E,F] :
( m1_subset_1(F,k1_zfmisc_1(D))
=> m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_relset_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B))))
=> ! [D,E,F] :
( m1_subset_1(F,k1_zfmisc_1(D))
=> m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E))) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A,B,C] :
( ? [D,E,F] :
( ~ m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E)))
& m1_subset_1(F,k1_zfmisc_1(D)) )
& m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ~ m1_subset_1(a_6_0_relset_2(sk0,sk1,sk2,sk3,sk4,sk5),k1_zfmisc_1(k1_zfmisc_1(sk4)))
& m1_subset_1(sk5,k1_zfmisc_1(sk3))
& m1_subset_1(sk2,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sk0,sk1)))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5])],[f0_nnf]) ).
cnf(c2,plain,
~ m1_subset_1(a_6_0_relset_2(sk0,sk1,sk2,sk3,sk4,sk5),k1_zfmisc_1(k1_zfmisc_1(sk4))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t130,plain,
ifeq(m1_subset_1(a_6_0_relset_2(sk0,sk1,sk2,sk3,sk4,sk5),k1_zfmisc_1(k1_zfmisc_1(sk4))),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
fof(f41,axiom,
! [A,B,C,D,E,F] :
( ( m1_subset_1(F,k1_zfmisc_1(D))
& m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) )
=> m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s8_domain_1__e1_46__relset_2) ).
fof(f41_nnf,plain,
! [A,B,C,D,E,F] :
( m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E)))
| ~ m1_subset_1(F,k1_zfmisc_1(D))
| ~ m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [C,A,B,F,D,E] :
( m1_subset_1(a_6_0_relset_2(A,B,C,D,E,F),k1_zfmisc_1(k1_zfmisc_1(E)))
| ~ m1_subset_1(F,k1_zfmisc_1(D))
| ~ m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c60,plain,
( m1_subset_1(a_6_0_relset_2(X0,X1,X2,X3,X4,X5),k1_zfmisc_1(k1_zfmisc_1(X4)))
| ~ m1_subset_1(X5,k1_zfmisc_1(X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X0,X1)))) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(hi49,axiom,
ifeq(m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),true,ifeq(m1_subset_1(X3,k1_zfmisc_1(X4)),true,m1_subset_1(a_6_0_relset_2(X1,X2,X0,X4,X5,X3),k1_zfmisc_1(k1_zfmisc_1(X5))),true),true) = true,
inference(equality_encoding,[status(esa)],[c60]) ).
cnf(c0,plain,
m1_subset_1(sk2,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sk0,sk1)))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,negated_conjecture,
m1_subset_1(sk2,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sk0,sk1)))) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(c1,plain,
m1_subset_1(sk5,k1_zfmisc_1(sk3)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi1,negated_conjecture,
m1_subset_1(sk5,k1_zfmisc_1(sk3)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t96,plain,
m1_subset_1(a_6_0_relset_2(sk0,sk1,sk2,sk3,X1,sk5),k1_zfmisc_1(k1_zfmisc_1(X1))) = true,
inference(hyper_resolution,[status(thm)],[hi49,hi0,hi1]) ).
cnf(t245,plain,
m1_subset_1(a_6_0_relset_2(sk0,sk1,sk2,sk3,X1,sk5),k1_zfmisc_1(k1_zfmisc_1(X1))) = true,
inference(orient,[status(thm)],[t96]) ).
cnf(t1015,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t130,t245]) ).
cnf(t45,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t207,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t45]) ).
cnf(t1016,plain,
false = true,
inference(step,[status(thm)],[t1015,t207]) ).
cnf(t1012,plain,
false = true,
inference(orient,[status(thm)],[t1016]) ).
fof(f1,axiom,
! [A,B] :
( r2_hidden(A,B)
=> ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ r2_hidden(B,A)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c3,plain,
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f25,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f25_nnf,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c32,plain,
~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f33,axiom,
? [A] :
( v1_relat_1(A)
& ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f33_nnf,plain,
? [A] :
( v1_relat_1(A)
& ~ v1_xboole_0(A) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
( v1_relat_1(sk14)
& ~ v1_xboole_0(sk14) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f33_nnf]) ).
cnf(c48,plain,
~ v1_xboole_0(sk14),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
fof(f47,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f47_nnf,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c70,plain,
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
fof(f49,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f49_nnf,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c72,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c3,c32,c48,c70,c72]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1012]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU435+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 14:14:12 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.76/1.94 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.76/1.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------