%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT361+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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:02:56 PM UTC 2026
% Result : Theorem 1.67s 0.87s
% Output : CNFRefutation 1.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 104
% Number of leaves : 18
% Syntax : Number of formulae : 187 ( 10 unt; 0 def)
% Number of atoms : 1197 ( 151 equ)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 1848 ( 838 ~; 833 |; 149 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-5 aty)
% Number of variables : 119 ( 118 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ~ v2_setfam_1(A)
=> ( k13_functor0(k4_waybel34(A),k5_waybel34(A),k4_waybel34(A),k6_waybel34(A),k7_waybel34(A)) = k12_functor0(k4_waybel34(A))
& k13_functor0(k5_waybel34(A),k4_waybel34(A),k5_waybel34(A),k7_waybel34(A),k6_waybel34(A)) = k12_functor0(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> ( k13_functor0(k4_waybel34(A),k5_waybel34(A),k4_waybel34(A),k6_waybel34(A),k7_waybel34(A)) = k12_functor0(k4_waybel34(A))
& k13_functor0(k5_waybel34(A),k4_waybel34(A),k5_waybel34(A),k7_waybel34(A),k6_waybel34(A)) = k12_functor0(k5_waybel34(A)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f4,axiom,
! [A,B,C] :
( ( l2_functor0(C,A,B)
& l1_altcat_1(B)
& l1_altcat_1(A) )
=> ( v9_functor0(C,A,B)
=> C = g2_functor0(A,B,u1_functor0(A,B,C),u2_functor0(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B] :
( ( l2_altcat_1(B)
& v12_altcat_1(B)
& ~ v3_struct_0(B)
& l2_altcat_1(A)
& v12_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m2_functor0(C,A,B)
=> ( v12_functor0(C,A,B)
& v8_functor0(C,A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( l2_altcat_1(A)
=> ( ( v12_altcat_1(A)
& ~ v3_struct_0(A) )
=> ( v1_altcat_2(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,B,C] :
( ( l2_functor0(C,A,B)
& l1_altcat_1(B)
& ~ v3_struct_0(B)
& l1_altcat_1(A)
& ~ v3_struct_0(A) )
=> ( l2_functor0(k15_functor0(A,B,C),B,A)
& v9_functor0(k15_functor0(A,B,C),B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,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(f53,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(f54,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(f55,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m2_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v16_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v9_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( l2_altcat_1(A)
=> l1_altcat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [A,B] :
( ( l2_altcat_1(B)
& v12_altcat_1(B)
& ~ v3_struct_0(B)
& l2_altcat_1(A)
& v12_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [C] :
( m2_functor0(C,A,B)
=> l2_functor0(C,A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,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(f99,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(f101,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(f102,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v21_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v16_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v14_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v12_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v11_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v9_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v8_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v6_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,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(f131,axiom,
! [A] :
( ( l2_altcat_1(A)
& v1_altcat_2(A)
& v12_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l2_altcat_1(B)
& v1_altcat_2(B)
& v12_altcat_1(B)
& v2_altcat_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( l2_functor0(C,A,B)
& v8_functor0(C,A,B) )
=> ( v21_functor0(C,A,B)
=> ! [D] :
( ( l2_functor0(D,B,A)
& v8_functor0(D,B,A) )
=> ( g2_functor0(B,A,u1_functor0(B,A,D),u2_functor0(B,A,D)) = k15_functor0(A,B,C)
=> k13_functor0(B,A,B,D,C) = k12_functor0(B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,plain,
? [A] :
( ( k13_functor0(k4_waybel34(A),k5_waybel34(A),k4_waybel34(A),k6_waybel34(A),k7_waybel34(A)) != k12_functor0(k4_waybel34(A))
| k13_functor0(k5_waybel34(A),k4_waybel34(A),k5_waybel34(A),k7_waybel34(A),k6_waybel34(A)) != k12_functor0(k5_waybel34(A)) )
& ~ v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f140,plain,
( ( k13_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k6_waybel34(sK0_skl),k7_waybel34(sK0_skl)) != k12_functor0(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) )
& ~ v2_setfam_1(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f139]) ).
fof(f141,plain,
~ v2_setfam_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f142,plain,
( k13_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k6_waybel34(sK0_skl),k7_waybel34(sK0_skl)) != k12_functor0(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f145,plain,
! [A,B,C] :
( C = g2_functor0(A,B,u1_functor0(A,B,C),u2_functor0(A,B,C))
| ~ v9_functor0(C,A,B)
| ~ l2_functor0(C,A,B)
| ~ l1_altcat_1(B)
| ~ l1_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f146,plain,
! [X0,X1,X2] :
( X2 = g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2))
| ~ v9_functor0(X2,X0,X1)
| ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f195,plain,
! [A,B] :
( ! [C] :
( ( v12_functor0(C,A,B)
& v8_functor0(C,A,B) )
| ~ m2_functor0(C,A,B) )
| ~ l2_altcat_1(B)
| ~ v12_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)],[f19]) ).
fof(f196,plain,
! [X0,X1,X2] :
( v8_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v12_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)],[f195]) ).
fof(f222,plain,
! [A] :
( ( v1_altcat_2(A)
& ~ v3_struct_0(A) )
| ~ v12_altcat_1(A)
| v3_struct_0(A)
| ~ l2_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f224,plain,
! [X0] :
( v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f233,plain,
! [A] :
( ~ v1_xboole_0(A)
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f234,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f290,plain,
! [A,B,C] :
( ( l2_functor0(k15_functor0(A,B,C),B,A)
& v9_functor0(k15_functor0(A,B,C),B,A) )
| ~ l2_functor0(C,A,B)
| ~ l1_altcat_1(B)
| v3_struct_0(B)
| ~ l1_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f291,plain,
! [X0,X1,X2] :
( v9_functor0(k15_functor0(X0,X1,X2),X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| v3_struct_0(X1)
| ~ l1_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f292,plain,
! [X0,X1,X2] :
( l2_functor0(k15_functor0(X0,X1,X2),X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| v3_struct_0(X1)
| ~ l1_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f297,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)],[f52]) ).
fof(f302,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f304,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f305,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)],[f53]) ).
fof(f310,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f312,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f313,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)],[f54]) ).
fof(f316,plain,
! [X0] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f317,plain,
! [A] :
( ( m2_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v16_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v9_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f320,plain,
! [X0] :
( m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f323,plain,
! [A] :
( l1_altcat_1(A)
| ~ l2_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f324,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f333,plain,
! [A,B] :
( ! [C] :
( l2_functor0(C,A,B)
| ~ m2_functor0(C,A,B) )
| ~ l2_altcat_1(B)
| ~ v12_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)],[f65]) ).
fof(f334,plain,
! [X0,X1,X2] :
( l2_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v12_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)],[f333]) ).
fof(f415,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)],[f97]) ).
fof(f416,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f417,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f421,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f435,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)],[f99]) ).
fof(f436,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f437,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f441,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f453,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)],[f101]) ).
fof(f455,plain,
! [X0] :
( v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f461,plain,
! [X0] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f453]) ).
fof(f462,plain,
! [A] :
( ( v21_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v16_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v14_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v12_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v11_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v9_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v8_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A))
& v6_functor0(k7_waybel34(A),k5_waybel34(A),k4_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f464,plain,
! [X0] :
( v8_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f470,plain,
! [X0] :
( v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f593,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)],[f129]) ).
fof(f594,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)],[f593]) ).
fof(f595,plain,
! [X0] :
( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f593]) ).
fof(f598,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( k13_functor0(B,A,B,D,C) = k12_functor0(B)
| g2_functor0(B,A,u1_functor0(B,A,D),u2_functor0(B,A,D)) != k15_functor0(A,B,C)
| ~ l2_functor0(D,B,A)
| ~ v8_functor0(D,B,A) )
| ~ v21_functor0(C,A,B)
| ~ l2_functor0(C,A,B)
| ~ v8_functor0(C,A,B) )
| ~ l2_altcat_1(B)
| ~ v1_altcat_2(B)
| ~ v12_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v1_altcat_2(A)
| ~ v12_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f131]) ).
fof(f599,plain,
! [X0,X1,X2,X3] :
( k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1)
| g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3)) != k15_functor0(X0,X1,X2)
| ~ l2_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| ~ v21_functor0(X2,X0,X1)
| ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v1_altcat_2(X1)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f598]) ).
fof(f620,plain,
~ v3_struct_0(k4_waybel34(sK0_skl)),
inference(resolution,[status(thm)],[f416,f141]) ).
fof(f621,plain,
~ v3_struct_0(k5_waybel34(sK0_skl)),
inference(resolution,[status(thm)],[f436,f141]) ).
fof(f630,plain,
k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)) = k7_waybel34(sK0_skl),
inference(resolution,[status(thm)],[f594,f141]) ).
fof(f631,plain,
k15_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)) = k6_waybel34(sK0_skl),
inference(resolution,[status(thm)],[f595,f141]) ).
fof(f632,plain,
! [X0,X1,X2,X3] :
( k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1)
| g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3)) != k15_functor0(X0,X1,X2)
| ~ l2_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| ~ v21_functor0(X2,X0,X1)
| ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v1_altcat_2(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(forward_subsumption_resolution,[status(thm)],[f599,f224]) ).
fof(f636,plain,
! [X0,X1,X2] :
( k13_functor0(X0,k5_waybel34(sK0_skl),X0,X2,X1) = k12_functor0(X0)
| g2_functor0(X0,k5_waybel34(sK0_skl),u1_functor0(X0,k5_waybel34(sK0_skl),X2),u2_functor0(X0,k5_waybel34(sK0_skl),X2)) != k15_functor0(k5_waybel34(sK0_skl),X0,X1)
| ~ l2_functor0(X2,X0,k5_waybel34(sK0_skl))
| ~ v8_functor0(X2,X0,k5_waybel34(sK0_skl))
| ~ v21_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ v8_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f632,f621]) ).
fof(f638,plain,
! [X0,X1,X2] :
( k13_functor0(X0,k4_waybel34(sK0_skl),X0,X2,X1) = k12_functor0(X0)
| g2_functor0(X0,k4_waybel34(sK0_skl),u1_functor0(X0,k4_waybel34(sK0_skl),X2),u2_functor0(X0,k4_waybel34(sK0_skl),X2)) != k15_functor0(k4_waybel34(sK0_skl),X0,X1)
| ~ l2_functor0(X2,X0,k4_waybel34(sK0_skl))
| ~ v8_functor0(X2,X0,k4_waybel34(sK0_skl))
| ~ v21_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ v8_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f632,f620]) ).
fof(f646,plain,
! [X0,X1,X2] :
( k13_functor0(X0,k5_waybel34(sK0_skl),X0,X2,X1) = k12_functor0(X0)
| g2_functor0(X0,k5_waybel34(sK0_skl),u1_functor0(X0,k5_waybel34(sK0_skl),X2),u2_functor0(X0,k5_waybel34(sK0_skl),X2)) != k15_functor0(k5_waybel34(sK0_skl),X0,X1)
| ~ l2_functor0(X2,X0,k5_waybel34(sK0_skl))
| ~ v8_functor0(X2,X0,k5_waybel34(sK0_skl))
| ~ v21_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ v8_functor0(X1,k5_waybel34(sK0_skl),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f636,f224]) ).
fof(f648,plain,
! [X0,X1,X2] :
( k13_functor0(X0,k4_waybel34(sK0_skl),X0,X2,X1) = k12_functor0(X0)
| g2_functor0(X0,k4_waybel34(sK0_skl),u1_functor0(X0,k4_waybel34(sK0_skl),X2),u2_functor0(X0,k4_waybel34(sK0_skl),X2)) != k15_functor0(k4_waybel34(sK0_skl),X0,X1)
| ~ l2_functor0(X2,X0,k4_waybel34(sK0_skl))
| ~ v8_functor0(X2,X0,k4_waybel34(sK0_skl))
| ~ v21_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ v8_functor0(X1,k4_waybel34(sK0_skl),X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f638,f224]) ).
fof(f668,plain,
! [X0,X1] :
( k13_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),X1,X0) = k12_functor0(k4_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),X1),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),X1)) != k15_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(X1,k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v21_functor0(X0,k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(X0,k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(X0,k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f646,f620]) ).
fof(f672,plain,
! [X0,X1] :
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),X1,X0) = k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),X1),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),X1)) != k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),X0)
| ~ l2_functor0(X1,k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(X1,k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v21_functor0(X0,k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(X0,k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(X0,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))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f648,f621]) ).
fof(f686,plain,
( l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f630,f292]) ).
fof(f687,plain,
( v9_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f630,f291]) ).
fof(f688,plain,
( l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f620]) ).
fof(f689,plain,
( v9_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f620]) ).
fof(f690,plain,
( l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f621]) ).
fof(f691,plain,
( v9_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f621]) ).
fof(f692,plain,
( l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f631,f292]) ).
fof(f693,plain,
( v9_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f631,f291]) ).
fof(f694,plain,
( l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f621]) ).
fof(f695,plain,
( v9_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f693,f621]) ).
fof(f696,plain,
( l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f694,f620]) ).
fof(f697,plain,
( v9_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f620]) ).
fof(f701,plain,
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k15_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v21_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f668,f142]) ).
fof(f702,plain,
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v21_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f631,f701]) ).
fof(f703,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f702,f470]) ).
fof(f704,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f703,f437]) ).
fof(f705,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f441]) ).
fof(f706,plain,
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f705,f141]) ).
fof(f707,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f706,f455]) ).
fof(f709,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f707,f417]) ).
fof(f712,plain,
( v2_setfam_1(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f421]) ).
fof(f713,plain,
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f712,f141]) ).
fof(f715,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_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))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f713,f196]) ).
fof(f717,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f715]) ).
fof(f718,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f334]) ).
fof(f763,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f718,f621]) ).
fof(f764,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f763,f620]) ).
fof(f816,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f764,f320]) ).
fof(f817,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f816,f437]) ).
fof(f818,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f441]) ).
fof(f819,plain,
( ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f818,f141]) ).
fof(f821,plain,
( ~ m2_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))
| 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))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f819,f334]) ).
fof(f822,plain,
( ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f821]) ).
fof(f823,plain,
( ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f620]) ).
fof(f824,plain,
( ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f823,f621]) ).
fof(f825,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f824,f316]) ).
fof(f826,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f421]) ).
fof(f827,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f826,f417]) ).
fof(f828,plain,
( ~ v12_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f827,f141]) ).
fof(f829,plain,
( v1_xboole_0(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f828,f310]) ).
fof(f831,plain,
( v1_xboole_0(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f312]) ).
fof(f833,plain,
( v1_xboole_0(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f831,f304]) ).
fof(f918,plain,
~ v1_xboole_0(sK0_skl),
inference(resolution,[status(thm)],[f234,f141]) ).
fof(f919,plain,
( k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| g2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),u1_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),u2_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))) != k6_waybel34(sK0_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f833,f918]) ).
fof(f920,plain,
( ~ v9_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f919,f146]) ).
fof(f921,plain,
( ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f920,f697]) ).
fof(f923,plain,
( ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f921]) ).
fof(f924,plain,
( ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f696]) ).
fof(f927,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_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))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f924,f334]) ).
fof(f929,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f621]) ).
fof(f934,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f620]) ).
fof(f935,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f934,f320]) ).
fof(f936,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f935,f437]) ).
fof(f937,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f936,f441]) ).
fof(f938,plain,
( ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f937,f141]) ).
fof(f939,plain,
( v1_xboole_0(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f938,f302]) ).
fof(f941,plain,
( v1_xboole_0(sK0_skl)
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f939,f312]) ).
fof(f943,plain,
( v1_xboole_0(sK0_skl)
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f941,f304]) ).
fof(f944,plain,
( ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f943,f918]) ).
fof(f945,plain,
( ~ l1_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f324,f944]) ).
fof(f946,plain,
( ~ l2_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f945,f324]) ).
fof(f947,plain,
( v1_xboole_0(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f946,f304]) ).
fof(f948,plain,
( v1_xboole_0(sK0_skl)
| k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f312]) ).
fof(f949,plain,
k13_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k7_waybel34(sK0_skl),k6_waybel34(sK0_skl)) != k12_functor0(k5_waybel34(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f948,f918]) ).
fof(f950,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(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)) ),
inference(resolution,[status(thm)],[f949,f672]) ).
fof(f951,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(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)) ),
inference(forward_demodulation,[status(thm)],[f630,f950]) ).
fof(f952,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(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)) ),
inference(resolution,[status(thm)],[f951,f461]) ).
fof(f953,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f417]) ).
fof(f954,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f953,f421]) ).
fof(f955,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v8_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))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f954,f141]) ).
fof(f956,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_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))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f955,f455]) ).
fof(f958,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_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))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f956,f437]) ).
fof(f963,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f441]) ).
fof(f964,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v8_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f963,f141]) ).
fof(f965,plain,
( v2_setfam_1(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f964,f464]) ).
fof(f967,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f965,f141]) ).
fof(f972,plain,
( ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f967,f696]) ).
fof(f974,plain,
( ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f972]) ).
fof(f975,plain,
( ~ l1_altcat_1(k4_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f974,f324]) ).
fof(f978,plain,
( g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f324]) ).
fof(f980,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_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))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f978,f334]) ).
fof(f982,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f980]) ).
fof(f983,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f621]) ).
fof(f989,plain,
( ~ m2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f983,f620]) ).
fof(f990,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f989,f320]) ).
fof(f991,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f990,f437]) ).
fof(f992,plain,
( v2_setfam_1(sK0_skl)
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f991,f441]) ).
fof(f993,plain,
( ~ v12_altcat_1(k4_waybel34(sK0_skl))
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f992,f141]) ).
fof(f994,plain,
( v1_xboole_0(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f993,f302]) ).
fof(f996,plain,
( v1_xboole_0(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f994,f304]) ).
fof(f998,plain,
( v1_xboole_0(sK0_skl)
| g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f996,f312]) ).
fof(f999,plain,
g2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),u1_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl)),u2_functor0(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl))) != k7_waybel34(sK0_skl),
inference(resolution,[status(thm)],[f998,f918]) ).
fof(f1000,plain,
( ~ v9_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f999,f146]) ).
fof(f1001,plain,
( ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1000,f691]) ).
fof(f1003,plain,
( ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_functor0(k7_waybel34(sK0_skl),k5_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1001]) ).
fof(f1004,plain,
( ~ l2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f690]) ).
fof(f1007,plain,
( ~ m2_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))
| 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))
| ~ l1_altcat_1(k4_waybel34(sK0_skl))
| ~ l1_altcat_1(k5_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1004,f334]) ).
fof(f1008,plain,
( ~ m2_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))
| 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))
| ~ l1_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1007,f324]) ).
fof(f1009,plain,
( ~ m2_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))
| 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(forward_subsumption_resolution,[status(thm)],[f1008,f324]) ).
fof(f1010,plain,
( ~ m2_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))
| 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)) ),
inference(resolution,[status(thm)],[f1009,f620]) ).
fof(f1011,plain,
( ~ m2_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))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f621]) ).
fof(f1017,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(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)) ),
inference(resolution,[status(thm)],[f1011,f316]) ).
fof(f1018,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f417]) ).
fof(f1019,plain,
( v2_setfam_1(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1018,f421]) ).
fof(f1020,plain,
( ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1019,f141]) ).
fof(f1021,plain,
( v1_xboole_0(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1020,f310]) ).
fof(f1023,plain,
( v1_xboole_0(sK0_skl)
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1021,f304]) ).
fof(f1026,plain,
v1_xboole_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1023,f312]) ).
fof(f1027,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f918,f1026]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT361+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 23:51:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 1.67/0.87 % Refutation found
% 1.67/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.67/0.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.67/0.90 % Elapsed time: 0.523404 seconds
% 1.67/0.90 % CPU time: 3.710644 seconds
% 1.67/0.90 % Total memory used: 144.039 MB
% 1.67/0.90 % Net memory used: 142.012 MB
%------------------------------------------------------------------------------