%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT362+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 227.83s 30.36s
% Output : CNFRefutation 228.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 23
% Syntax : Number of formulae : 109 ( 17 unt; 14 def)
% Number of atoms : 373 ( 0 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 380 ( 116 ~; 129 |; 108 &)
% ( 16 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 41 ( 40 usr; 15 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% Number of variables : 50 ( 46 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f451,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7789,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10317,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10318,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10319,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10351,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10352,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10360,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10364,conjecture,
! [A] :
( ~ v2_setfam_1(A)
=> r2_functor0(k4_waybel34(A),k5_waybel34(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10365,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r2_functor0(k4_waybel34(A),k5_waybel34(A)) ),
inference(negated_conjecture,[status(cth)],[f10364]) ).
fof(f11487,plain,
! [A] :
( ~ v1_xboole_0(A)
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f451]) ).
fof(f11488,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f11487]) ).
fof(f35617,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)],[f7789]) ).
fof(f35618,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)],[f35617]) ).
fof(f35619,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(sK2510_skl(B,A),A,B)
& v21_functor0(sK2510_skl(B,A),A,B)
& m2_functor0(sK2510_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,[sK2510_skl]),skolemize(C,sK2510_skl(B,A))],[f35618]) ).
fof(f35623,plain,
! [X0,X1,X2] :
( ~ v2_altcat_1(X0)
| ~ m2_functor0(X1,X0,X2)
| r2_functor0(X0,X2)
| v3_struct_0(X0)
| ~ v21_functor0(X1,X0,X2)
| ~ v2_altcat_1(X2)
| ~ v12_altcat_1(X2)
| v3_struct_0(X2)
| ~ l2_altcat_1(X2)
| ~ v16_functor0(X1,X0,X2)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f35619]) ).
fof(f48637,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)],[f10317]) ).
fof(f48639,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48637]) ).
fof(f48641,plain,
! [X0] :
( v1_xboole_0(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48637]) ).
fof(f48642,plain,
! [X0] :
( v1_xboole_0(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48637]) ).
fof(f48644,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48637]) ).
fof(f48645,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)],[f10318]) ).
fof(f48647,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48645]) ).
fof(f48649,plain,
! [X0] :
( v1_xboole_0(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48645]) ).
fof(f48650,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f48645]) ).
fof(f48652,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48645]) ).
fof(f48653,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)],[f10319]) ).
fof(f48656,plain,
! [X0] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f48653]) ).
fof(f48832,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)],[f10351]) ).
fof(f48833,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f48832]) ).
fof(f48846,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)],[f10352]) ).
fof(f48847,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f48846]) ).
fof(f48920,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)],[f10360]) ).
fof(f48927,plain,
! [X0] :
( v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f48920]) ).
fof(f48928,plain,
! [X0] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[status(thm)],[f48920]) ).
fof(f48944,plain,
? [A] :
( ~ r2_functor0(k4_waybel34(A),k5_waybel34(A))
& ~ v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10365]) ).
fof(f48945,plain,
( ~ r2_functor0(k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
& ~ v2_setfam_1(sK3762_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3762_skl]),skolemize(A,sK3762_skl)],[f48944]) ).
fof(f48946,plain,
~ v2_setfam_1(sK3762_skl),
inference(cnf_transformation,[status(thm)],[f48945]) ).
fof(f48947,plain,
~ r2_functor0(k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)),
inference(cnf_transformation,[status(thm)],[f48945]) ).
fof(f65930,plain,
~ v1_xboole_0(sK3762_skl),
inference(resolution,[status(thm)],[f48946,f11488]) ).
fof(f65931,plain,
~ v3_struct_0(k4_waybel34(sK3762_skl)),
inference(resolution,[status(thm)],[f48833,f48946]) ).
fof(f65933,plain,
~ v3_struct_0(k5_waybel34(sK3762_skl)),
inference(resolution,[status(thm)],[f48847,f48946]) ).
fof(f65939,definition,
( sQ2255_spl
<=> v2_altcat_1(k4_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2255_spl])],[split_symbol_definition]) ).
fof(f65941,plain,
( sQ2255_spl
| ~ v2_altcat_1(k4_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65939]) ).
fof(f65942,definition,
( sQ2256_spl
<=> l2_altcat_1(k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2256_spl])],[split_symbol_definition]) ).
fof(f65944,plain,
( sQ2256_spl
| ~ l2_altcat_1(k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65942]) ).
fof(f65945,definition,
( sQ2257_spl
<=> v3_struct_0(k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2257_spl])],[split_symbol_definition]) ).
fof(f65946,plain,
( ~ sQ2257_spl
| v3_struct_0(k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65945]) ).
fof(f65948,definition,
( sQ2258_spl
<=> l2_altcat_1(k4_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2258_spl])],[split_symbol_definition]) ).
fof(f65950,plain,
( sQ2258_spl
| ~ l2_altcat_1(k4_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65948]) ).
fof(f65951,definition,
( sQ2259_spl
<=> v2_altcat_1(k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2259_spl])],[split_symbol_definition]) ).
fof(f65953,plain,
( sQ2259_spl
| ~ v2_altcat_1(k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65951]) ).
fof(f65954,definition,
( sQ2260_spl
<=> v12_altcat_1(k4_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2260_spl])],[split_symbol_definition]) ).
fof(f65956,plain,
( sQ2260_spl
| ~ v12_altcat_1(k4_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65954]) ).
fof(f65957,definition,
( sQ2261_spl
<=> v3_struct_0(k4_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2261_spl])],[split_symbol_definition]) ).
fof(f65958,plain,
( ~ sQ2261_spl
| v3_struct_0(k4_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65957]) ).
fof(f65963,definition,
( sQ2263_spl
<=> v12_altcat_1(k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2263_spl])],[split_symbol_definition]) ).
fof(f65965,plain,
( sQ2263_spl
| ~ v12_altcat_1(k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65963]) ).
fof(f65972,definition,
( sQ2265_spl
<=> v11_altcat_1(k4_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2265_spl])],[split_symbol_definition]) ).
fof(f65974,plain,
( sQ2265_spl
| ~ v11_altcat_1(k4_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65972]) ).
fof(f65982,definition,
( sQ2267_spl
<=> v11_altcat_1(k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2267_spl])],[split_symbol_definition]) ).
fof(f65984,plain,
( sQ2267_spl
| ~ v11_altcat_1(k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65982]) ).
fof(f65994,plain,
! [X0] :
( ~ v2_altcat_1(k4_waybel34(sK3762_skl))
| ~ m2_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| v3_struct_0(k4_waybel34(sK3762_skl))
| ~ v21_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v2_altcat_1(k5_waybel34(sK3762_skl))
| ~ v12_altcat_1(k5_waybel34(sK3762_skl))
| v3_struct_0(k5_waybel34(sK3762_skl))
| ~ l2_altcat_1(k5_waybel34(sK3762_skl))
| ~ v16_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v12_altcat_1(k4_waybel34(sK3762_skl))
| ~ l2_altcat_1(k4_waybel34(sK3762_skl)) ),
inference(resolution,[status(thm)],[f35623,f48947]) ).
fof(f65995,definition,
! [X0] :
( sQ2270_spl
<=> ( ~ m2_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v21_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v16_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2270_spl])],[split_symbol_definition]) ).
fof(f65996,plain,
! [X0] :
( ~ sQ2270_spl
| ~ m2_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v16_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v21_functor0(X0,k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f65995]) ).
fof(f65998,plain,
( ~ sQ2255_spl
| sQ2261_spl
| ~ sQ2259_spl
| ~ sQ2263_spl
| sQ2257_spl
| ~ sQ2256_spl
| sQ2270_spl
| ~ sQ2260_spl
| ~ sQ2258_spl ),
inference(split_clause,[status(thm)],[f65994,f65948,f65954,f65995,f65942,f65945,f65963,f65951,f65957,f65939]) ).
fof(f66054,definition,
( sQ2283_spl
<=> v2_setfam_1(sK3762_skl) ),
introduced(definition,[new_symbols(definition,[sQ2283_spl])],[split_symbol_definition]) ).
fof(f66055,plain,
( ~ sQ2283_spl
| v2_setfam_1(sK3762_skl) ),
inference(component_clause,[status(thm)],[f66054]) ).
fof(f66071,plain,
( ~ sQ2283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66055,f48946]) ).
fof(f66072,plain,
~ sQ2283_spl,
inference(contradiction_clause,[status(thm)],[f66071]) ).
fof(f66126,plain,
( ~ sQ2261_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f65958,f65931]) ).
fof(f66127,plain,
~ sQ2261_spl,
inference(contradiction_clause,[status(thm)],[f66126]) ).
fof(f66131,plain,
( sQ2258_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65950,f48644]) ).
fof(f66132,plain,
( sQ2258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66131,f65930]) ).
fof(f66133,plain,
sQ2258_spl,
inference(contradiction_clause,[status(thm)],[f66132]) ).
fof(f66135,plain,
( sQ2263_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65965,f48650]) ).
fof(f66138,plain,
( sQ2263_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66135,f65930]) ).
fof(f66139,plain,
sQ2263_spl,
inference(contradiction_clause,[status(thm)],[f66138]) ).
fof(f66141,plain,
( ~ sQ2257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f65946,f65933]) ).
fof(f66142,plain,
~ sQ2257_spl,
inference(contradiction_clause,[status(thm)],[f66141]) ).
fof(f66188,plain,
( sQ2256_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65944,f48652]) ).
fof(f66189,plain,
( sQ2256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66188,f65930]) ).
fof(f66190,plain,
sQ2256_spl,
inference(contradiction_clause,[status(thm)],[f66189]) ).
fof(f66282,plain,
( sQ2259_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65953,f48647]) ).
fof(f66285,plain,
( sQ2259_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66282,f65930]) ).
fof(f66286,plain,
sQ2259_spl,
inference(contradiction_clause,[status(thm)],[f66285]) ).
fof(f66298,plain,
( sQ2260_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65956,f48642]) ).
fof(f66301,plain,
( sQ2260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66298,f65930]) ).
fof(f66302,plain,
sQ2260_spl,
inference(contradiction_clause,[status(thm)],[f66301]) ).
fof(f66303,plain,
( sQ2255_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65941,f48639]) ).
fof(f66306,plain,
( sQ2255_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66303,f65930]) ).
fof(f66307,plain,
sQ2255_spl,
inference(contradiction_clause,[status(thm)],[f66306]) ).
fof(f66352,plain,
( sQ2267_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65984,f48649]) ).
fof(f66355,plain,
( sQ2267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66352,f65930]) ).
fof(f66356,plain,
sQ2267_spl,
inference(contradiction_clause,[status(thm)],[f66355]) ).
fof(f66407,plain,
( sQ2265_spl
| v1_xboole_0(sK3762_skl) ),
inference(resolution,[status(thm)],[f65974,f48641]) ).
fof(f66409,plain,
( sQ2265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66407,f65930]) ).
fof(f66410,plain,
sQ2265_spl,
inference(contradiction_clause,[status(thm)],[f66409]) ).
fof(f66472,plain,
( ~ sQ2270_spl
| ~ v16_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| ~ v21_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl))
| v2_setfam_1(sK3762_skl) ),
inference(resolution,[status(thm)],[f48656,f65996]) ).
fof(f66473,definition,
( sQ2328_spl
<=> v21_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2328_spl])],[split_symbol_definition]) ).
fof(f66475,plain,
( sQ2328_spl
| ~ v21_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f66473]) ).
fof(f66476,definition,
( sQ2329_spl
<=> v16_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2329_spl])],[split_symbol_definition]) ).
fof(f66478,plain,
( sQ2329_spl
| ~ v16_functor0(k6_waybel34(sK3762_skl),k4_waybel34(sK3762_skl),k5_waybel34(sK3762_skl)) ),
inference(component_clause,[status(thm)],[f66476]) ).
fof(f66479,plain,
( ~ sQ2270_spl
| ~ sQ2329_spl
| ~ sQ2328_spl
| sQ2283_spl ),
inference(split_clause,[status(thm)],[f66472,f66054,f66473,f66476,f65995]) ).
fof(f66953,plain,
( sQ2329_spl
| v2_setfam_1(sK3762_skl) ),
inference(resolution,[status(thm)],[f66478,f48927]) ).
fof(f66954,plain,
( sQ2329_spl
| sQ2283_spl ),
inference(split_clause,[status(thm)],[f66953,f66054,f66476]) ).
fof(f67401,plain,
( sQ2328_spl
| v2_setfam_1(sK3762_skl) ),
inference(resolution,[status(thm)],[f66475,f48928]) ).
fof(f67402,plain,
( sQ2328_spl
| sQ2283_spl ),
inference(split_clause,[status(thm)],[f67401,f66054,f66473]) ).
fof(f67403,plain,
$false,
inference(sat_refutation,[status(thm)],[f65998,f66072,f66127,f66133,f66139,f66142,f66190,f66286,f66302,f66307,f66356,f66410,f66479,f66954,f67402]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT362+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 23:49:56 UTC 2026
% 0.09/0.35 % CPUTime :
% 1.55/1.81 % Drodi V4.1.1
% 227.83/30.36 % Refutation found
% 227.83/30.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 227.83/30.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 35.60/30.59 % Elapsed time: 30.218895 seconds
% 35.60/30.59 % CPU time: 228.995157 seconds
% 35.60/30.59 % Total memory used: 3.292 GB
% 35.60/30.59 % Net memory used: 3.203 GB
%------------------------------------------------------------------------------