%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU413+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 08:59:14 AM UTC 2026
% Result : Theorem 43.64s 43.95s
% Output : Proof 43.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 67 ( 35 unt; 0 def)
% Number of atoms : 237 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 257 ( 87 ~; 77 |; 75 &)
% ( 1 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 58 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t23_latsum_1,conjecture,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k1_latsum_1(A,B)))
=> ( ( r2_hidden(D,u1_struct_0(A))
& r1_orders_2(k1_latsum_1(A,B),C,D)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B) )
=> r2_hidden(C,u1_struct_0(A)) ) ) ) ) ),
file('theBenchmark.p',t23_latsum_1) ).
fof(d9_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r1_orders_2(A,B,C)
<=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ),
file('theBenchmark.p',d9_orders_2) ).
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(t21_latsum_1,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C,D] :
( ( r2_hidden(D,u1_struct_0(A))
& r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B) )
=> r2_hidden(C,u1_struct_0(A)) ) ) ),
file('theBenchmark.p',t21_latsum_1) ).
fof(f_1_1,negated_conjecture,
~ ! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B)))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(k1_latsum_1(A,B)))
=> ( ( r2_hidden(D,u1_struct_0(A))
& r1_orders_2(k1_latsum_1(A,B),C,D)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B) )
=> r2_hidden(C,u1_struct_0(A)) ) ) ) ) ),
inference(negate,[status(cth)],[t23_latsum_1]) ).
fof(f_1_2,negated_conjecture,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ~ r2_hidden(C,u1_struct_0(A))
& r2_hidden(D,u1_struct_0(A))
& r1_orders_2(k1_latsum_1(A,B),C,D)
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& m1_subset_1(D,u1_struct_0(k1_latsum_1(A,B))) )
& m1_subset_1(C,u1_struct_0(k1_latsum_1(A,B))) )
& l1_orders_2(B) )
& l1_orders_2(A) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
? [U_3] :
( ? [U_2] :
( ? [U_1] :
( ? [U_0] :
( ~ r2_hidden(U_1,u1_struct_0(U_3))
& r2_hidden(U_0,u1_struct_0(U_3))
& r1_orders_2(k1_latsum_1(U_3,U_2),U_1,U_0)
& m1_subset_1(k3_xboole_0(u1_struct_0(U_3),u1_struct_0(U_2)),k1_zfmisc_1(u1_struct_0(U_2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(U_3),u1_struct_0(U_2)),U_2)
& m1_subset_1(U_0,u1_struct_0(k1_latsum_1(U_3,U_2))) )
& m1_subset_1(U_1,u1_struct_0(k1_latsum_1(U_3,U_2))) )
& l1_orders_2(U_2) )
& l1_orders_2(U_3) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ? [U_2] :
( ? [U_1] :
( ? [U_0] :
( ~ r2_hidden(U_1,u1_struct_0(sK1))
& r2_hidden(U_0,u1_struct_0(sK1))
& r1_orders_2(k1_latsum_1(sK1,U_2),U_1,U_0)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(U_2)),k1_zfmisc_1(u1_struct_0(U_2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(U_2)),U_2)
& m1_subset_1(U_0,u1_struct_0(k1_latsum_1(sK1,U_2))) )
& m1_subset_1(U_1,u1_struct_0(k1_latsum_1(sK1,U_2))) )
& l1_orders_2(U_2) )
& l1_orders_2(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_3,sK1)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ? [U_1] :
( ? [U_0] :
( ~ r2_hidden(U_1,u1_struct_0(sK1))
& r2_hidden(U_0,u1_struct_0(sK1))
& r1_orders_2(k1_latsum_1(sK1,sK2),U_1,U_0)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
& m1_subset_1(U_0,u1_struct_0(k1_latsum_1(sK1,sK2))) )
& m1_subset_1(U_1,u1_struct_0(k1_latsum_1(sK1,sK2))) )
& l1_orders_2(sK2)
& l1_orders_2(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ? [U_0] :
( ~ r2_hidden(sK3,u1_struct_0(sK1))
& r2_hidden(U_0,u1_struct_0(sK1))
& r1_orders_2(k1_latsum_1(sK1,sK2),sK3,U_0)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
& m1_subset_1(U_0,u1_struct_0(k1_latsum_1(sK1,sK2))) )
& m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2)))
& l1_orders_2(sK2)
& l1_orders_2(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_1,sK3)],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ~ r2_hidden(sK3,u1_struct_0(sK1))
& r2_hidden(sK4,u1_struct_0(sK1))
& r1_orders_2(k1_latsum_1(sK1,sK2),sK3,sK4)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
& m1_subset_1(sK4,u1_struct_0(k1_latsum_1(sK1,sK2)))
& m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2)))
& l1_orders_2(sK2)
& l1_orders_2(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_0,sK4)],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ~ r2_hidden(sK3,u1_struct_0(sK1))
& r2_hidden(sK4,u1_struct_0(sK1))
& r1_orders_2(k1_latsum_1(sK1,sK2),sK3,sK4)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
& m1_subset_1(sK4,u1_struct_0(k1_latsum_1(sK1,sK2)))
& m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2)))
& l1_orders_2(sK2)
& l1_orders_2(sK1) ),
inference(definitional_conversion,[status(esa)],[f_1_7]) ).
cnf(f_1_9,negated_conjecture,
l1_orders_2(sK1),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_10,negated_conjecture,
l1_orders_2(sK2),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_11,negated_conjecture,
m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2))),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_12,negated_conjecture,
m1_subset_1(sK4,u1_struct_0(k1_latsum_1(sK1,sK2))),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_13,negated_conjecture,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_14,negated_conjecture,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_15,negated_conjecture,
r1_orders_2(k1_latsum_1(sK1,sK2),sK3,sK4),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_16,negated_conjecture,
r2_hidden(sK4,u1_struct_0(sK1)),
inference(clausify,[status(thm)],[f_1_8]) ).
cnf(f_1_17,negated_conjecture,
~ r2_hidden(sK3,u1_struct_0(sK1)),
inference(clausify,[status(thm)],[f_1_8]) ).
fof(f_6_1,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( r1_orders_2(A,B,C)
| ~ r2_hidden(k4_tarski(B,C),u1_orders_2(A)) )
& ( r2_hidden(k4_tarski(B,C),u1_orders_2(A))
| ~ r1_orders_2(A,B,C) ) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_orders_2(A) ),
inference(fof_nnf,[status(thm)],[d9_orders_2]) ).
fof(f_6_2,plain,
! [U_14] :
( ! [U_13] :
( ! [U_12] :
( ( ( r1_orders_2(U_14,U_13,U_12)
| ~ r2_hidden(k4_tarski(U_13,U_12),u1_orders_2(U_14)) )
& ( r2_hidden(k4_tarski(U_13,U_12),u1_orders_2(U_14))
| ~ r1_orders_2(U_14,U_13,U_12) ) )
| ~ m1_subset_1(U_12,u1_struct_0(U_14)) )
| ~ m1_subset_1(U_13,u1_struct_0(U_14)) )
| ~ l1_orders_2(U_14) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_14,U_12,U_13] :
( r1_orders_2(U_14,U_13,U_12)
| ~ r2_hidden(k4_tarski(U_13,U_12),u1_orders_2(U_14))
| ~ sP0(U_14,U_12,U_13) )
& ! [U_14,U_12,U_13] :
( r2_hidden(k4_tarski(U_13,U_12),u1_orders_2(U_14))
| ~ r1_orders_2(U_14,U_13,U_12)
| ~ sP0(U_14,U_12,U_13) )
& ! [U_14,U_12,U_13] :
( sP0(U_14,U_12,U_13)
| ~ m1_subset_1(U_12,u1_struct_0(U_14))
| ~ m1_subset_1(U_13,u1_struct_0(U_14))
| ~ l1_orders_2(U_14) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_6_2]) ).
cnf(f_6_4,plain,
( sP0(U_14,U_12,U_13)
| ~ m1_subset_1(U_12,u1_struct_0(U_14))
| ~ m1_subset_1(U_13,u1_struct_0(U_14))
| ~ l1_orders_2(U_14) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( r2_hidden(k4_tarski(U_13,U_12),u1_orders_2(U_14))
| ~ r1_orders_2(U_14,U_13,U_12)
| ~ sP0(U_14,U_12,U_13) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_8_1,plain,
! [A,B] :
( ( l1_orders_2(k1_latsum_1(A,B))
& v1_orders_2(k1_latsum_1(A,B)) )
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(fof_nnf,[status(thm)],[dt_k1_latsum_1]) ).
fof(f_8_2,plain,
! [U_18,U_17] :
( ( l1_orders_2(k1_latsum_1(U_18,U_17))
& v1_orders_2(k1_latsum_1(U_18,U_17)) )
| ~ l1_orders_2(U_17)
| ~ l1_orders_2(U_18) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_18,U_17] :
( l1_orders_2(k1_latsum_1(U_18,U_17))
| ~ sP2(U_18,U_17) )
& ! [U_18,U_17] :
( v1_orders_2(k1_latsum_1(U_18,U_17))
| ~ sP2(U_18,U_17) )
& ! [U_18,U_17] :
( sP2(U_18,U_17)
| ~ l1_orders_2(U_17)
| ~ l1_orders_2(U_18) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP2])],[f_8_2]) ).
cnf(f_8_4,plain,
( sP2(U_18,U_17)
| ~ l1_orders_2(U_17)
| ~ l1_orders_2(U_18) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_6,plain,
( l1_orders_2(k1_latsum_1(U_18,U_17))
| ~ sP2(U_18,U_17) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_34_1,plain,
! [A] :
( ! [B] :
( ! [C,D] :
( r2_hidden(C,u1_struct_0(A))
| ~ r2_hidden(D,u1_struct_0(A))
| ~ r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(fof_nnf,[status(thm)],[t21_latsum_1]) ).
fof(f_34_2,plain,
! [U_58] :
( ! [U_57] :
( ! [U_56,U_55] :
( r2_hidden(U_56,u1_struct_0(U_58))
| ~ r2_hidden(U_55,u1_struct_0(U_58))
| ~ r2_hidden(k4_tarski(U_56,U_55),u1_orders_2(k1_latsum_1(U_58,U_57)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),k1_zfmisc_1(u1_struct_0(U_57)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),U_57) )
| ~ l1_orders_2(U_57) )
| ~ l1_orders_2(U_58) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
! [U_58] :
( ! [U_57] :
( ! [U_56] :
( ! [U_55] :
( ~ r2_hidden(U_55,u1_struct_0(U_58))
| ~ r2_hidden(k4_tarski(U_56,U_55),u1_orders_2(k1_latsum_1(U_58,U_57))) )
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),k1_zfmisc_1(u1_struct_0(U_57)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),U_57)
| r2_hidden(U_56,u1_struct_0(U_58)) )
| ~ l1_orders_2(U_57) )
| ~ l1_orders_2(U_58) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
fof(f_34_4,plain,
! [U_56,U_55,U_57,U_58] :
( ~ r2_hidden(U_55,u1_struct_0(U_58))
| ~ r2_hidden(k4_tarski(U_56,U_55),u1_orders_2(k1_latsum_1(U_58,U_57)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),k1_zfmisc_1(u1_struct_0(U_57)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),U_57)
| r2_hidden(U_56,u1_struct_0(U_58))
| ~ l1_orders_2(U_57)
| ~ l1_orders_2(U_58) ),
inference(definitional_conversion,[status(esa)],[f_34_3]) ).
cnf(f_34_5,plain,
( ~ r2_hidden(U_55,u1_struct_0(U_58))
| ~ r2_hidden(k4_tarski(U_56,U_55),u1_orders_2(k1_latsum_1(U_58,U_57)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),k1_zfmisc_1(u1_struct_0(U_57)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(U_58),u1_struct_0(U_57)),U_57)
| r2_hidden(U_56,u1_struct_0(U_58))
| ~ l1_orders_2(U_57)
| ~ l1_orders_2(U_58) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(t1,plain,
m1_subset_1(sK4,u1_struct_0(k1_latsum_1(sK1,sK2))),
inference(start,[status(thm),parent(0:0)],[f_1_12]) ).
cnf(t2,plain,
( ~ m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2)))
| sP0(k1_latsum_1(sK1,sK2),sK4,sK3)
| ~ l1_orders_2(k1_latsum_1(sK1,sK2))
| ~ m1_subset_1(sK4,u1_struct_0(k1_latsum_1(sK1,sK2))) ),
inference(extension,[status(thm),parent(t1:1)],[f_6_4]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ sP2(sK1,sK2)
| l1_orders_2(k1_latsum_1(sK1,sK2)) ),
inference(extension,[status(thm),parent(t2:2)],[f_8_6]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK1)
| sP2(sK1,sK2) ),
inference(extension,[status(thm),parent(t4:2)],[f_8_4]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
l1_orders_2(sK1),
inference(extension,[status(thm),parent(t6:2)],[f_1_9]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
l1_orders_2(sK2),
inference(extension,[status(thm),parent(t6:3)],[f_1_10]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t6:3]) ).
cnf(t12,plain,
( ~ r1_orders_2(k1_latsum_1(sK1,sK2),sK3,sK4)
| r2_hidden(k4_tarski(sK3,sK4),u1_orders_2(k1_latsum_1(sK1,sK2)))
| ~ sP0(k1_latsum_1(sK1,sK2),sK4,sK3) ),
inference(extension,[status(thm),parent(t2:3)],[f_6_5]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t2:3]) ).
cnf(t14,plain,
( ~ l1_orders_2(sK2)
| r2_hidden(sK3,u1_struct_0(sK1))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2)))
| ~ r2_hidden(sK4,u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ r2_hidden(k4_tarski(sK3,sK4),u1_orders_2(k1_latsum_1(sK1,sK2))) ),
inference(extension,[status(thm),parent(t12:2)],[f_34_5]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
l1_orders_2(sK1),
inference(extension,[status(thm),parent(t14:2)],[f_1_9]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
r2_hidden(sK4,u1_struct_0(sK1)),
inference(extension,[status(thm),parent(t14:3)],[f_1_16]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t14:3]) ).
cnf(t20,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),k1_zfmisc_1(u1_struct_0(sK2))),
inference(extension,[status(thm),parent(t14:4)],[f_1_14]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t14:4]) ).
cnf(t22,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK2)),sK2),
inference(extension,[status(thm),parent(t14:5)],[f_1_13]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t14:5]) ).
cnf(t24,plain,
~ r2_hidden(sK3,u1_struct_0(sK1)),
inference(extension,[status(thm),parent(t14:6)],[f_1_17]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t14:6]) ).
cnf(t26,plain,
l1_orders_2(sK2),
inference(extension,[status(thm),parent(t14:7)],[f_1_10]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t14:7]) ).
cnf(t28,plain,
r1_orders_2(k1_latsum_1(sK1,sK2),sK3,sK4),
inference(extension,[status(thm),parent(t12:3)],[f_1_15]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t12:3]) ).
cnf(t30,plain,
m1_subset_1(sK3,u1_struct_0(k1_latsum_1(sK1,sK2))),
inference(extension,[status(thm),parent(t2:4)],[f_1_11]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t2:4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU413+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.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 : Sun Sep 20 00:18:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 43.64/43.95 % SZS status Theorem for theBenchmark
% 43.64/43.95 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------