%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT377+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 : n016.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:03:01 PM UTC 2026
% Result : Theorem 5.21s 1.67s
% Output : CNFRefutation 5.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 37
% Syntax : Number of formulae : 221 ( 4 unt; 21 def)
% Number of atoms : 1266 ( 5 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1656 ( 611 ~; 838 |; 161 &)
% ( 21 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 52 ( 50 usr; 22 prp; 0-5 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-3 aty)
% Number of variables : 179 ( 178 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k11_waybel34(A),k10_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k11_waybel34(A),k10_waybel34(A)) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f29,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m1_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v3_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v2_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v6_altcat_1(k10_waybel34(A))
& v2_altcat_1(k10_waybel34(A))
& ~ v3_struct_0(k10_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m1_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v3_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v2_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v6_altcat_1(k11_waybel34(A))
& v2_altcat_1(k11_waybel34(A))
& ~ v3_struct_0(k11_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,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(f54,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(f55,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(f57,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( m1_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v6_altcat_1(k8_waybel34(A))
& v2_altcat_1(k8_waybel34(A))
& ~ v3_struct_0(k8_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m1_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v6_altcat_1(k9_waybel34(A))
& v2_altcat_1(k9_waybel34(A))
& ~ v3_struct_0(k9_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,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(f96,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(f98,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(f122,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A)
& k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [A] :
( ( l2_altcat_1(A)
& v12_altcat_1(A)
& v11_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_altcat_2(B,A)
& v3_altcat_2(B,A)
& v2_altcat_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m1_altcat_2(C,B)
& v3_altcat_2(C,B)
& v2_altcat_1(C)
& ~ v3_struct_0(C) )
=> ( m1_altcat_2(C,A)
& v3_altcat_2(C,A)
& v2_altcat_1(C)
& ~ v3_struct_0(C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [A] :
( ( l2_altcat_1(A)
& v12_altcat_1(A)
& v11_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l2_altcat_1(B)
& v12_altcat_1(B)
& v11_altcat_1(B)
& v2_altcat_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_functor0(C,A,B)
& v16_functor0(C,A,B) )
=> ( v21_functor0(C,A,B)
=> ! [D] :
( ( m1_altcat_2(D,A)
& v3_altcat_2(D,A)
& v2_altcat_1(D)
& ~ v3_struct_0(D) )
=> ! [E] :
( ( m1_altcat_2(E,B)
& v3_altcat_2(E,B)
& v2_altcat_1(E)
& ~ v3_struct_0(E) )
=> ( r3_yellow20(A,B,C,D,E)
=> r3_yellow20(B,A,k15_functor0(A,B,C),E,D) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k10_waybel34(A),k11_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,plain,
? [A] :
( ~ r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k11_waybel34(A),k10_waybel34(A))
& ~ v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f135,plain,
( ~ r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k11_waybel34(sK0_skl),k10_waybel34(sK0_skl))
& ~ v2_setfam_1(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f134]) ).
fof(f136,plain,
~ v2_setfam_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
~ r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k11_waybel34(sK0_skl),k10_waybel34(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f236,plain,
! [A] :
( ~ v1_xboole_0(A)
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f237,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f316,plain,
! [A] :
( ( m1_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v3_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v2_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v6_altcat_1(k10_waybel34(A))
& v2_altcat_1(k10_waybel34(A))
& ~ v3_struct_0(k10_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f317,plain,
! [X0] :
( ~ v3_struct_0(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [X0] :
( v2_altcat_1(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f321,plain,
! [X0] :
( v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f322,plain,
! [X0] :
( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f323,plain,
! [A] :
( ( m1_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v3_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v2_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v6_altcat_1(k11_waybel34(A))
& v2_altcat_1(k11_waybel34(A))
& ~ v3_struct_0(k11_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f324,plain,
! [X0] :
( ~ v3_struct_0(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f325,plain,
! [X0] :
( v2_altcat_1(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f328,plain,
! [X0] :
( v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f329,plain,
! [X0] :
( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f337,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)],[f53]) ).
fof(f344,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f345,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)],[f54]) ).
fof(f352,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f353,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)],[f55]) ).
fof(f355,plain,
! [X0] :
( v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f356,plain,
! [X0] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f361,plain,
! [A] :
( ( m1_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v6_altcat_1(k8_waybel34(A))
& v2_altcat_1(k8_waybel34(A))
& ~ v3_struct_0(k8_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f362,plain,
! [X0] :
( ~ v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f363,plain,
! [X0] :
( v2_altcat_1(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f365,plain,
! [X0] :
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f366,plain,
! [X0] :
( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f367,plain,
! [A] :
( ( m1_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v6_altcat_1(k9_waybel34(A))
& v2_altcat_1(k9_waybel34(A))
& ~ v3_struct_0(k9_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f368,plain,
! [X0] :
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f369,plain,
! [X0] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f371,plain,
! [X0] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f372,plain,
! [X0] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f457,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)],[f94]) ).
fof(f458,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f462,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f463,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f477,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)],[f96]) ).
fof(f478,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f479,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f482,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f483,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f495,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)],[f98]) ).
fof(f503,plain,
! [X0] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f495]) ).
fof(f622,plain,
! [A] :
( ( k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A)
& k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f122]) ).
fof(f623,plain,
! [X0] :
( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f622]) ).
fof(f629,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( m1_altcat_2(C,A)
& v3_altcat_2(C,A)
& v2_altcat_1(C)
& ~ v3_struct_0(C) )
| ~ m1_altcat_2(C,B)
| ~ v3_altcat_2(C,B)
| ~ v2_altcat_1(C)
| v3_struct_0(C) )
| ~ m1_altcat_2(B,A)
| ~ v3_altcat_2(B,A)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v11_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f125]) ).
fof(f632,plain,
! [X0,X1,X2] :
( v3_altcat_2(X2,X0)
| ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f629]) ).
fof(f633,plain,
! [X0,X1,X2] :
( m1_altcat_2(X2,X0)
| ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f629]) ).
fof(f641,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( r3_yellow20(B,A,k15_functor0(A,B,C),E,D)
| ~ r3_yellow20(A,B,C,D,E)
| ~ m1_altcat_2(E,B)
| ~ v3_altcat_2(E,B)
| ~ v2_altcat_1(E)
| v3_struct_0(E) )
| ~ m1_altcat_2(D,A)
| ~ v3_altcat_2(D,A)
| ~ v2_altcat_1(D)
| v3_struct_0(D) )
| ~ v21_functor0(C,A,B)
| ~ m2_functor0(C,A,B)
| ~ v16_functor0(C,A,B) )
| ~ l2_altcat_1(B)
| ~ v12_altcat_1(B)
| ~ v11_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v11_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f128]) ).
fof(f642,plain,
! [X0,X1,X2,X3,X4] :
( r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| ~ r3_yellow20(X0,X1,X2,X3,X4)
| ~ m1_altcat_2(X4,X1)
| ~ v3_altcat_2(X4,X1)
| ~ v2_altcat_1(X4)
| v3_struct_0(X4)
| ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| v3_struct_0(X3)
| ~ v21_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f643,plain,
! [A] :
( r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k10_waybel34(A),k11_waybel34(A))
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f129]) ).
fof(f644,plain,
! [X0] :
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f643]) ).
fof(f3635,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ v2_altcat_1(k10_waybel34(X1))
| v3_struct_0(k10_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f632,f321]) ).
fof(f3636,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v2_altcat_1(k9_waybel34(X1))
| v3_struct_0(k9_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f632,f328]) ).
fof(f3641,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3635,f317]) ).
fof(f3642,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v2_altcat_1(k9_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3636,f368]) ).
fof(f3760,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ v2_altcat_1(k10_waybel34(X1))
| v3_struct_0(k10_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f633,f321]) ).
fof(f3761,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v2_altcat_1(k9_waybel34(X1))
| v3_struct_0(k9_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f633,f328]) ).
fof(f3766,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3760,f317]) ).
fof(f3767,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v2_altcat_1(k9_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3761,f368]) ).
fof(f3769,plain,
! [X0,X1,X2] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),X2,X1)
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2)
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0)) ),
inference(paramodulation,[status(thm)],[f623,f642]) ).
fof(f3771,plain,
! [X0,X1,X2] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),X2,X1)
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2)
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3769,f458]) ).
fof(f3779,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3641,f318]) ).
fof(f3780,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v2_setfam_1(X1)
| v3_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f3779,f322]) ).
fof(f3781,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3780]) ).
fof(f3782,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3781,f365]) ).
fof(f3783,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3782,f458]) ).
fof(f3784,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3783,f459]) ).
fof(f3785,plain,
! [X0] :
( v1_xboole_0(X0)
| v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3784,f366]) ).
fof(f3786,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3785]) ).
fof(f3787,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3786,f462]) ).
fof(f3788,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3642,f369]) ).
fof(f3789,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f3788,f329]) ).
fof(f3790,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3789]) ).
fof(f3791,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3790,f324]) ).
fof(f3792,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3787,f463]) ).
fof(f3859,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v3_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3791,f325]) ).
fof(f3860,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3859,f371]) ).
fof(f3861,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3860]) ).
fof(f3862,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3861,f478]) ).
fof(f3863,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3862,f479]) ).
fof(f3864,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3863,f372]) ).
fof(f3865,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3864]) ).
fof(f3866,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3865,f482]) ).
fof(f3867,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3866,f483]) ).
fof(f3944,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3766,f318]) ).
fof(f3945,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v2_setfam_1(X1)
| m1_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f3944,f322]) ).
fof(f3946,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k10_waybel34(X1),X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(k8_waybel34(X1))
| v3_struct_0(k8_waybel34(X1))
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3945]) ).
fof(f3947,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3946,f365]) ).
fof(f3948,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3947,f458]) ).
fof(f3949,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3948,f459]) ).
fof(f3950,plain,
! [X0] :
( v1_xboole_0(X0)
| v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(resolution,[status(thm)],[f3949,f366]) ).
fof(f3951,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3950]) ).
fof(f3952,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3951,f462]) ).
fof(f3953,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| v3_struct_0(k8_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3952,f463]) ).
fof(f3960,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3767,f369]) ).
fof(f3961,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f3960,f329]) ).
fof(f3962,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| v3_struct_0(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3961]) ).
fof(f3963,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3962,f324]) ).
fof(f4063,plain,
! [X0,X1] :
( v2_setfam_1(X1)
| m1_altcat_2(k11_waybel34(X1),X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3963,f325]) ).
fof(f4064,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0)) ),
inference(resolution,[status(thm)],[f4063,f371]) ).
fof(f4065,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4064]) ).
fof(f4066,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4065,f478]) ).
fof(f4067,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4066,f479]) ).
fof(f4068,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(resolution,[status(thm)],[f4067,f372]) ).
fof(f4069,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4068]) ).
fof(f4070,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4069,f482]) ).
fof(f4071,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4070,f483]) ).
fof(f4087,plain,
! [X0,X1,X2] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),X2,X1)
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2)
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3771,f459]) ).
fof(f4088,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0))
| ~ m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v2_altcat_1(k11_waybel34(X0))
| v3_struct_0(k11_waybel34(X0))
| ~ m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k10_waybel34(X0))
| v3_struct_0(k10_waybel34(X0))
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(resolution,[status(thm)],[f4087,f644]) ).
fof(f4089,plain,
! [X0] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0))
| ~ m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v2_altcat_1(k11_waybel34(X0))
| v3_struct_0(k11_waybel34(X0))
| ~ m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k10_waybel34(X0))
| v3_struct_0(k10_waybel34(X0))
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f4088]) ).
fof(f4090,plain,
! [X0] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0))
| ~ m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v2_altcat_1(k11_waybel34(X0))
| v3_struct_0(k11_waybel34(X0))
| ~ m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k10_waybel34(X0))
| v3_struct_0(k10_waybel34(X0))
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4089,f462]) ).
fof(f4102,plain,
! [X0] :
( v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0))
| ~ m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| ~ v2_altcat_1(k11_waybel34(X0))
| v3_struct_0(k11_waybel34(X0))
| ~ m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| ~ v2_altcat_1(k10_waybel34(X0))
| v3_struct_0(k10_waybel34(X0))
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4090,f463]) ).
fof(f4103,plain,
( v2_setfam_1(sK0_skl)
| ~ m1_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v3_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k11_waybel34(sK0_skl))
| v3_struct_0(k11_waybel34(sK0_skl))
| ~ m1_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v3_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k10_waybel34(sK0_skl))
| v3_struct_0(k10_waybel34(sK0_skl))
| ~ 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))
| ~ v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v11_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)) ),
inference(resolution,[status(thm)],[f4102,f137]) ).
fof(f4105,definition,
( sQ25_spl
<=> l2_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f4107,plain,
( sQ25_spl
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4105]) ).
fof(f4108,definition,
( sQ26_spl
<=> v3_struct_0(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f4109,plain,
( ~ sQ26_spl
| v3_struct_0(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4108]) ).
fof(f4111,definition,
( sQ27_spl
<=> v2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f4113,plain,
( sQ27_spl
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4111]) ).
fof(f4114,definition,
( sQ28_spl
<=> v11_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f4116,plain,
( sQ28_spl
| ~ v11_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4114]) ).
fof(f4117,definition,
( sQ29_spl
<=> v12_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f4119,plain,
( sQ29_spl
| ~ v12_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4117]) ).
fof(f4120,definition,
( sQ30_spl
<=> l2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f4122,plain,
( sQ30_spl
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4120]) ).
fof(f4123,definition,
( sQ31_spl
<=> v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f4125,plain,
( sQ31_spl
| ~ v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4123]) ).
fof(f4126,definition,
( sQ32_spl
<=> m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f4128,plain,
( sQ32_spl
| ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4126]) ).
fof(f4129,definition,
( sQ33_spl
<=> v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f4131,plain,
( sQ33_spl
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4129]) ).
fof(f4132,definition,
( sQ34_spl
<=> v3_struct_0(k10_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f4133,plain,
( ~ sQ34_spl
| v3_struct_0(k10_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4132]) ).
fof(f4135,definition,
( sQ35_spl
<=> v2_altcat_1(k10_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f4137,plain,
( sQ35_spl
| ~ v2_altcat_1(k10_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4135]) ).
fof(f4138,definition,
( sQ36_spl
<=> v3_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f4140,plain,
( sQ36_spl
| ~ v3_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4138]) ).
fof(f4141,definition,
( sQ37_spl
<=> m1_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f4143,plain,
( sQ37_spl
| ~ m1_altcat_2(k10_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4141]) ).
fof(f4144,definition,
( sQ38_spl
<=> v3_struct_0(k11_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f4145,plain,
( ~ sQ38_spl
| v3_struct_0(k11_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4144]) ).
fof(f4147,definition,
( sQ39_spl
<=> v2_altcat_1(k11_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f4149,plain,
( sQ39_spl
| ~ v2_altcat_1(k11_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4147]) ).
fof(f4150,definition,
( sQ40_spl
<=> v3_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f4152,plain,
( sQ40_spl
| ~ v3_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4150]) ).
fof(f4153,definition,
( sQ41_spl
<=> m1_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f4155,plain,
( sQ41_spl
| ~ m1_altcat_2(k11_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4153]) ).
fof(f4156,definition,
( sQ42_spl
<=> v2_setfam_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f4157,plain,
( ~ sQ42_spl
| v2_setfam_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f4156]) ).
fof(f4159,plain,
( sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| sQ26_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f4103,f4105,f4108,f4111,f4114,f4117,f4120,f4123,f4126,f4129,f4132,f4135,f4138,f4141,f4144,f4147,f4150,f4153,f4156]) ).
fof(f4161,plain,
( ~ sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4157,f136]) ).
fof(f4162,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f4161]) ).
fof(f4163,plain,
( sQ39_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4149,f325]) ).
fof(f4164,plain,
( sQ39_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4163,f4156,f4147]) ).
fof(f4165,plain,
( ~ sQ38_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4145,f324]) ).
fof(f4166,plain,
( ~ sQ38_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4165,f4156,f4144]) ).
fof(f4167,plain,
( sQ35_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4137,f318]) ).
fof(f4168,plain,
( sQ35_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4167,f4156,f4135]) ).
fof(f4169,plain,
( ~ sQ34_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4133,f317]) ).
fof(f4170,plain,
( ~ sQ34_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4169,f4156,f4132]) ).
fof(f4171,plain,
( sQ30_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f4122,f352]) ).
fof(f4174,plain,
( sQ30_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4171,f237]) ).
fof(f4182,plain,
( sQ30_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4174,f4156,f4120]) ).
fof(f4183,plain,
( sQ41_spl
| v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f4155,f4071]) ).
fof(f4184,plain,
( sQ41_spl
| sQ42_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f4183,f4120,f4156,f4153]) ).
fof(f4185,plain,
( sQ40_spl
| v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f4152,f3867]) ).
fof(f4186,plain,
( sQ40_spl
| sQ42_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f4185,f4120,f4156,f4150]) ).
fof(f4187,plain,
( sQ29_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4119,f483]) ).
fof(f4189,plain,
( sQ29_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4187,f4156,f4117]) ).
fof(f4190,plain,
( sQ28_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4116,f482]) ).
fof(f4192,plain,
( sQ28_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4190,f4156,f4114]) ).
fof(f4193,plain,
( sQ27_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4113,f479]) ).
fof(f4195,plain,
( sQ27_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4193,f4156,f4111]) ).
fof(f4196,plain,
( ~ sQ26_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4109,f478]) ).
fof(f4198,plain,
( ~ sQ26_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4196,f4156,f4108]) ).
fof(f4199,plain,
( sQ25_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f4107,f344]) ).
fof(f4202,plain,
( sQ25_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4199,f237]) ).
fof(f4210,plain,
( sQ25_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4202,f4156,f4105]) ).
fof(f4262,definition,
( sQ51_spl
<=> v3_struct_0(k8_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f4263,plain,
( ~ sQ51_spl
| v3_struct_0(k8_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4262]) ).
fof(f4265,definition,
( sQ52_spl
<=> v2_altcat_1(k8_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f4267,plain,
( sQ52_spl
| ~ v2_altcat_1(k8_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f4265]) ).
fof(f4323,plain,
( sQ37_spl
| v1_xboole_0(sK0_skl)
| v2_setfam_1(sK0_skl)
| ~ v2_altcat_1(k8_waybel34(sK0_skl))
| v3_struct_0(k8_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f4143,f3953]) ).
fof(f4324,definition,
( sQ66_spl
<=> v1_xboole_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f4325,plain,
( ~ sQ66_spl
| v1_xboole_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f4324]) ).
fof(f4327,plain,
( sQ37_spl
| sQ66_spl
| sQ42_spl
| ~ sQ52_spl
| sQ51_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f4323,f4105,f4262,f4265,f4156,f4324,f4141]) ).
fof(f4330,plain,
( ~ sQ66_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4325,f237]) ).
fof(f4338,plain,
( ~ sQ66_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4330,f4156,f4324]) ).
fof(f4340,plain,
( sQ52_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f4267,f363]) ).
fof(f4341,plain,
( sQ52_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f4340,f4324,f4265]) ).
fof(f4342,plain,
( ~ sQ51_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f4263,f362]) ).
fof(f4343,plain,
( ~ sQ51_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f4342,f4324,f4262]) ).
fof(f4352,plain,
( sQ36_spl
| v1_xboole_0(sK0_skl)
| v2_setfam_1(sK0_skl)
| ~ v2_altcat_1(k8_waybel34(sK0_skl))
| v3_struct_0(k8_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f4140,f3792]) ).
fof(f4353,plain,
( sQ36_spl
| sQ66_spl
| sQ42_spl
| ~ sQ52_spl
| sQ51_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f4352,f4105,f4262,f4265,f4156,f4324,f4138]) ).
fof(f4354,plain,
( sQ33_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4131,f503]) ).
fof(f4355,plain,
( sQ33_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4354,f4156,f4129]) ).
fof(f4471,plain,
( sQ32_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4128,f356]) ).
fof(f4472,plain,
( sQ32_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4471,f4156,f4126]) ).
fof(f4696,plain,
( sQ31_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f4125,f355]) ).
fof(f4697,plain,
( sQ31_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f4696,f4156,f4123]) ).
fof(f4698,plain,
$false,
inference(sat_refutation,[status(thm)],[f4159,f4162,f4164,f4166,f4168,f4170,f4182,f4184,f4186,f4189,f4192,f4195,f4198,f4210,f4327,f4338,f4341,f4343,f4353,f4355,f4472,f4697]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT377+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n016.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 00:00:23 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 5.21/1.67 % Refutation found
% 5.21/1.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.21/1.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.79/1.74 % Elapsed time: 1.262217 seconds
% 0.79/1.74 % CPU time: 9.405627 seconds
% 0.79/1.74 % Total memory used: 194.104 MB
% 0.79/1.74 % Net memory used: 190.562 MB
%------------------------------------------------------------------------------