%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU408+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 08:46:13 AM UTC 2026
% Result : Theorem 91.40s 12.02s
% Output : CNFRefutation 91.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 9
% Syntax : Number of formulae : 47 ( 22 unt; 0 def)
% Number of atoms : 156 ( 26 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 165 ( 56 ~; 43 |; 51 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-6 aty)
% Number of variables : 74 ( 6 sgn 25 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_xboole_0,axiom,
! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(d2_latsum_1,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( ( l1_orders_2(C)
& v1_orders_2(C) )
=> ( C = k1_latsum_1(A,B)
<=> ( u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))
& u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) ) ) ) ) ),
file('theBenchmark.p',d2_latsum_1) ).
fof(d2_xboole_0,axiom,
! [A,B,C] :
( C = k2_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,B)
| r2_hidden(D,A) ) ) ),
file('theBenchmark.p',d2_xboole_0) ).
fof(dt_k1_latsum_1,axiom,
! [A,B] :
( ( l1_orders_2(B)
& l1_orders_2(A) )
=> ( l1_orders_2(k1_latsum_1(A,B))
& v1_orders_2(k1_latsum_1(A,B)) ) ),
file('theBenchmark.p',dt_k1_latsum_1) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t1_boole,axiom,
! [A] : k2_xboole_0(A,k1_xboole_0) = A,
file('theBenchmark.p',t1_boole) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t11_latsum_1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( r2_hidden(C,u1_struct_0(B))
=> m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) ) ) ),
file('theBenchmark.p',t11_latsum_1) ).
fof(t11_latsum_1_neg,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( r2_hidden(C,u1_struct_0(B))
=> m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) ) ) ),
inference(assume_negation,[status(cth)],[t11_latsum_1]) ).
cnf(c_54,plain,
( k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) = u1_struct_0(C)
| k1_latsum_1(A,B) != C
| ~ l1_orders_2(C)
| ~ v1_orders_2(C)
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[d2_latsum_1]) ).
cnf(c_56,plain,
( v1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_k1_latsum_1]) ).
cnf(c_72,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_73,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_74,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_73,c_72]) ).
cnf(c_84,plain,
k2_xboole_0(A,B) = k2_xboole_0(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_87,plain,
( ~ r2_hidden(D,B)
| r2_hidden(D,C)
| k2_xboole_0(A,B) != C ),
inference(clausify,[status(thm)],[d2_xboole_0]) ).
cnf(c_92,plain,
( l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_k1_latsum_1]) ).
cnf(c_110,plain,
k2_xboole_0(A,k1_xboole_0) = A,
inference(clausify,[status(thm)],[t1_boole]) ).
cnf(c_113,plain,
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
fof(nnf_50,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
& r2_hidden(C,u1_struct_0(B)) )
& l1_orders_2(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
& l1_orders_2(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t11_latsum_1_neg]) ).
fof(sk_t11_latsum_1_neg,plain,
( ~ m1_subset_1(sK2,u1_struct_0(k1_latsum_1(sK0,sK1)))
& r2_hidden(sK2,u1_struct_0(sK1))
& l1_orders_2(sK1)
& v1_lattice3(sK1)
& v4_orders_2(sK1)
& v3_orders_2(sK1)
& v2_orders_2(sK1)
& ~ v3_struct_0(sK1)
& l1_orders_2(sK0)
& v1_lattice3(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_50]) ).
cnf(c_119,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t11_latsum_1_neg]) ).
cnf(c_121,negated_conjecture,
l1_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t11_latsum_1_neg]) ).
cnf(c_122,negated_conjecture,
r2_hidden(sK2,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t11_latsum_1_neg]) ).
cnf(c_123,negated_conjecture,
~ m1_subset_1(sK2,u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(split_conjunct,[status(thm)],[sk_t11_latsum_1_neg]) ).
cnf(c_133,plain,
( k2_xboole_0(u1_struct_0(C),u1_struct_0(D)) = u1_struct_0(k1_latsum_1(A,B))
| k1_latsum_1(C,D) != k1_latsum_1(A,B)
| ~ l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(D)
| ~ l1_orders_2(C)
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(resolve,[status(thm)],[c_56,c_54]) ).
cnf(c_186,plain,
( k2_xboole_0(u1_struct_0(A),u1_struct_0(C)) = u1_struct_0(k1_latsum_1(A,B))
| k1_latsum_1(A,C) != k1_latsum_1(A,B)
| ~ l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(C)
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(factor,[status(thm)],[c_133]) ).
cnf(c_1595,plain,
( k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) = u1_struct_0(k1_latsum_1(A,B))
| k1_latsum_1(A,B) != k1_latsum_1(A,B)
| ~ l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(factor,[status(thm)],[c_186]) ).
cnf(c_1596,plain,
( u1_struct_0(k1_latsum_1(A,B)) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B))
| k1_latsum_1(A,B) != k1_latsum_1(A,B)
| ~ l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(copy,[status(thm)],[c_1595]) ).
cnf(c_233,plain,
( u1_struct_0(k1_latsum_1(A,B)) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B))
| ~ l1_orders_2(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(copy,[status(thm)],[c_1596]) ).
cnf(c_1597,plain,
A = k2_xboole_0(k1_xboole_0,A),
inference(paramod,[status(thm)],[c_110,c_84]) ).
cnf(c_451,plain,
k2_xboole_0(k1_xboole_0,A) = A,
inference(copy,[status(thm)],[c_1597]) ).
cnf(c_1598,negated_conjecture,
( l1_orders_2(k1_latsum_1(sK0,A))
| ~ l1_orders_2(A) ),
inference(resolve,[status(thm)],[c_92,c_119]) ).
cnf(c_529,negated_conjecture,
l1_orders_2(k1_latsum_1(sK0,sK1)),
inference(resolve,[status(thm)],[c_1598,c_121]) ).
cnf(c_1599,plain,
A = k2_xboole_0(A,k1_xboole_0),
inference(copy,[status(thm)],[c_110]) ).
cnf(c_1600,plain,
( ~ r2_hidden(A,C)
| r2_hidden(A,k2_xboole_0(k2_xboole_0(B,C),k1_xboole_0)) ),
inference(resolve,[status(thm)],[c_87,c_1599]) ).
cnf(c_1601,negated_conjecture,
r2_hidden(sK2,k2_xboole_0(k2_xboole_0(A,u1_struct_0(sK1)),k1_xboole_0)),
inference(resolve,[status(thm)],[c_1600,c_122]) ).
cnf(c_1602,negated_conjecture,
r2_hidden(sK2,k2_xboole_0(k1_xboole_0,k2_xboole_0(A,u1_struct_0(sK1)))),
inference(paramod,[status(thm)],[c_84,c_1601]) ).
cnf(c_545,negated_conjecture,
r2_hidden(sK2,k2_xboole_0(A,u1_struct_0(sK1))),
inference(paramod,[status(thm)],[c_451,c_1602]) ).
cnf(c_1603,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(resolve,[status(thm)],[c_113,c_74]) ).
cnf(c_549,negated_conjecture,
~ r2_hidden(sK2,u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(resolve,[status(thm)],[c_1603,c_123]) ).
cnf(c_1604,plain,
( u1_struct_0(k1_latsum_1(sK0,sK1)) = k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_529,c_233]) ).
cnf(c_1605,negated_conjecture,
( u1_struct_0(k1_latsum_1(sK0,sK1)) = k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1))
| ~ l1_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_119,c_1604]) ).
cnf(c_1456,negated_conjecture,
u1_struct_0(k1_latsum_1(sK0,sK1)) = k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_121,c_1605]) ).
cnf(c_1606,negated_conjecture,
~ r2_hidden(sK2,k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1))),
inference(paramod,[status(thm)],[c_1456,c_549]) ).
cnf(c_1594,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_545,c_1606]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU408+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.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 09:29:19 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 1226523 was started by sandbox2 on n020,
% 0.11/0.37 % Sat Sep 26 09:29:19 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.39
% 0.11/0.39 % From the command line: assign(max_seconds, 300).
% 91.40/12.02
% 91.40/12.02 % SZS status Theorem for theBenchmark
% 91.40/12.02
% 91.40/12.02 % Proof 1 at 3.54 (+ 0.06) seconds.
% 91.40/12.02 % Length of proof is 32.
% 91.40/12.02 % Level of proof is 6.
% 91.40/12.02 % Maximum clause weight is 35.000.
% 91.40/12.02 % Given clauses 203.
% 91.40/12.02
% 91.40/12.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------