%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT359+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 01:56:58 PM UTC 2026
% Result : Theorem 76.66s 11.90s
% Output : Proof 76.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 12
% Syntax : Number of formulae : 94 ( 21 unt; 0 def)
% Number of atoms : 297 ( 62 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 340 ( 137 ~; 129 |; 52 &)
% ( 4 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 151 ( 9 sgn 85 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f68_nnf,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f68]) ).
fof(f68_sk,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f68_nnf]) ).
cnf(c136,plain,
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f68_sk]) ).
fof(f36,axiom,
! [A] :
( l1_altcat_1(A)
=> m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_altcat_1) ).
fof(f36_nnf,plain,
! [A] :
( m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)))
| ~ l1_altcat_1(A) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [A] :
( m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)))
| ~ l1_altcat_1(A) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c60,plain,
( m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
fof(f33,axiom,
! [A] :
( l2_altcat_1(A)
=> l1_altcat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f33_nnf,plain,
! [A] :
( l1_altcat_1(A)
| ~ l2_altcat_1(A) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A] :
( l1_altcat_1(A)
| ~ l2_altcat_1(A) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c56,plain,
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
fof(f0,conjecture,
! [A] :
( ( l2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B,C,D] :
~ ( ! [E] :
( m1_subset_1(E,u1_struct_0(A))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(A))
=> ~ ( m1_subset_1(D,k1_altcat_1(A,E,F))
& r2_hidden(D,k1_altcat_1(A,E,F))
& F = C
& E = B ) ) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_waybel34) ).
fof(f0_neg,negated_conjecture,
~ ! [A] :
( ( l2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B,C,D] :
~ ( ! [E] :
( m1_subset_1(E,u1_struct_0(A))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(A))
=> ~ ( m1_subset_1(D,k1_altcat_1(A,E,F))
& r2_hidden(D,k1_altcat_1(A,E,F))
& F = C
& E = B ) ) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [A] :
( ? [B,C,D] :
( ! [E] :
( ! [F] :
( ~ m1_subset_1(D,k1_altcat_1(A,E,F))
| ~ r2_hidden(D,k1_altcat_1(A,E,F))
| F != C
| E != B
| ~ m1_subset_1(F,u1_struct_0(A)) )
| ~ m1_subset_1(E,u1_struct_0(A)) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) )
& l2_altcat_1(A)
& ~ v3_struct_0(A) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [E,F] :
( ( ~ m1_subset_1(sk3,k1_altcat_1(sk0,E,F))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,E,F))
| F != sk2
| E != sk1
| ~ m1_subset_1(F,u1_struct_0(sk0))
| ~ m1_subset_1(E,u1_struct_0(sk0)) )
& r2_hidden(sk3,k1_binop_1(u1_altcat_1(sk0),sk1,sk2))
& l2_altcat_1(sk0)
& ~ v3_struct_0(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c1,plain,
l2_altcat_1(sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p177,plain,
l1_altcat_1(sk0),
inference(resolution,[status(thm)],[c56,c1]) ).
cnf(p254,plain,
m1_pboole(u1_altcat_1(sk0),k2_zfmisc_1(u1_struct_0(sk0),u1_struct_0(sk0))),
inference(resolution,[status(thm)],[c60,p177]) ).
fof(f34,axiom,
! [A,B] :
( m1_pboole(B,A)
=> ( v1_funct_1(B)
& v1_relat_1(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_pboole) ).
fof(f34_nnf,plain,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
| ~ m1_pboole(B,A) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [B,A] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
| ~ m1_pboole(B,A) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c57,plain,
( v1_relat_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p256,plain,
v1_relat_1(u1_altcat_1(sk0)),
inference(resolution,[status(thm)],[p254,c57]) ).
fof(f19,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( m1_pboole(B,A)
<=> k1_relat_1(B) = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pboole) ).
fof(f19_nnf,plain,
! [A,B] :
( ( ( k1_relat_1(B) != A
| m1_pboole(B,A) )
& ( k1_relat_1(B) = A
| ~ m1_pboole(B,A) ) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [B,A] :
( ( ( k1_relat_1(B) != A
| m1_pboole(B,A) )
& ( k1_relat_1(B) = A
| ~ m1_pboole(B,A) ) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c38,plain,
( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0)
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p260,plain,
( k1_relat_1(u1_altcat_1(sk0)) = X0
| ~ m1_pboole(u1_altcat_1(sk0),X0)
| ~ v1_funct_1(u1_altcat_1(sk0)) ),
inference(resolution,[status(thm)],[p256,c38]) ).
cnf(c58,plain,
( v1_funct_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p257,plain,
v1_funct_1(u1_altcat_1(sk0)),
inference(resolution,[status(thm)],[p254,c58]) ).
cnf(p269,plain,
( k1_relat_1(u1_altcat_1(sk0)) = X0
| ~ m1_pboole(u1_altcat_1(sk0),X0) ),
inference(resolution,[status(thm)],[p260,p257]) ).
cnf(p270,plain,
k1_relat_1(u1_altcat_1(sk0)) = k2_zfmisc_1(u1_struct_0(sk0),u1_struct_0(sk0)),
inference(resolution,[status(thm)],[p269,p254]) ).
fof(f67,axiom,
! [A,B,C,D] :
( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
<=> ( r2_hidden(B,D)
& r2_hidden(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f67_nnf,plain,
! [A,B,C,D] :
( ( ~ r2_hidden(B,D)
| ~ r2_hidden(A,C)
| r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) )
& ( ( r2_hidden(B,D)
& r2_hidden(A,C) )
| ~ r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A,B,C,D] :
( ( ~ r2_hidden(B,D)
| ~ r2_hidden(A,C)
| r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) )
& ( ( r2_hidden(B,D)
& r2_hidden(A,C) )
| ~ r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) ) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c133,plain,
( r2_hidden(X0,X2)
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p397,plain,
( r2_hidden(X0,u1_struct_0(sk0))
| ~ r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sk0))) ),
inference(superposition,[status(thm)],[p270,c133]) ).
fof(f20,axiom,
! [A] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ! [B,C] :
( ( ~ r2_hidden(B,k1_relat_1(A))
=> ( C = k1_funct_1(A,B)
<=> C = k1_xboole_0 ) )
& ( r2_hidden(B,k1_relat_1(A))
=> ( C = k1_funct_1(A,B)
<=> r2_hidden(k4_tarski(B,C),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f20_nnf,plain,
! [A] :
( ! [B,C] :
( ( ( ( C != k1_xboole_0
| C = k1_funct_1(A,B) )
& ( C = k1_xboole_0
| C != k1_funct_1(A,B) ) )
| r2_hidden(B,k1_relat_1(A)) )
& ( ( ( ~ r2_hidden(k4_tarski(B,C),A)
| C = k1_funct_1(A,B) )
& ( r2_hidden(k4_tarski(B,C),A)
| C != k1_funct_1(A,B) ) )
| ~ r2_hidden(B,k1_relat_1(A)) ) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A,B,C] :
( ( ( ( ( C != k1_xboole_0
| C = k1_funct_1(A,B) )
& ( C = k1_xboole_0
| C != k1_funct_1(A,B) ) )
| r2_hidden(B,k1_relat_1(A)) )
& ( ( ( ~ r2_hidden(k4_tarski(B,C),A)
| C = k1_funct_1(A,B) )
& ( r2_hidden(k4_tarski(B,C),A)
| C != k1_funct_1(A,B) ) )
| ~ r2_hidden(B,k1_relat_1(A)) ) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c42,plain,
( X2 = k1_xboole_0
| X2 != k1_funct_1(X0,X1)
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p264,plain,
( X1 = k1_xboole_0
| X1 != k1_funct_1(u1_altcat_1(sk0),X0)
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0)))
| ~ v1_funct_1(u1_altcat_1(sk0)) ),
inference(resolution,[status(thm)],[p256,c42]) ).
cnf(p283,plain,
( k1_funct_1(u1_altcat_1(sk0),X0) = k1_xboole_0
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0)))
| ~ v1_funct_1(u1_altcat_1(sk0)) ),
inference(equality_resolution,[status(thm)],[p264]) ).
cnf(p291,plain,
( k1_funct_1(u1_altcat_1(sk0),X0) = k1_xboole_0
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0))) ),
inference(resolution,[status(thm)],[p283,p257]) ).
cnf(c43,plain,
( X2 != k1_xboole_0
| X2 = k1_funct_1(X0,X1)
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p265,plain,
( X1 != k1_xboole_0
| X1 = k1_funct_1(u1_altcat_1(sk0),X0)
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0)))
| ~ v1_funct_1(u1_altcat_1(sk0)) ),
inference(resolution,[status(thm)],[p256,c43]) ).
cnf(p301,plain,
( X1 != k1_xboole_0
| X1 = k1_funct_1(u1_altcat_1(sk0),X0)
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0))) ),
inference(resolution,[status(thm)],[p265,p257]) ).
cnf(p311,plain,
( r2_hidden(X1,k1_relat_1(u1_altcat_1(sk0)))
| k1_funct_1(u1_altcat_1(sk0),X1) = k1_funct_1(u1_altcat_1(sk0),X0)
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0))) ),
inference(resolution,[status(thm)],[p301,p291]) ).
fof(f17,axiom,
! [A] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_binop_1) ).
fof(f17_nnf,plain,
! [A] :
( ! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C))
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B,C] :
( k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C))
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c36,plain,
( k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p259,plain,
( k1_binop_1(u1_altcat_1(sk0),X0,X1) = k1_funct_1(u1_altcat_1(sk0),k4_tarski(X0,X1))
| ~ v1_funct_1(u1_altcat_1(sk0)) ),
inference(resolution,[status(thm)],[p256,c36]) ).
cnf(p276,plain,
k1_binop_1(u1_altcat_1(sk0),X0,X1) = k1_funct_1(u1_altcat_1(sk0),k4_tarski(X0,X1)),
inference(resolution,[status(thm)],[p259,p257]) ).
cnf(p312,plain,
( k1_binop_1(u1_altcat_1(sk0),X1,X2) = k1_funct_1(u1_altcat_1(sk0),X0)
| r2_hidden(k4_tarski(X1,X2),k1_relat_1(u1_altcat_1(sk0)))
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0))) ),
inference(superposition,[status(thm)],[p311,p276]) ).
fof(f71,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f71_nnf,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(nnf_transformation,[status(thm)],[f71]) ).
fof(f71_sk,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(skolemisation,[status(esa)],[f71_nnf]) ).
cnf(c139,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(c2,plain,
r2_hidden(sk3,k1_binop_1(u1_altcat_1(sk0),sk1,sk2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p218,plain,
~ v1_xboole_0(k1_binop_1(u1_altcat_1(sk0),sk1,sk2)),
inference(resolution,[status(thm)],[c139,c2]) ).
cnf(p356,plain,
( ~ v1_xboole_0(k1_funct_1(u1_altcat_1(sk0),X0))
| r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0)))
| r2_hidden(X0,k1_relat_1(u1_altcat_1(sk0))) ),
inference(superposition,[status(thm)],[p312,p218]) ).
cnf(p360,plain,
( ~ v1_xboole_0(k1_funct_1(u1_altcat_1(sk0),k4_tarski(sk1,sk2)))
| r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0))) ),
inference(factoring,[status(thm)],[p356]) ).
cnf(p364,plain,
( ~ v1_xboole_0(k1_xboole_0)
| r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0)))
| r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0))) ),
inference(superposition,[status(thm)],[p291,p360]) ).
cnf(p366,plain,
( ~ v1_xboole_0(k1_xboole_0)
| r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0))) ),
inference(factoring,[status(thm)],[p364]) ).
fof(f56,axiom,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_membered) ).
fof(f56_nnf,plain,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c101,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p367,plain,
r2_hidden(k4_tarski(sk1,sk2),k1_relat_1(u1_altcat_1(sk0))),
inference(resolution,[status(thm)],[p366,c101]) ).
cnf(p402,plain,
r2_hidden(sk1,u1_struct_0(sk0)),
inference(resolution,[status(thm)],[p397,p367]) ).
cnf(p455,plain,
m1_subset_1(sk1,u1_struct_0(sk0)),
inference(resolution,[status(thm)],[c136,p402]) ).
cnf(c3,plain,
( ~ m1_subset_1(sk3,k1_altcat_1(sk0,X4,X5))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,X4,X5))
| X5 != sk2
| X4 != sk1
| ~ m1_subset_1(X5,u1_struct_0(sk0))
| ~ m1_subset_1(X4,u1_struct_0(sk0)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p142,plain,
( ~ m1_subset_1(sk3,k1_altcat_1(sk0,sk1,X0))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,sk1,X0))
| X0 != sk2
| ~ m1_subset_1(X0,u1_struct_0(sk0))
| ~ m1_subset_1(sk1,u1_struct_0(sk0)) ),
inference(equality_resolution,[status(thm)],[c3]) ).
cnf(p148,plain,
( ~ m1_subset_1(sk3,k1_altcat_1(sk0,sk1,sk2))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,sk1,sk2))
| ~ m1_subset_1(sk2,u1_struct_0(sk0))
| ~ m1_subset_1(sk1,u1_struct_0(sk0)) ),
inference(equality_resolution,[status(thm)],[p142]) ).
cnf(p461,plain,
( ~ m1_subset_1(sk3,k1_altcat_1(sk0,sk1,sk2))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,sk1,sk2))
| ~ m1_subset_1(sk2,u1_struct_0(sk0)) ),
inference(resolution,[status(thm)],[p455,p148]) ).
cnf(c134,plain,
( r2_hidden(X1,X3)
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p405,plain,
( r2_hidden(X1,u1_struct_0(sk0))
| ~ r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sk0))) ),
inference(superposition,[status(thm)],[p270,c134]) ).
cnf(p410,plain,
r2_hidden(sk2,u1_struct_0(sk0)),
inference(resolution,[status(thm)],[p405,p367]) ).
cnf(p456,plain,
m1_subset_1(sk2,u1_struct_0(sk0)),
inference(resolution,[status(thm)],[c136,p410]) ).
cnf(p5462,plain,
( ~ m1_subset_1(sk3,k1_altcat_1(sk0,sk1,sk2))
| ~ r2_hidden(sk3,k1_altcat_1(sk0,sk1,sk2)) ),
inference(resolution,[status(thm)],[p461,p456]) ).
fof(f18,axiom,
! [A] :
( l1_altcat_1(A)
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_altcat_1) ).
fof(f18_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_altcat_1(A) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A,B,C] :
( k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_altcat_1(A) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c37,plain,
( k1_altcat_1(X0,X1,X2) = k1_binop_1(u1_altcat_1(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p192,plain,
( k1_altcat_1(sk0,X0,X1) = k1_binop_1(u1_altcat_1(sk0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sk0))
| ~ m1_subset_1(X0,u1_struct_0(sk0)) ),
inference(resolution,[status(thm)],[c37,p177]) ).
cnf(p463,plain,
( k1_altcat_1(sk0,sk1,X0) = k1_binop_1(u1_altcat_1(sk0),sk1,X0)
| ~ m1_subset_1(X0,u1_struct_0(sk0)) ),
inference(resolution,[status(thm)],[p455,p192]) ).
cnf(p902,plain,
k1_altcat_1(sk0,sk1,sk2) = k1_binop_1(u1_altcat_1(sk0),sk1,sk2),
inference(resolution,[status(thm)],[p463,p456]) ).
cnf(p903,plain,
r2_hidden(sk3,k1_altcat_1(sk0,sk1,sk2)),
inference(superposition,[status(thm)],[p902,c2]) ).
cnf(p5463,plain,
~ m1_subset_1(sk3,k1_altcat_1(sk0,sk1,sk2)),
inference(resolution,[status(thm)],[p5462,p903]) ).
cnf(p443,plain,
m1_subset_1(sk3,k1_binop_1(u1_altcat_1(sk0),sk1,sk2)),
inference(resolution,[status(thm)],[c136,c2]) ).
cnf(p914,plain,
m1_subset_1(sk3,k1_altcat_1(sk0,sk1,sk2)),
inference(superposition,[status(thm)],[p902,p443]) ).
cnf(p5464,plain,
$false,
inference(resolution,[status(thm)],[p5463,p914]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT359+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n017.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.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 21:15:44 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 76.66/11.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 76.66/11.90 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------