%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP028+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 09:52:59 AM UTC 2026
% Result : Theorem 0.12s 0.42s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 8
% Syntax : Number of formulae : 55 ( 14 unt; 0 def)
% Number of atoms : 205 ( 4 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 253 ( 103 ~; 105 |; 31 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 57 ( 0 sgn 25 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k1_pre_topc,axiom,
! [A] :
( l1_struct_0(A)
=> m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))) ),
file('theBenchmark.p',dt_k1_pre_topc) ).
fof(dt_l1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_pre_topc) ).
fof(fc1_pre_topc,axiom,
! [A] :
( l1_struct_0(A)
=> ( v5_membered(k1_pre_topc(A))
& v4_membered(k1_pre_topc(A))
& v3_membered(k1_pre_topc(A))
& v2_membered(k1_pre_topc(A))
& v1_membered(k1_pre_topc(A))
& v1_xboole_0(k1_pre_topc(A)) ) ),
file('theBenchmark.p',fc1_pre_topc) ).
fof(t11_tsp_1,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('theBenchmark.p',t11_tsp_1) ).
fof(t35_tex_2,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('theBenchmark.p',t35_tex_2) ).
fof(t6_boole,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('theBenchmark.p',t6_boole) ).
fof(t9_tsp_2,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('theBenchmark.p',t9_tsp_2) ).
fof(t10_tsp_2,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('theBenchmark.p',t10_tsp_2) ).
fof(t10_tsp_2_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(assume_negation,[status(cth)],[t10_tsp_2]) ).
fof(nnf_63,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(fof_nnf,[status(thm)],[t10_tsp_2_neg]) ).
fof(sk_t10_tsp_2_neg,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(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_63]) ).
cnf(c_64,negated_conjecture,
v2_pre_topc(sK0),
inference(split_conjunct,[status(thm)],[sk_t10_tsp_2_neg]) ).
fof(nnf_62,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(fof_nnf,[status(thm)],[t9_tsp_2]) ).
fof(sk_t9_tsp_2_sk,plain,
! [A] :
( ! [B] :
( ( v1_tsp_2(sK1(A,B),A)
& r1_tarski(B,sK1(A,B))
& m1_subset_1(sK1(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(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_62]) ).
fof(sk_t9_tsp_2,plain,
( ! [VAR_0,VAR_1] :
( v1_tsp_2(sK1(VAR_0,VAR_1),VAR_0)
| ~ v1_tsp_1(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( r1_tarski(VAR_1,sK1(VAR_0,VAR_1))
| ~ v1_tsp_1(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( m1_subset_1(sK1(VAR_0,VAR_1),k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ v1_tsp_1(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l1_pre_topc(VAR_0)
| ~ v2_pre_topc(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t9_tsp_2_sk]) ).
cnf(c_65,plain,
( v1_tsp_2(sK1(A,B),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(split_conjunct,[status(thm)],[sk_t9_tsp_2]) ).
cnf(c_67,plain,
( m1_subset_1(sK1(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(split_conjunct,[status(thm)],[sk_t9_tsp_2]) ).
cnf(c_68,plain,
( 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(clausify,[status(thm)],[t35_tex_2]) ).
cnf(c_122,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_123,plain,
( m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k1_pre_topc]) ).
cnf(c_125,plain,
( v1_xboole_0(k1_pre_topc(A))
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_pre_topc]) ).
cnf(c_139,negated_conjecture,
( v3_tex_2(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_64,c_68]) ).
cnf(c_140,plain,
( 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(clausify,[status(thm)],[t11_tsp_1]) ).
cnf(c_141,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_139,c_140]) ).
cnf(c_775,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_776,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_775]) ).
cnf(c_142,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_776]) ).
cnf(c_169,plain,
( ~ l1_pre_topc(A)
| v1_xboole_0(k1_pre_topc(A)) ),
inference(resolve,[status(thm)],[c_125,c_122]) ).
cnf(c_172,plain,
( m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_pre_topc(A) ),
inference(resolve,[status(thm)],[c_122,c_123]) ).
cnf(c_212,negated_conjecture,
( m1_subset_1(sK1(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_64,c_67]) ).
cnf(c_213,negated_conjecture,
( v1_tsp_2(sK1(sK0,A),sK0)
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_64,c_65]) ).
cnf(c_214,negated_conjecture,
( ~ v1_tsp_2(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(split_conjunct,[status(thm)],[sk_t10_tsp_2_neg]) ).
cnf(c_215,negated_conjecture,
l1_pre_topc(sK0),
inference(split_conjunct,[status(thm)],[sk_t10_tsp_2_neg]) ).
cnf(c_216,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t10_tsp_2_neg]) ).
cnf(c_219,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_777,negated_conjecture,
( v1_tsp_2(sK1(sK0,A),sK0)
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_216,c_213]) ).
cnf(c_281,negated_conjecture,
( v1_tsp_2(sK1(sK0,A),sK0)
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_215,c_777]) ).
cnf(c_778,negated_conjecture,
( m1_subset_1(sK1(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_216,c_212]) ).
cnf(c_282,negated_conjecture,
( m1_subset_1(sK1(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_215,c_778]) ).
cnf(c_779,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A)
| ~ l1_pre_topc(sK0) ),
inference(resolve,[status(thm)],[c_216,c_142]) ).
cnf(c_322,negated_conjecture,
( v1_tsp_1(A,sK0)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_215,c_779]) ).
cnf(c_327,plain,
m1_subset_1(k1_pre_topc(sK0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_215,c_172]) ).
cnf(c_328,plain,
v1_xboole_0(k1_pre_topc(sK0)),
inference(resolve,[status(thm)],[c_215,c_169]) ).
cnf(c_780,negated_conjecture,
( v1_tsp_1(k1_pre_topc(sK0),sK0)
| ~ v1_xboole_0(k1_pre_topc(sK0)) ),
inference(resolve,[status(thm)],[c_327,c_322]) ).
cnf(c_684,negated_conjecture,
v1_tsp_1(k1_pre_topc(sK0),sK0),
inference(resolve,[status(thm)],[c_328,c_780]) ).
cnf(c_781,negated_conjecture,
( m1_subset_1(sK1(sK0,k1_pre_topc(sK0)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_tsp_1(k1_pre_topc(sK0),sK0) ),
inference(resolve,[status(thm)],[c_327,c_282]) ).
cnf(c_687,negated_conjecture,
m1_subset_1(sK1(sK0,k1_pre_topc(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_684,c_781]) ).
cnf(c_782,negated_conjecture,
( v1_tsp_2(sK1(sK0,k1_pre_topc(sK0)),sK0)
| ~ v1_tsp_1(k1_pre_topc(sK0),sK0) ),
inference(resolve,[status(thm)],[c_327,c_281]) ).
cnf(c_688,negated_conjecture,
v1_tsp_2(sK1(sK0,k1_pre_topc(sK0)),sK0),
inference(resolve,[status(thm)],[c_684,c_782]) ).
cnf(c_783,plain,
k1_xboole_0 = k1_pre_topc(sK0),
inference(resolve,[status(thm)],[c_328,c_219]) ).
cnf(c_695,plain,
k1_pre_topc(sK0) = k1_xboole_0,
inference(copy,[status(thm)],[c_783]) ).
cnf(c_698,negated_conjecture,
v1_tsp_2(sK1(sK0,k1_xboole_0),sK0),
inference(paramod,[status(thm)],[c_695,c_688]) ).
cnf(c_699,negated_conjecture,
m1_subset_1(sK1(sK0,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_695,c_687]) ).
cnf(c_784,negated_conjecture,
~ m1_subset_1(sK1(sK0,k1_xboole_0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_698,c_214]) ).
cnf(c_774,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_699,c_784]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP028+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 20:35:14 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 1061436 was started by sandbox on n009,
% 0.09/0.35 % Sat Sep 26 20:35:14 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 0.12/0.42
% 0.12/0.42 % SZS status Theorem for theBenchmark
% 0.12/0.42
% 0.12/0.42 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.12/0.42 % Length of proof is 39.
% 0.12/0.42 % Level of proof is 9.
% 0.12/0.42 % Maximum clause weight is 34.000.
% 0.12/0.42 % Given clauses 206.
% 0.12/0.42
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------