%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT362+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 01:02:57 PM UTC 2026
% Result : Theorem 0.09s 0.42s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 20
% Syntax : Number of formulae : 97 ( 15 unt; 11 def)
% Number of atoms : 345 ( 0 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 349 ( 101 ~; 116 |; 108 &)
% ( 13 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 12 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% Number of variables : 45 ( 41 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ~ v2_setfam_1(A)
=> r2_functor0(k4_waybel34(A),k5_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r2_functor0(k4_waybel34(A),k5_waybel34(A)) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f28,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( ( l2_altcat_1(A)
& v12_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l2_altcat_1(B)
& v12_altcat_1(B)
& v2_altcat_1(B)
& ~ v3_struct_0(B) )
=> ( r2_functor0(A,B)
<=> ? [C] :
( v16_functor0(C,A,B)
& v21_functor0(C,A,B)
& m2_functor0(C,A,B) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( l2_altcat_1(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( l2_altcat_1(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v3_yellow21(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v1_yellow21(k4_waybel34(A))
& v4_yellow18(k4_waybel34(A))
& v3_yellow18(k4_waybel34(A))
& v2_yellow18(k4_waybel34(A))
& v1_altcat_2(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v9_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v3_yellow21(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v1_yellow21(k5_waybel34(A))
& v4_yellow18(k5_waybel34(A))
& v3_yellow18(k5_waybel34(A))
& v2_yellow18(k5_waybel34(A))
& v1_altcat_2(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v9_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,plain,
? [A] :
( ~ r2_functor0(k4_waybel34(A),k5_waybel34(A))
& ~ v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f116,plain,
( ~ r2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
& ~ v2_setfam_1(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f115]) ).
fof(f117,plain,
~ v2_setfam_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
~ r2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f203,plain,
! [A] :
( ~ v1_xboole_0(A)
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f204,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f235,plain,
! [A] :
( ! [B] :
( ( r2_functor0(A,B)
<=> ? [C] :
( v16_functor0(C,A,B)
& v21_functor0(C,A,B)
& m2_functor0(C,A,B) ) )
| ~ l2_altcat_1(B)
| ~ v12_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f236,plain,
! [A] :
( ! [B] :
( ( ( ! [C] :
( ~ v16_functor0(C,A,B)
| ~ v21_functor0(C,A,B)
| ~ m2_functor0(C,A,B) )
| r2_functor0(A,B) )
& ( ? [C] :
( v16_functor0(C,A,B)
& v21_functor0(C,A,B)
& m2_functor0(C,A,B) )
| ~ r2_functor0(A,B) ) )
| ~ l2_altcat_1(B)
| ~ v12_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f235]) ).
fof(f237,plain,
! [A] :
( ! [B] :
( ( ( ! [C] :
( ~ v16_functor0(C,A,B)
| ~ v21_functor0(C,A,B)
| ~ m2_functor0(C,A,B) )
| r2_functor0(A,B) )
& ( ( v16_functor0(sK1_skl(B,A),A,B)
& v21_functor0(sK1_skl(B,A),A,B)
& m2_functor0(sK1_skl(B,A),A,B) )
| ~ r2_functor0(A,B) ) )
| ~ l2_altcat_1(B)
| ~ v12_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f236]) ).
fof(f241,plain,
! [X0,X1,X2] :
( ~ v16_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| r2_functor0(X0,X1)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f252,plain,
! [A] :
( ( l2_altcat_1(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f259,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f260,plain,
! [A] :
( ( l2_altcat_1(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f267,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f268,plain,
! [A] :
( ( m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f270,plain,
! [X0] :
( v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f271,plain,
! [X0] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f335,plain,
! [A] :
( ( v3_yellow21(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v1_yellow21(k4_waybel34(A))
& v4_yellow18(k4_waybel34(A))
& v3_yellow18(k4_waybel34(A))
& v2_yellow18(k4_waybel34(A))
& v1_altcat_2(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v9_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f80]) ).
fof(f336,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f337,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f341,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f355,plain,
! [A] :
( ( v3_yellow21(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v1_yellow21(k5_waybel34(A))
& v4_yellow18(k5_waybel34(A))
& v3_yellow18(k5_waybel34(A))
& v2_yellow18(k5_waybel34(A))
& v1_altcat_2(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v9_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f356,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f357,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f361,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f373,plain,
! [A] :
( ( v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f381,plain,
! [X0] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f592,plain,
v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)),
inference(resolution,[status(thm)],[f270,f117]) ).
fof(f594,plain,
( ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| r2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f592,f241]) ).
fof(f598,definition,
( sQ19_spl
<=> v3_struct_0(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ19_spl
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f601,definition,
( sQ20_spl
<=> v2_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( sQ20_spl
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,definition,
( sQ21_spl
<=> v12_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( sQ21_spl
| ~ v12_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f607,definition,
( sQ22_spl
<=> l2_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( sQ22_spl
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f610,definition,
( sQ23_spl
<=> v3_struct_0(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( ~ sQ23_spl
| v3_struct_0(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,definition,
( sQ24_spl
<=> v2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( sQ24_spl
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f613]) ).
fof(f616,definition,
( sQ25_spl
<=> v12_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f618,plain,
( sQ25_spl
| ~ v12_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f619,definition,
( sQ26_spl
<=> l2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( sQ26_spl
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f619]) ).
fof(f622,definition,
( sQ27_spl
<=> r2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( ~ sQ27_spl
| r2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f622]) ).
fof(f625,definition,
( sQ28_spl
<=> m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( sQ28_spl
| ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f628,definition,
( sQ29_spl
<=> v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ29_spl
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f631,plain,
( ~ sQ29_spl
| ~ sQ28_spl
| sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f594,f598,f601,f604,f607,f610,f613,f616,f619,f622,f625,f628]) ).
fof(f644,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f118]) ).
fof(f645,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f644]) ).
fof(f646,plain,
( sQ28_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f627,f271]) ).
fof(f647,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f117]) ).
fof(f648,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f647]) ).
fof(f649,plain,
( sQ26_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f621,f267]) ).
fof(f650,plain,
( sQ26_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f649,f204]) ).
fof(f651,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f117]) ).
fof(f652,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f651]) ).
fof(f655,plain,
( sQ25_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f618,f361]) ).
fof(f657,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f655,f117]) ).
fof(f658,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f657]) ).
fof(f659,plain,
( ~ sQ23_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f611,f356]) ).
fof(f661,plain,
( ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f659,f117]) ).
fof(f662,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f661]) ).
fof(f663,plain,
( sQ22_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f609,f259]) ).
fof(f666,plain,
( sQ22_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f663,f204]) ).
fof(f667,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f666,f117]) ).
fof(f668,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f667]) ).
fof(f669,plain,
( sQ21_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f606,f341]) ).
fof(f671,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f117]) ).
fof(f672,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f671]) ).
fof(f673,plain,
( sQ20_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f603,f337]) ).
fof(f675,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f117]) ).
fof(f676,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f677,plain,
( ~ sQ19_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f599,f336]) ).
fof(f679,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f117]) ).
fof(f680,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f679]) ).
fof(f688,plain,
( sQ24_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f615,f357]) ).
fof(f690,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f117]) ).
fof(f691,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f690]) ).
fof(f1034,plain,
( sQ29_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f381,f630]) ).
fof(f1035,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1034,f117]) ).
fof(f1036,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1035]) ).
fof(f1037,plain,
$false,
inference(sat_refutation,[status(thm)],[f631,f645,f648,f652,f658,f662,f668,f672,f676,f680,f691,f1036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT362+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.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 23:50:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.42 % Refutation found
% 0.09/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.44 % Elapsed time: 0.074323 seconds
% 0.09/0.44 % CPU time: 0.237618 seconds
% 0.09/0.44 % Total memory used: 94.031 MB
% 0.09/0.44 % Net memory used: 93.830 MB
%------------------------------------------------------------------------------