%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU407+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 : n006.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:12 AM UTC 2026
% Result : Theorem 24.29s 14.21s
% Output : CNFRefutation 24.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 49 ( 16 unt; 0 def)
% Number of atoms : 146 ( 19 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 172 ( 75 ~; 56 |; 24 &)
% ( 3 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-6 aty)
% Number of variables : 64 ( 0 sgn 23 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(dt_l1_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_orders_2) ).
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(fc2_latsum_1,axiom,
! [A,B] :
( ( l1_orders_2(B)
& l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v1_orders_2(k1_latsum_1(A,B))
& ~ v3_struct_0(k1_latsum_1(A,B)) ) ),
file('theBenchmark.p',fc2_latsum_1) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t39_xboole_1,axiom,
! [A,B] : k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B),
file('theBenchmark.p',t39_xboole_1) ).
fof(t7_latsum_1,conjecture,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
=> ( r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A)))
| r2_hidden(C,u1_struct_0(A)) ) ) ) ),
file('theBenchmark.p',t7_latsum_1) ).
fof(t7_latsum_1_neg,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
=> ( r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A)))
| r2_hidden(C,u1_struct_0(A)) ) ) ) ),
inference(assume_negation,[status(cth)],[t7_latsum_1]) ).
cnf(c_58,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_60,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_69,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_71,plain,
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_l1_orders_2]) ).
cnf(c_89,plain,
( r2_hidden(D,B)
| r2_hidden(D,A)
| ~ r2_hidden(D,C)
| k2_xboole_0(A,B) != C ),
inference(clausify,[status(thm)],[d2_xboole_0]) ).
cnf(c_96,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_103,plain,
( ~ v3_struct_0(k1_latsum_1(A,B))
| ~ l1_orders_2(B)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc2_latsum_1]) ).
cnf(c_116,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_117,plain,
k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B),
inference(clausify,[status(thm)],[t39_xboole_1]) ).
fof(nnf_54,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r2_hidden(C,k4_xboole_0(u1_struct_0(B),u1_struct_0(A)))
& ~ r2_hidden(C,u1_struct_0(A))
& m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) )
& l1_orders_2(B)
& ~ v3_struct_0(B) )
& l1_orders_2(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t7_latsum_1_neg]) ).
fof(sk_t7_latsum_1_neg,plain,
( ~ r2_hidden(sK2,k4_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
& ~ r2_hidden(sK2,u1_struct_0(sK0))
& m1_subset_1(sK2,u1_struct_0(k1_latsum_1(sK0,sK1)))
& l1_orders_2(sK1)
& ~ v3_struct_0(sK1)
& l1_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_54]) ).
cnf(c_125,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_126,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_128,negated_conjecture,
l1_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_129,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_130,negated_conjecture,
~ r2_hidden(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_131,negated_conjecture,
~ r2_hidden(sK2,k4_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t7_latsum_1_neg]) ).
cnf(c_141,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_60,c_58]) ).
cnf(c_144,plain,
( ~ l1_orders_2(A)
| ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_69,c_71]) ).
cnf(c_194,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_141]) ).
cnf(c_1598,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_194]) ).
cnf(c_241,plain,
( k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) = u1_struct_0(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_1598]) ).
cnf(c_1599,negated_conjecture,
( l1_orders_2(k1_latsum_1(sK0,A))
| ~ l1_orders_2(A) ),
inference(resolve,[status(thm)],[c_96,c_126]) ).
cnf(c_581,negated_conjecture,
l1_orders_2(k1_latsum_1(sK0,sK1)),
inference(resolve,[status(thm)],[c_1599,c_128]) ).
cnf(c_1600,negated_conjecture,
( ~ v3_struct_0(k1_latsum_1(sK0,A))
| ~ l1_orders_2(A)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_103,c_125]) ).
cnf(c_1601,negated_conjecture,
( ~ v3_struct_0(k1_latsum_1(sK0,A))
| ~ l1_orders_2(A) ),
inference(resolve,[status(thm)],[c_1600,c_126]) ).
cnf(c_586,negated_conjecture,
~ v3_struct_0(k1_latsum_1(sK0,sK1)),
inference(resolve,[status(thm)],[c_1601,c_128]) ).
cnf(c_590,plain,
( r2_hidden(sK2,u1_struct_0(k1_latsum_1(sK0,sK1)))
| v1_xboole_0(u1_struct_0(k1_latsum_1(sK0,sK1))) ),
inference(resolve,[status(thm)],[c_129,c_116]) ).
cnf(c_1602,plain,
( r2_hidden(A,k4_xboole_0(C,B))
| r2_hidden(A,B)
| ~ r2_hidden(A,k2_xboole_0(B,C)) ),
inference(resolve,[status(thm)],[c_89,c_117]) ).
cnf(c_1603,negated_conjecture,
( r2_hidden(sK2,k4_xboole_0(A,u1_struct_0(sK0)))
| ~ r2_hidden(sK2,k2_xboole_0(u1_struct_0(sK0),A)) ),
inference(resolve,[status(thm)],[c_1602,c_130]) ).
cnf(c_591,negated_conjecture,
~ r2_hidden(sK2,k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_1603,c_131]) ).
cnf(c_1604,plain,
( k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)) = u1_struct_0(k1_latsum_1(sK0,sK1))
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_581,c_241]) ).
cnf(c_1605,negated_conjecture,
( k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)) = u1_struct_0(k1_latsum_1(sK0,sK1))
| ~ l1_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_126,c_1604]) ).
cnf(c_1466,negated_conjecture,
k2_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)) = u1_struct_0(k1_latsum_1(sK0,sK1)),
inference(resolve,[status(thm)],[c_128,c_1605]) ).
cnf(c_1585,negated_conjecture,
~ r2_hidden(sK2,u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(paramod,[status(thm)],[c_1466,c_591]) ).
cnf(c_1586,plain,
v1_xboole_0(u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(resolve,[status(thm)],[c_1585,c_590]) ).
cnf(c_1606,plain,
( ~ l1_orders_2(k1_latsum_1(sK0,sK1))
| ~ v1_xboole_0(u1_struct_0(k1_latsum_1(sK0,sK1))) ),
inference(resolve,[status(thm)],[c_144,c_586]) ).
cnf(c_1607,plain,
~ v1_xboole_0(u1_struct_0(k1_latsum_1(sK0,sK1))),
inference(resolve,[status(thm)],[c_1606,c_581]) ).
cnf(c_1597,plain,
$false,
inference(resolve,[status(thm)],[c_1586,c_1607]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU407+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.10/10.59 % Computer : n006.cluster.edu
% 0.10/10.59 % Model : x86_64 x86_64
% 0.10/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.59 % Memory : 8046.5625MB
% 0.10/10.59 % OS : Linux 6.8.0-71-generic
% 0.10/10.59 % CPULimit : 300
% 0.10/10.59 % WCLimit : 300
% 0.10/10.59 % DateTime : Sat Sep 26 09:27:52 UTC 2026
% 0.14/10.60 % CPUTime :
% 0.14/10.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/10.60 % Process 939826 was started by sandbox on n006,
% 0.14/10.60 % Sat Sep 26 09:27:52 2026
% 0.14/10.60 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/10.61
% 0.14/10.61 % From the command line: assign(max_seconds, 300).
% 24.29/14.21
% 24.29/14.21 % SZS status Theorem for theBenchmark
% 24.29/14.21
% 24.29/14.21 % Proof 1 at 3.32 (+ 0.09) seconds.
% 24.29/14.21 % Length of proof is 36.
% 24.29/14.21 % Level of proof is 8.
% 24.29/14.21 % Maximum clause weight is 44.000.
% 24.29/14.21 % Given clauses 200.
% 24.29/14.21
% 24.29/14.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------