%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT286+2 : 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 : n020.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 07:50:01 AM UTC 2026
% Result : Theorem 210.43s 31.11s
% Output : CNFRefutation 210.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 66 ( 29 unt; 0 def)
% Number of atoms : 147 ( 22 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 136 ( 55 ~; 49 |; 18 &)
% ( 1 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 48 ( 2 sgn 18 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rc1_xboole_0,axiom,
? [A] : v1_xboole_0(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(d5_xboole_0,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('theBenchmark.p',d5_xboole_0) ).
fof(t4_subset_1,axiom,
! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
file('theBenchmark.p',t4_subset_1) ).
fof(d5_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> k3_subset_1(A,B) = k4_xboole_0(A,B) ),
file('theBenchmark.p',d5_subset_1) ).
fof(dt_k3_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> m1_subset_1(k3_subset_1(A,B),k1_zfmisc_1(A)) ),
file('theBenchmark.p',dt_k3_subset_1) ).
fof(t1_subset,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(fc5_pre_topc,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A) )
=> v4_pre_topc(k2_pre_topc(A),A) ),
file('theBenchmark.p',fc5_pre_topc) ).
fof(d3_pre_topc,axiom,
! [A] :
( l1_struct_0(A)
=> k2_pre_topc(A) = u1_struct_0(A) ),
file('theBenchmark.p',d3_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(fc8_tops_1,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A) )
=> ( v4_pre_topc(k2_pre_topc(A),A)
& v3_pre_topc(k2_pre_topc(A),A) ) ),
file('theBenchmark.p',fc8_tops_1) ).
fof(t13_lopclset,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> u1_struct_0(k6_lopclset(A)) = k1_lopclset(A) ),
file('theBenchmark.p',t13_lopclset) ).
fof(t3_boole,axiom,
! [A] : k4_xboole_0(A,k1_xboole_0) = A,
file('theBenchmark.p',t3_boole) ).
fof(t4_lopclset,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)))
=> ( ( v4_pre_topc(B,A)
& v3_pre_topc(B,A) )
=> r2_hidden(B,k1_lopclset(A)) ) ) ),
file('theBenchmark.p',t4_lopclset) ).
fof(t15_lopclset,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
file('theBenchmark.p',t15_lopclset) ).
fof(t15_lopclset_neg,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
inference(assume_negation,[status(cth)],[t15_lopclset]) ).
cnf(c_1330,plain,
k4_xboole_0(A,k1_xboole_0) = A,
inference(clausify,[status(thm)],[t3_boole]) ).
cnf(c_3343,plain,
( r2_hidden(B,k1_lopclset(A))
| ~ v4_pre_topc(B,A)
| ~ v3_pre_topc(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(clausify,[status(thm)],[t4_lopclset]) ).
fof(nnf_6,plain,
? [A] : v1_xboole_0(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
v1_xboole_0(sK0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_6]) ).
cnf(c_3359,plain,
v1_xboole_0(sK0),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_3377,plain,
( k1_xboole_0 = A
| ~ v1_xboole_0(A) ),
inference(clausify,[status(thm)],[d5_xboole_0]) ).
cnf(c_3590,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)),
inference(clausify,[status(thm)],[t4_subset_1]) ).
cnf(c_3599,plain,
( k3_subset_1(B,A) = k4_xboole_0(B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[d5_subset_1]) ).
cnf(c_3600,plain,
( k4_xboole_0(B,A) = k3_subset_1(B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(copy,[status(thm)],[c_3599]) ).
cnf(c_3649,plain,
( m1_subset_1(k3_subset_1(B,A),k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[dt_k3_subset_1]) ).
cnf(c_3665,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_3814,plain,
( v4_pre_topc(k2_pre_topc(A),A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(clausify,[status(thm)],[fc5_pre_topc]) ).
cnf(c_3820,plain,
( k2_pre_topc(A) = u1_struct_0(A)
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[d3_pre_topc]) ).
cnf(c_3821,plain,
( u1_struct_0(A) = k2_pre_topc(A)
| ~ l1_struct_0(A) ),
inference(copy,[status(thm)],[c_3820]) ).
cnf(c_3869,plain,
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[dt_l1_pre_topc]) ).
cnf(c_3878,plain,
( v3_pre_topc(k2_pre_topc(A),A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A) ),
inference(clausify,[status(thm)],[fc8_tops_1]) ).
cnf(c_4061,plain,
( k1_lopclset(A) = u1_struct_0(k6_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t13_lopclset]) ).
cnf(c_4062,plain,
( u1_struct_0(k6_lopclset(A)) = k1_lopclset(A)
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_4061]) ).
fof(nnf_1305,plain,
? [A] :
( ~ m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A)))
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t15_lopclset_neg]) ).
fof(sk_t15_lopclset_neg,plain,
( ~ m1_subset_1(k2_pre_topc(sK1),u1_struct_0(k6_lopclset(sK1)))
& l1_pre_topc(sK1)
& v2_pre_topc(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(A,sK1)],[nnf_1305]) ).
cnf(c_4064,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t15_lopclset_neg]) ).
cnf(c_4065,negated_conjecture,
v2_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t15_lopclset_neg]) ).
cnf(c_4066,negated_conjecture,
l1_pre_topc(sK1),
inference(split_conjunct,[status(thm)],[sk_t15_lopclset_neg]) ).
cnf(c_4067,negated_conjecture,
~ m1_subset_1(k2_pre_topc(sK1),u1_struct_0(k6_lopclset(sK1))),
inference(split_conjunct,[status(thm)],[sk_t15_lopclset_neg]) ).
cnf(c_9159,plain,
k1_xboole_0 = sK0,
inference(resolve,[status(thm)],[c_3377,c_3359]) ).
cnf(c_9960,plain,
m1_subset_1(sK0,k1_zfmisc_1(A)),
inference(paramod,[status(thm)],[c_9159,c_3590]) ).
cnf(c_10116,plain,
k4_xboole_0(A,sK0) = A,
inference(paramod,[status(thm)],[c_9159,c_1330]) ).
cnf(c_40635,plain,
k4_xboole_0(A,sK0) = k3_subset_1(A,sK0),
inference(resolve,[status(thm)],[c_9960,c_3600]) ).
cnf(c_40636,plain,
A = k3_subset_1(A,sK0),
inference(paramod,[status(thm)],[c_10116,c_40635]) ).
cnf(c_20293,plain,
k3_subset_1(A,sK0) = A,
inference(copy,[status(thm)],[c_40636]) ).
cnf(c_40637,plain,
m1_subset_1(k3_subset_1(A,sK0),k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_3649,c_9960]) ).
cnf(c_20833,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(paramod,[status(thm)],[c_20293,c_40637]) ).
cnf(c_40638,negated_conjecture,
( v4_pre_topc(k2_pre_topc(sK1),sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_3814,c_4065]) ).
cnf(c_25698,negated_conjecture,
v4_pre_topc(k2_pre_topc(sK1),sK1),
inference(resolve,[status(thm)],[c_4066,c_40638]) ).
cnf(c_27968,plain,
l1_struct_0(sK1),
inference(resolve,[status(thm)],[c_3869,c_4066]) ).
cnf(c_27982,plain,
u1_struct_0(sK1) = k2_pre_topc(sK1),
inference(resolve,[status(thm)],[c_27968,c_3821]) ).
cnf(c_40639,negated_conjecture,
( v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_3878,c_4065]) ).
cnf(c_28109,negated_conjecture,
v3_pre_topc(k2_pre_topc(sK1),sK1),
inference(resolve,[status(thm)],[c_4066,c_40639]) ).
cnf(c_40640,plain,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ m1_subset_1(k2_pre_topc(sK1),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_25698,c_3343]) ).
cnf(c_40641,plain,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ m1_subset_1(k2_pre_topc(sK1),k1_zfmisc_1(k2_pre_topc(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_27982,c_40640]) ).
cnf(c_40642,negated_conjecture,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ m1_subset_1(k2_pre_topc(sK1),k1_zfmisc_1(k2_pre_topc(sK1)))
| ~ l1_pre_topc(sK1)
| ~ v2_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_4064,c_40641]) ).
cnf(c_40643,negated_conjecture,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ m1_subset_1(k2_pre_topc(sK1),k1_zfmisc_1(k2_pre_topc(sK1)))
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_4065,c_40642]) ).
cnf(c_40644,negated_conjecture,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1)
| ~ m1_subset_1(k2_pre_topc(sK1),k1_zfmisc_1(k2_pre_topc(sK1))) ),
inference(resolve,[status(thm)],[c_4066,c_40643]) ).
cnf(c_40645,negated_conjecture,
( r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1))
| ~ v3_pre_topc(k2_pre_topc(sK1),sK1) ),
inference(resolve,[status(thm)],[c_20833,c_40644]) ).
cnf(c_29853,negated_conjecture,
r2_hidden(k2_pre_topc(sK1),k1_lopclset(sK1)),
inference(resolve,[status(thm)],[c_28109,c_40645]) ).
cnf(c_40646,negated_conjecture,
( u1_struct_0(k6_lopclset(sK1)) = k1_lopclset(sK1)
| ~ l1_pre_topc(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_4062,c_4065]) ).
cnf(c_40647,negated_conjecture,
( u1_struct_0(k6_lopclset(sK1)) = k1_lopclset(sK1)
| ~ l1_pre_topc(sK1) ),
inference(resolve,[status(thm)],[c_4064,c_40646]) ).
cnf(c_32605,negated_conjecture,
u1_struct_0(k6_lopclset(sK1)) = k1_lopclset(sK1),
inference(resolve,[status(thm)],[c_4066,c_40647]) ).
cnf(c_32608,negated_conjecture,
~ m1_subset_1(k2_pre_topc(sK1),k1_lopclset(sK1)),
inference(paramod,[status(thm)],[c_32605,c_4067]) ).
cnf(c_40648,plain,
m1_subset_1(k2_pre_topc(sK1),k1_lopclset(sK1)),
inference(resolve,[status(thm)],[c_29853,c_3665]) ).
cnf(c_40634,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_32608,c_40648]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT286+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 20:27:19 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 3702648 was started by sandbox on n020,
% 0.13/0.36 % Fri Sep 25 20:27:19 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 210.43/31.11
% 210.43/31.11 % SInE (scan): 1032 to sos (tol 1.5x), 281 to usable (tol 2.0x), 5113 zapped, of 6426 axioms (depth 3).
% 210.43/31.11
% 210.43/31.11 % From the command line: assign(max_seconds, 300).
% 210.43/31.11
% 210.43/31.11 % given #500 (F,wt=22): 18157 f250(A) != k5_relat_1(c11,c1) | -r2_hidden(k4_tarski(B,C),f250(A)). [resolve(16122,a,2479,a),flip(a)].
% 210.43/31.11
% 210.43/31.11 % given #1000 (W,wt=14): 20300 r2_hidden(c1,k1_zfmisc_1(A)). [resolve(9960,a,3586,b),unit_del(a,3581)].
% 210.43/31.11
% 210.43/31.11 % given #1500 (F,wt=14): 30701 -r2_hidden(k1_numbers,f230(k5_numbers)). [resolve(27817,a,3350,b)].
% 210.43/31.11
% 210.43/31.11 % given #2000 (T,wt=15): 9812 k4_xboole_0(A,A) = c1. [back_rewrite(6095),rewrite([9159(2)])].
% 210.43/31.11
% 210.43/31.11 % given #2500 (F,wt=14): 36142 -r1_tarski(k1_numbers,f27(k5_ordinal2)). [resolve(36095,a,3715,a)].
% 210.43/31.11
% 210.43/31.11 % given #3000 (T,wt=14): 39519 v1_xcmplx_0(f2(k3_numbers,c1)). [resolve(25665,a,2349,b),unit_del(a,2196)].
% 210.43/31.11
% 210.43/31.11 % SZS status Theorem for theBenchmark
% 210.43/31.11
% 210.43/31.11 % Proof 1 at 25.90 (+ 3.52) seconds.
% 210.43/31.11 % Length of proof is 47.
% 210.43/31.11 % Level of proof is 7.
% 210.43/31.11 % Maximum clause weight is 121.000.
% 210.43/31.11 % Given clauses 3363.
% 210.43/31.11
% 210.43/31.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------