%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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:06 AM UTC 2026
% Result : Theorem 0.15s 0.85s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 15
% Syntax : Number of formulae : 86 ( 24 unt; 0 def)
% Number of atoms : 253 ( 13 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 270 ( 103 ~; 101 |; 44 &)
% ( 3 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 1 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 19 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_k5_lattices,axiom,
! [A] :
( ( l1_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k5_lattices) ).
fof(dt_k6_lattices,axiom,
! [A] :
( ( l2_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k6_lattices) ).
fof(dt_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(redefinition_k6_domain_1,axiom,
! [A,B] :
( ( m1_subset_1(B,A)
& ~ v1_xboole_0(A) )
=> k6_domain_1(A,B) = k1_tarski(B) ),
file('theBenchmark.p',redefinition_k6_domain_1) ).
fof(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
fof(t13_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A) ) ),
file('theBenchmark.p',t13_filter_0) ).
fof(t21_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) ) ),
file('theBenchmark.p',t21_filter_2) ).
fof(t63_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t63_lattice2) ).
fof(t78_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ),
file('theBenchmark.p',t78_lattice2) ).
fof(t26_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ),
file('theBenchmark.p',t26_filter_2) ).
fof(t26_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ),
inference(assume_negation,[status(cth)],[t26_filter_2]) ).
cnf(c_95,plain,
( v14_lattices(k1_lattice2(A))
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_lattice2]) ).
cnf(c_97,plain,
( k6_lattices(k1_lattice2(A)) = k5_lattices(A)
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t78_lattice2]) ).
fof(nnf_91,plain,
? [A] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A)
& v13_lattices(A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t26_filter_2_neg]) ).
fof(sk_t26_filter_2_neg,plain,
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),sK0)
& v13_lattices(sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_91]) ).
cnf(c_98,negated_conjecture,
v13_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t26_filter_2_neg]) ).
cnf(c_176,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_178,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_184,plain,
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
cnf(c_185,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t13_filter_0]) ).
cnf(c_214,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l2_lattices(A) ),
inference(resolve,[status(thm)],[c_178,c_176]) ).
cnf(c_241,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_242,plain,
( m1_subset_1(k5_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_lattices]) ).
cnf(c_244,plain,
( m1_subset_1(k6_lattices(A),u1_struct_0(A))
| ~ l2_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k6_lattices]) ).
cnf(c_245,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_246,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_260,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_267,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_297,plain,
( k1_tarski(B) = k6_domain_1(A,B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_k6_domain_1]) ).
cnf(c_298,plain,
( k6_domain_1(A,B) = k1_tarski(B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_297]) ).
cnf(c_301,plain,
( ~ m1_filter_2(B,k1_lattice2(A))
| m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t21_filter_2]) ).
cnf(c_308,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t26_filter_2_neg]) ).
cnf(c_309,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t26_filter_2_neg]) ).
cnf(c_310,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t26_filter_2_neg]) ).
cnf(c_311,negated_conjecture,
~ m2_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),sK0),
inference(split_conjunct,[status(thm)],[sk_t26_filter_2_neg]) ).
cnf(c_318,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_98,c_97]) ).
cnf(c_1491,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_308,c_318]) ).
cnf(c_1492,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_309,c_1491]) ).
cnf(c_319,negated_conjecture,
k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0),
inference(resolve,[status(thm)],[c_310,c_1492]) ).
cnf(c_320,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_98,c_95]) ).
cnf(c_1493,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_308,c_320]) ).
cnf(c_1494,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_309,c_1493]) ).
cnf(c_321,negated_conjecture,
v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_310,c_1494]) ).
cnf(c_348,plain,
( m1_filter_2(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_185,c_184]) ).
cnf(c_1495,plain,
( m1_filter_2(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_348]) ).
cnf(c_1496,plain,
( m1_filter_2(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_1495]) ).
cnf(c_349,plain,
( m1_filter_2(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_1496]) ).
cnf(c_1497,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_309,c_267]) ).
cnf(c_1498,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_308,c_1497]) ).
cnf(c_475,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_310,c_1498]) ).
cnf(c_1499,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_310,c_260]) ).
cnf(c_480,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_308,c_1499]) ).
cnf(c_481,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_310,c_246]) ).
cnf(c_482,plain,
l1_lattices(sK0),
inference(resolve,[status(thm)],[c_310,c_245]) ).
cnf(c_483,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_310,c_241]) ).
cnf(c_1500,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k6_lattices(k1_lattice2(sK0))),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_349,c_321]) ).
cnf(c_1501,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_319,c_1500]) ).
cnf(c_1502,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_480,c_1501]) ).
cnf(c_1503,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_475,c_1502]) ).
cnf(c_491,negated_conjecture,
m1_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_483,c_1503]) ).
cnf(c_1504,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_481,c_214]) ).
cnf(c_605,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_308,c_1504]) ).
cnf(c_1505,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_482,c_242]) ).
cnf(c_612,negated_conjecture,
m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_308,c_1505]) ).
cnf(c_668,plain,
l2_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_483,c_246]) ).
cnf(c_1506,plain,
( m1_subset_1(k6_lattices(k1_lattice2(sK0)),u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_668,c_244]) ).
cnf(c_1507,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_319,c_1506]) ).
cnf(c_748,plain,
m1_subset_1(k5_lattices(sK0),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_480,c_1507]) ).
cnf(c_1508,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_668,c_214]) ).
cnf(c_749,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_480,c_1508]) ).
cnf(c_1509,plain,
( k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_612,c_298]) ).
cnf(c_950,plain,
k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0)),
inference(resolve,[status(thm)],[c_605,c_1509]) ).
cnf(c_952,negated_conjecture,
~ m2_filter_2(k1_tarski(k5_lattices(sK0)),sK0),
inference(paramod,[status(thm)],[c_950,c_311]) ).
cnf(c_1510,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_748,c_298]) ).
cnf(c_1364,plain,
k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0)),
inference(resolve,[status(thm)],[c_749,c_1510]) ).
cnf(c_1366,negated_conjecture,
m1_filter_2(k1_tarski(k5_lattices(sK0)),k1_lattice2(sK0)),
inference(paramod,[status(thm)],[c_1364,c_491]) ).
cnf(c_1511,plain,
( m2_filter_2(k1_tarski(k5_lattices(sK0)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1366,c_301]) ).
cnf(c_1512,negated_conjecture,
( m2_filter_2(k1_tarski(k5_lattices(sK0)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_308,c_1511]) ).
cnf(c_1513,negated_conjecture,
( m2_filter_2(k1_tarski(k5_lattices(sK0)),sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_309,c_1512]) ).
cnf(c_1514,negated_conjecture,
m2_filter_2(k1_tarski(k5_lattices(sK0)),sK0),
inference(resolve,[status(thm)],[c_310,c_1513]) ).
cnf(c_1490,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_952,c_1514]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.57 % Computer : n020.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Fri Sep 25 20:38:49 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.58 % Process 3723328 was started by sandbox2 on n020,
% 0.10/0.58 % Fri Sep 25 20:38:49 2026
% 0.10/0.58 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.60
% 0.10/0.60 % From the command line: assign(max_seconds, 300).
% 0.15/0.85
% 0.15/0.85 % given #500 (T,wt=6): 1214 r2_hidden(f1(c17),k1_zfmisc_1(u1_struct_0(c17))). [resolve(485,a,302,a),unit_del(a,261)].
% 0.15/0.85
% 0.15/0.85 % SZS status Theorem for theBenchmark
% 0.15/0.85
% 0.15/0.85 % Proof 1 at 0.19 (+ 0.05) seconds.
% 0.15/0.85 % Length of proof is 59.
% 0.15/0.85 % Level of proof is 7.
% 0.15/0.85 % Maximum clause weight is 15.000.
% 0.15/0.85 % Given clauses 526.
% 0.15/0.85
% 0.15/0.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------