%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP028+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 03:54:42 PM UTC 2026
% Result : Theorem 30.48s 4.46s
% Output : Proof 30.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 58 ( 10 unt; 0 def)
% Number of atoms : 208 ( 5 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 229 ( 79 ~; 97 |; 42 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 56 ( 3 sgn 29 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f62,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( ! [C] :
( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
=> ~ ( v1_tsp_2(C,A)
& r1_tarski(B,C) ) )
& v1_tsp_1(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_tsp_2) ).
fof(f62_nnf,plain,
! [A] :
( ! [B] :
( ? [C] :
( v1_tsp_2(C,A)
& r1_tarski(B,C)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )
| ~ v1_tsp_1(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [A,B] :
( ( v1_tsp_2(sk16(A,B),A)
& r1_tarski(B,sk16(A,B))
& m1_subset_1(sk16(A,B),k1_zfmisc_1(u1_struct_0(A))) )
| ~ v1_tsp_1(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16])],[f62_nnf]) ).
cnf(c159,plain,
( m1_subset_1(sk16(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( v1_tsp_2(B,A)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_tsp_2) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( v1_tsp_2(B,A)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ! [B] :
( ~ v1_tsp_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [B] :
( ( ~ v1_tsp_2(B,sk0)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sk0))) )
& l1_pre_topc(sk0)
& v2_pre_topc(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c1,plain,
v2_pre_topc(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1035,plain,
( m1_subset_1(sk16(sk0,X0),k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c159,c1]) ).
cnf(c2,plain,
l1_pre_topc(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1476,plain,
( m1_subset_1(sk16(sk0,X0),k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1035,c2]) ).
fof(f59,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f59_nnf,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c156,plain,
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f42,axiom,
! [A] :
? [B] :
( v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(f42_nnf,plain,
! [A] :
? [B] :
( v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [A] :
( v1_xboole_0(sk7(A))
& m1_subset_1(sk7(A),k1_zfmisc_1(A)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f42_nnf]) ).
cnf(c111,plain,
v1_xboole_0(sk7(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p809,plain,
sk7(X0) = k1_xboole_0,
inference(resolution,[status(thm)],[c156,c111]) ).
cnf(c110,plain,
m1_subset_1(sk7(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p810,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(demodulation,[status(thm)],[p809,c110]) ).
cnf(p1486,plain,
( m1_subset_1(sk16(sk0,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_tsp_1(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1476,p810]) ).
fof(f52,axiom,
! [A] :
( ( l1_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v3_tex_2(B,A)
=> v1_tsp_1(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_tsp_1) ).
fof(f52_nnf,plain,
! [A] :
( ! [B] :
( v1_tsp_1(B,A)
| ~ v3_tex_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_pre_topc(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [A,B] :
( v1_tsp_1(B,A)
| ~ v3_tex_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c148,plain,
( v1_tsp_1(X1,X0)
| ~ v3_tex_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p744,plain,
( v1_tsp_1(X0,sk0)
| ~ v3_tex_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c148,c2]) ).
cnf(p1193,plain,
( v1_tsp_1(k1_xboole_0,sk0)
| ~ v3_tex_2(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p810,p744]) ).
fof(f55,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& v1_xboole_0(B) )
=> v3_tex_2(B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_tex_2) ).
fof(f55_nnf,plain,
! [A] :
( ! [B] :
( v3_tex_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_xboole_0(B) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [A,B] :
( v3_tex_2(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ v1_xboole_0(B)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c151,plain,
( v3_tex_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_xboole_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(p772,plain,
( v3_tex_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_xboole_0(X0)
| ~ l1_pre_topc(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c151,c1]) ).
cnf(p1170,plain,
( v3_tex_2(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ v1_xboole_0(X0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p772,c2]) ).
fof(f37,axiom,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_membered) ).
fof(f37_nnf,plain,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c86,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p1171,plain,
( v3_tex_2(k1_xboole_0,sk0)
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1170,c86]) ).
cnf(p1195,plain,
( v3_tex_2(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p810,p1171]) ).
cnf(p1196,plain,
( v3_struct_0(sk0)
| v1_tsp_1(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1193,p1195]) ).
cnf(p1197,plain,
( v1_tsp_1(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1196]) ).
cnf(p1487,plain,
( v3_struct_0(sk0)
| m1_subset_1(sk16(sk0,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1486,p1197]) ).
cnf(p1488,plain,
( m1_subset_1(sk16(sk0,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1487]) ).
cnf(c3,plain,
( ~ v1_tsp_2(X1,sk0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sk0))) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1489,plain,
( ~ v1_tsp_2(sk16(sk0,k1_xboole_0),sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1488,c3]) ).
cnf(c161,plain,
( v1_tsp_2(sk16(X0,X1),X0)
| ~ v1_tsp_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p1037,plain,
( v1_tsp_2(sk16(sk0,X0),sk0)
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| ~ l1_pre_topc(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[c161,c1]) ).
cnf(p1343,plain,
( v1_tsp_2(sk16(sk0,X0),sk0)
| ~ v1_tsp_1(X0,sk0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sk0)))
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1037,c2]) ).
cnf(p1353,plain,
( v1_tsp_2(sk16(sk0,k1_xboole_0),sk0)
| ~ v1_tsp_1(k1_xboole_0,sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1343,p810]) ).
cnf(p1354,plain,
( v3_struct_0(sk0)
| v1_tsp_2(sk16(sk0,k1_xboole_0),sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1353,p1197]) ).
cnf(p1355,plain,
( v1_tsp_2(sk16(sk0,k1_xboole_0),sk0)
| v3_struct_0(sk0) ),
inference(factoring,[status(thm)],[p1354]) ).
cnf(p1509,plain,
( v3_struct_0(sk0)
| v3_struct_0(sk0) ),
inference(resolution,[status(thm)],[p1489,p1355]) ).
cnf(p1510,plain,
v3_struct_0(sk0),
inference(factoring,[status(thm)],[p1509]) ).
cnf(c0,plain,
~ v3_struct_0(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1511,plain,
$false,
inference(resolution,[status(thm)],[p1510,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP028+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.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 04:11:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 30.48/4.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.48/4.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------