%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT377+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 : Tue Sep 29 11:48:43 AM UTC 2026
% Result : Theorem 1.30s 0.69s
% Output : Refutation 1.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 34
% Syntax : Number of formulae : 287 ( 40 unt; 18 def)
% Number of atoms : 1416 ( 6 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 1765 ( 636 ~; 878 |; 201 &)
% ( 18 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 19 prp; 0-5 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-3 aty)
% Number of variables : 220 ( 0 sgn 219 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t59_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0)) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f29,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f44,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v2_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k10_waybel34) ).
fof(f45,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v2_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_waybel34) ).
fof(f53,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f54,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f55,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_waybel34) ).
fof(f57,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_waybel34) ).
fof(f58,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_waybel34) ).
fof(f94,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f96,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f98,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v6_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v12_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_waybel34) ).
fof(f122,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0)
& k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_waybel34) ).
fof(f125,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& l2_altcat_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v3_altcat_2(X1,X0)
& m1_altcat_2(X1,X0) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v3_altcat_2(X2,X1)
& m1_altcat_2(X2,X1) )
=> ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v3_altcat_2(X2,X0)
& m1_altcat_2(X2,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_altcat_4) ).
fof(f128,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& l2_altcat_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v11_altcat_1(X1)
& v12_altcat_1(X1)
& l2_altcat_1(X1) )
=> ! [X2] :
( ( v16_functor0(X2,X0,X1)
& m2_functor0(X2,X0,X1) )
=> ( v21_functor0(X2,X0,X1)
=> ! [X3] :
( ( ~ v3_struct_0(X3)
& v2_altcat_1(X3)
& v3_altcat_2(X3,X0)
& m1_altcat_2(X3,X0) )
=> ! [X4] :
( ( ~ v3_struct_0(X4)
& v2_altcat_1(X4)
& v3_altcat_2(X4,X1)
& m1_altcat_2(X4,X1) )
=> ( r3_yellow20(X0,X1,X2,X3,X4)
=> r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_yellow20) ).
fof(f129,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_waybel34) ).
fof(f136,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f45]) ).
fof(f139,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f44]) ).
fof(f147,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v12_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f98]) ).
fof(f154,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f147]) ).
fof(f159,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f154]) ).
fof(f173,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f94]) ).
fof(f175,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f187,plain,
? [X0] :
( ~ r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0))
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f213,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f236,plain,
! [X0] :
( ( ~ v3_struct_0(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f139]) ).
fof(f237,plain,
! [X0] :
( ( ~ v3_struct_0(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f136]) ).
fof(f243,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f244,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f245,plain,
! [X0] :
( ( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f247,plain,
! [X0] :
( ( ~ v3_struct_0(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f248,plain,
! [X0] :
( ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f286,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f173]) ).
fof(f287,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f175]) ).
fof(f290,plain,
! [X0] :
( ( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f159]) ).
fof(f311,plain,
! [X0] :
( ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0)
& k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f315,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v3_altcat_2(X2,X0)
& m1_altcat_2(X2,X0) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v3_altcat_2(X2,X1)
| ~ m1_altcat_2(X2,X1) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v3_altcat_2(X1,X0)
| ~ m1_altcat_2(X1,X0) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f125]) ).
fof(f316,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v3_altcat_2(X2,X0)
& m1_altcat_2(X2,X0) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v3_altcat_2(X2,X1)
| ~ m1_altcat_2(X2,X1) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v3_altcat_2(X1,X0)
| ~ m1_altcat_2(X1,X0) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f315]) ).
fof(f320,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| ~ r3_yellow20(X0,X1,X2,X3,X4)
| v3_struct_0(X4)
| ~ v2_altcat_1(X4)
| ~ v3_altcat_2(X4,X1)
| ~ m1_altcat_2(X4,X1) )
| v3_struct_0(X3)
| ~ v2_altcat_1(X3)
| ~ v3_altcat_2(X3,X0)
| ~ m1_altcat_2(X3,X0) )
| ~ v21_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ l2_altcat_1(X1) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f128]) ).
fof(f321,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| ~ r3_yellow20(X0,X1,X2,X3,X4)
| v3_struct_0(X4)
| ~ v2_altcat_1(X4)
| ~ v3_altcat_2(X4,X1)
| ~ m1_altcat_2(X4,X1) )
| v3_struct_0(X3)
| ~ v2_altcat_1(X3)
| ~ v3_altcat_2(X3,X0)
| ~ m1_altcat_2(X3,X0) )
| ~ v21_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ l2_altcat_1(X1) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f320]) ).
fof(f322,plain,
! [X0] :
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f129]) ).
fof(f327,plain,
~ v2_setfam_1(sK0),
inference(cnf_transformation,[],[f187]) ).
fof(f328,plain,
~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),k11_waybel34(sK0),k10_waybel34(sK0)),
inference(cnf_transformation,[],[f187]) ).
fof(f370,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f407,plain,
! [X0] :
( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f236]) ).
fof(f408,plain,
! [X0] :
( v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f236]) ).
fof(f410,plain,
! [X0] :
( v2_altcat_1(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f236]) ).
fof(f411,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k10_waybel34(X0)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f412,plain,
! [X0] :
( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f413,plain,
! [X0] :
( v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f415,plain,
! [X0] :
( v2_altcat_1(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f416,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f237]) ).
fof(f421,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f243]) ).
fof(f428,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f244]) ).
fof(f435,plain,
! [X0] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f245]) ).
fof(f436,plain,
! [X0] :
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f245]) ).
fof(f441,plain,
! [X0] :
( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f442,plain,
! [X0] :
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f444,plain,
! [X0] :
( v2_altcat_1(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f445,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f446,plain,
! [X0] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f447,plain,
! [X0] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f449,plain,
! [X0] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f450,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f502,plain,
! [X0] :
( v2_setfam_1(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f286]) ).
fof(f503,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f506,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f286]) ).
fof(f507,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f286]) ).
fof(f520,plain,
! [X0] :
( v2_setfam_1(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f287]) ).
fof(f521,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f524,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f525,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f287]) ).
fof(f528,plain,
! [X0] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f290]) ).
fof(f608,plain,
! [X0] :
( v2_setfam_1(X0)
| k7_waybel34(X0) = k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) ),
inference(cnf_transformation,[],[f311]) ).
fof(f611,plain,
! [X2,X0,X1] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| m1_altcat_2(X2,X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f612,plain,
! [X2,X0,X1] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| v3_altcat_2(X2,X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f615,plain,
! [X2,X3,X0,X1,X4] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| v3_struct_0(X3)
| ~ m1_altcat_2(X4,X1)
| ~ v3_altcat_2(X4,X1)
| ~ v2_altcat_1(X4)
| v3_struct_0(X4)
| ~ r3_yellow20(X0,X1,X2,X3,X4)
| r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3) ),
inference(cnf_transformation,[],[f321]) ).
fof(f616,plain,
! [X0] :
( v2_setfam_1(X0)
| r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f322]) ).
fof(f621,plain,
r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),k11_waybel34(sK0),k10_waybel34(sK0)),
inference(consistent_polarity_flipping,[],[f328]) ).
fof(f692,plain,
! [X0] :
( v3_struct_0(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f411]) ).
fof(f694,plain,
! [X0] :
( v3_struct_0(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f416]) ).
fof(f702,plain,
! [X0] :
( ~ l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(consistent_polarity_flipping,[],[f421]) ).
fof(f707,plain,
! [X0] :
( ~ l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(consistent_polarity_flipping,[],[f428]) ).
fof(f708,plain,
! [X0] :
( ~ v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f436]) ).
fof(f709,plain,
! [X0] :
( ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f435]) ).
fof(f712,plain,
! [X0] :
( v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(consistent_polarity_flipping,[],[f445]) ).
fof(f714,plain,
! [X0] :
( v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f450]) ).
fof(f748,plain,
! [X0] :
( v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f507]) ).
fof(f750,plain,
! [X0] :
( ~ v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f502]) ).
fof(f757,plain,
! [X0] :
( v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f525]) ).
fof(f759,plain,
! [X0] :
( ~ v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f520]) ).
fof(f767,plain,
! [X0] :
( ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f528]) ).
fof(f817,plain,
! [X2,X0,X1] :
( ~ v3_altcat_2(X2,X1)
| v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| ~ m1_altcat_2(X2,X1)
| l2_altcat_1(X0)
| ~ v2_altcat_1(X2)
| ~ v3_struct_0(X2)
| v3_altcat_2(X2,X0) ),
inference(consistent_polarity_flipping,[],[f612]) ).
fof(f818,plain,
! [X2,X0,X1] :
( ~ v3_altcat_2(X2,X1)
| v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| ~ m1_altcat_2(X2,X1)
| l2_altcat_1(X0)
| ~ v2_altcat_1(X2)
| ~ v3_struct_0(X2)
| m1_altcat_2(X2,X0) ),
inference(consistent_polarity_flipping,[],[f611]) ).
fof(f820,plain,
! [X2,X3,X0,X1,X4] :
( ~ r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| l2_altcat_1(X1)
| v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| m2_functor0(X2,X0,X1)
| v16_functor0(X2,X0,X1)
| v21_functor0(X2,X0,X1)
| ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| ~ v3_struct_0(X3)
| ~ m1_altcat_2(X4,X1)
| ~ v3_altcat_2(X4,X1)
| ~ v2_altcat_1(X4)
| ~ v3_struct_0(X4)
| r3_yellow20(X0,X1,X2,X3,X4)
| l2_altcat_1(X0) ),
inference(consistent_polarity_flipping,[],[f615]) ).
fof(f821,plain,
! [X0] :
( ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(consistent_polarity_flipping,[],[f616]) ).
fof(f982,plain,
k7_waybel34(sK0) = k15_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)),
inference(resolution,[],[f608,f327]) ).
fof(f1040,definition,
( spl32_8
<=> v3_struct_0(k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
fof(f1041,plain,
( v3_struct_0(k4_waybel34(sK0))
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1042,plain,
( ~ v3_struct_0(k4_waybel34(sK0))
| spl32_8 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1048,definition,
( spl32_10
<=> v3_struct_0(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
fof(f1049,plain,
( v3_struct_0(k5_waybel34(sK0))
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1050,plain,
( ~ v3_struct_0(k5_waybel34(sK0))
| spl32_10 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1073,plain,
( v2_setfam_1(sK0)
| spl32_8 ),
inference(resolution,[],[f1042,f748]) ).
fof(f1075,plain,
( $false
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f1073,f327]) ).
fof(f1076,plain,
spl32_8,
inference(avatar_contradiction_clause,[],[f1075]) ).
fof(f1077,plain,
( v2_setfam_1(sK0)
| spl32_10 ),
inference(resolution,[],[f1050,f757]) ).
fof(f1079,plain,
( $false
| spl32_10 ),
inference(forward_subsumption_resolution,[],[f1077,f327]) ).
fof(f1080,plain,
spl32_10,
inference(avatar_contradiction_clause,[],[f1079]) ).
fof(f1741,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ 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))
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(resolution,[],[f817,f413]) ).
fof(f1742,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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))
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ v3_struct_0(k10_waybel34(X1))
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(resolution,[],[f817,f408]) ).
fof(f1750,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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)
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ v3_struct_0(k10_waybel34(X1))
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1742,f407]) ).
fof(f1751,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ 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)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1741,f412]) ).
fof(f1755,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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)
| ~ v3_struct_0(k10_waybel34(X1))
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1750,f410]) ).
fof(f1756,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v3_struct_0(k9_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1751,f449]) ).
fof(f1759,plain,
! [X0,X1] :
( ~ v2_altcat_1(k8_waybel34(X1))
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| ~ v3_struct_0(k8_waybel34(X1))
| l2_altcat_1(X0)
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1755,f692]) ).
fof(f1760,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1756,f714]) ).
fof(f1763,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| l2_altcat_1(X0)
| ~ v3_struct_0(k11_waybel34(X1))
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1760,f415]) ).
fof(f1766,plain,
! [X0,X1] :
( ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| v3_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1763,f694]) ).
fof(f1767,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ 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))
| ~ m1_altcat_2(k11_waybel34(X1),k9_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(resolution,[],[f818,f413]) ).
fof(f1768,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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))
| ~ m1_altcat_2(k10_waybel34(X1),k8_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ v3_struct_0(k10_waybel34(X1))
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(resolution,[],[f818,f408]) ).
fof(f1776,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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)
| ~ v2_altcat_1(k10_waybel34(X1))
| ~ v3_struct_0(k10_waybel34(X1))
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1768,f407]) ).
fof(f1777,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ 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)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1767,f412]) ).
fof(f1781,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(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)
| ~ v3_struct_0(k10_waybel34(X1))
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1776,f410]) ).
fof(f1782,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v3_struct_0(k9_waybel34(X1))
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1777,f449]) ).
fof(f1785,plain,
! [X0,X1] :
( ~ v2_altcat_1(k8_waybel34(X1))
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| ~ v3_struct_0(k8_waybel34(X1))
| l2_altcat_1(X0)
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1781,f692]) ).
fof(f1786,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| l2_altcat_1(X0)
| ~ v2_altcat_1(k11_waybel34(X1))
| ~ v3_struct_0(k11_waybel34(X1))
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1782,f714]) ).
fof(f1789,plain,
! [X0,X1] :
( v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| ~ v3_altcat_2(k9_waybel34(X1),X0)
| l2_altcat_1(X0)
| ~ v3_struct_0(k11_waybel34(X1))
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1786,f415]) ).
fof(f1792,plain,
! [X0,X1] :
( ~ v3_altcat_2(k9_waybel34(X1),X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k9_waybel34(X1),X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| m1_altcat_2(k11_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f1789,f694]) ).
fof(f1835,plain,
! [X0,X1] :
( ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),X0,X1)
| v12_altcat_1(k4_waybel34(sK0))
| ~ v11_altcat_1(k4_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0))
| ~ v3_struct_0(k4_waybel34(sK0))
| l2_altcat_1(k5_waybel34(sK0))
| v12_altcat_1(k5_waybel34(sK0))
| ~ v11_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0))
| ~ v3_struct_0(k5_waybel34(sK0))
| m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v16_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(X1,k4_waybel34(sK0))
| ~ v3_altcat_2(X1,k4_waybel34(sK0))
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| ~ m1_altcat_2(X0,k5_waybel34(sK0))
| ~ v3_altcat_2(X0,k5_waybel34(sK0))
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| r3_yellow20(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0),X1,X0)
| l2_altcat_1(k4_waybel34(sK0)) ),
inference(superposition,[],[f820,f982]) ).
fof(f1836,plain,
( ! [X0,X1] :
( ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),X0,X1)
| v12_altcat_1(k4_waybel34(sK0))
| ~ v11_altcat_1(k4_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0))
| l2_altcat_1(k5_waybel34(sK0))
| v12_altcat_1(k5_waybel34(sK0))
| ~ v11_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0))
| ~ v3_struct_0(k5_waybel34(sK0))
| m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v16_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(X1,k4_waybel34(sK0))
| ~ v3_altcat_2(X1,k4_waybel34(sK0))
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| ~ m1_altcat_2(X0,k5_waybel34(sK0))
| ~ v3_altcat_2(X0,k5_waybel34(sK0))
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| r3_yellow20(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0),X1,X0)
| l2_altcat_1(k4_waybel34(sK0)) )
| ~ spl32_8 ),
inference(forward_subsumption_resolution,[],[f1835,f1041]) ).
fof(f1838,plain,
( ! [X0,X1] :
( ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),X0,X1)
| v12_altcat_1(k4_waybel34(sK0))
| ~ v11_altcat_1(k4_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0))
| l2_altcat_1(k5_waybel34(sK0))
| v12_altcat_1(k5_waybel34(sK0))
| ~ v11_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0))
| m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v16_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(X1,k4_waybel34(sK0))
| ~ v3_altcat_2(X1,k4_waybel34(sK0))
| ~ v2_altcat_1(X1)
| ~ v3_struct_0(X1)
| ~ m1_altcat_2(X0,k5_waybel34(sK0))
| ~ v3_altcat_2(X0,k5_waybel34(sK0))
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| r3_yellow20(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0),X1,X0)
| l2_altcat_1(k4_waybel34(sK0)) )
| ~ spl32_8
| ~ spl32_10 ),
inference(forward_subsumption_resolution,[],[f1836,f1049]) ).
fof(f1841,definition,
( spl32_18
<=> l2_altcat_1(k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_18])],[avatar_definition]) ).
fof(f1843,plain,
( l2_altcat_1(k4_waybel34(sK0))
| ~ spl32_18 ),
inference(avatar_component_clause,[],[f1841]) ).
fof(f1845,definition,
( spl32_19
<=> v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_19])],[avatar_definition]) ).
fof(f1847,plain,
( v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ spl32_19 ),
inference(avatar_component_clause,[],[f1845]) ).
fof(f1849,definition,
( spl32_20
<=> v16_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_20])],[avatar_definition]) ).
fof(f1851,plain,
( v16_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ spl32_20 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1853,definition,
( spl32_21
<=> m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
fof(f1855,plain,
( m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f1853]) ).
fof(f1857,definition,
( spl32_22
<=> v2_altcat_1(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_22])],[avatar_definition]) ).
fof(f1859,plain,
( ~ v2_altcat_1(k5_waybel34(sK0))
| spl32_22 ),
inference(avatar_component_clause,[],[f1857]) ).
fof(f1861,definition,
( spl32_23
<=> v11_altcat_1(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_23])],[avatar_definition]) ).
fof(f1863,plain,
( ~ v11_altcat_1(k5_waybel34(sK0))
| spl32_23 ),
inference(avatar_component_clause,[],[f1861]) ).
fof(f1865,definition,
( spl32_24
<=> v12_altcat_1(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_24])],[avatar_definition]) ).
fof(f1867,plain,
( v12_altcat_1(k5_waybel34(sK0))
| ~ spl32_24 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1869,definition,
( spl32_25
<=> l2_altcat_1(k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_25])],[avatar_definition]) ).
fof(f1870,plain,
( ~ l2_altcat_1(k5_waybel34(sK0))
| spl32_25 ),
inference(avatar_component_clause,[],[f1869]) ).
fof(f1871,plain,
( l2_altcat_1(k5_waybel34(sK0))
| ~ spl32_25 ),
inference(avatar_component_clause,[],[f1869]) ).
fof(f1873,definition,
( spl32_26
<=> v2_altcat_1(k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_26])],[avatar_definition]) ).
fof(f1875,plain,
( ~ v2_altcat_1(k4_waybel34(sK0))
| spl32_26 ),
inference(avatar_component_clause,[],[f1873]) ).
fof(f1877,definition,
( spl32_27
<=> v11_altcat_1(k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_27])],[avatar_definition]) ).
fof(f1879,plain,
( ~ v11_altcat_1(k4_waybel34(sK0))
| spl32_27 ),
inference(avatar_component_clause,[],[f1877]) ).
fof(f1881,definition,
( spl32_28
<=> v12_altcat_1(k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
fof(f1883,plain,
( v12_altcat_1(k4_waybel34(sK0))
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f1881]) ).
fof(f1885,definition,
( spl32_29
<=> ! [X0,X1] :
( ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),X0,X1)
| r3_yellow20(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0),X1,X0)
| ~ v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v3_altcat_2(X0,k5_waybel34(sK0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0))
| ~ v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(sK0))
| ~ m1_altcat_2(X1,k4_waybel34(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
fof(f1886,plain,
( ! [X0,X1] :
( r3_yellow20(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0),X1,X0)
| ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),X0,X1)
| ~ v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v3_altcat_2(X0,k5_waybel34(sK0))
| ~ m1_altcat_2(X0,k5_waybel34(sK0))
| ~ v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(sK0))
| ~ m1_altcat_2(X1,k4_waybel34(sK0)) )
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f1885]) ).
fof(f1887,plain,
( spl32_18
| spl32_19
| spl32_20
| spl32_21
| ~ spl32_22
| ~ spl32_23
| spl32_24
| spl32_25
| ~ spl32_26
| ~ spl32_27
| spl32_28
| spl32_29
| ~ spl32_8
| ~ spl32_10 ),
inference(avatar_split_clause,[],[f1838,f1048,f1040,f1885,f1881,f1877,f1873,f1869,f1865,f1861,f1857,f1853,f1849,f1845,f1841]) ).
fof(f1920,plain,
( v2_setfam_1(sK0)
| spl32_22 ),
inference(resolution,[],[f1859,f524]) ).
fof(f1922,plain,
( $false
| spl32_22 ),
inference(forward_subsumption_resolution,[],[f1920,f327]) ).
fof(f1923,plain,
spl32_22,
inference(avatar_contradiction_clause,[],[f1922]) ).
fof(f1946,plain,
( v2_setfam_1(sK0)
| spl32_23 ),
inference(resolution,[],[f1863,f521]) ).
fof(f1948,plain,
( $false
| spl32_23 ),
inference(forward_subsumption_resolution,[],[f1946,f327]) ).
fof(f1949,plain,
spl32_23,
inference(avatar_contradiction_clause,[],[f1948]) ).
fof(f1962,plain,
( v2_setfam_1(sK0)
| spl32_26 ),
inference(resolution,[],[f1875,f506]) ).
fof(f1964,plain,
( $false
| spl32_26 ),
inference(forward_subsumption_resolution,[],[f1962,f327]) ).
fof(f1965,plain,
spl32_26,
inference(avatar_contradiction_clause,[],[f1964]) ).
fof(f1966,plain,
( v2_setfam_1(sK0)
| spl32_27 ),
inference(resolution,[],[f1879,f503]) ).
fof(f1968,plain,
( $false
| spl32_27 ),
inference(forward_subsumption_resolution,[],[f1966,f327]) ).
fof(f1969,plain,
spl32_27,
inference(avatar_contradiction_clause,[],[f1968]) ).
fof(f1970,plain,
( v1_xboole_0(sK0)
| ~ spl32_18 ),
inference(resolution,[],[f1843,f702]) ).
fof(f1977,plain,
( v2_setfam_1(sK0)
| ~ spl32_18 ),
inference(resolution,[],[f1970,f370]) ).
fof(f1981,plain,
( $false
| ~ spl32_18 ),
inference(forward_subsumption_resolution,[],[f1977,f327]) ).
fof(f1982,plain,
~ spl32_18,
inference(avatar_contradiction_clause,[],[f1981]) ).
fof(f2047,plain,
( v2_setfam_1(sK0)
| ~ spl32_24 ),
inference(resolution,[],[f1867,f759]) ).
fof(f2059,plain,
( $false
| ~ spl32_24 ),
inference(forward_subsumption_resolution,[],[f2047,f327]) ).
fof(f2060,plain,
~ spl32_24,
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2066,plain,
( v1_xboole_0(sK0)
| ~ spl32_25 ),
inference(resolution,[],[f1871,f707]) ).
fof(f2071,plain,
( v2_setfam_1(sK0)
| ~ spl32_25 ),
inference(resolution,[],[f2066,f370]) ).
fof(f2075,plain,
( $false
| ~ spl32_25 ),
inference(forward_subsumption_resolution,[],[f2071,f327]) ).
fof(f2076,plain,
~ spl32_25,
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2098,plain,
( v2_setfam_1(sK0)
| ~ spl32_28 ),
inference(resolution,[],[f1883,f750]) ).
fof(f2110,plain,
( $false
| ~ spl32_28 ),
inference(forward_subsumption_resolution,[],[f2098,f327]) ).
fof(f2111,plain,
~ spl32_28,
inference(avatar_contradiction_clause,[],[f2110]) ).
fof(f2117,plain,
( v2_setfam_1(sK0)
| ~ spl32_19 ),
inference(resolution,[],[f1847,f767]) ).
fof(f2118,plain,
( $false
| ~ spl32_19 ),
inference(forward_subsumption_resolution,[],[f2117,f327]) ).
fof(f2119,plain,
~ spl32_19,
inference(avatar_contradiction_clause,[],[f2118]) ).
fof(f2124,plain,
( v2_setfam_1(sK0)
| ~ spl32_20 ),
inference(resolution,[],[f1851,f708]) ).
fof(f2127,plain,
( $false
| ~ spl32_20 ),
inference(forward_subsumption_resolution,[],[f2124,f327]) ).
fof(f2128,plain,
~ spl32_20,
inference(avatar_contradiction_clause,[],[f2127]) ).
fof(f2144,plain,
( v2_setfam_1(sK0)
| ~ spl32_21 ),
inference(resolution,[],[f1855,f709]) ).
fof(f2145,plain,
( $false
| ~ spl32_21 ),
inference(forward_subsumption_resolution,[],[f2144,f327]) ).
fof(f2146,plain,
~ spl32_21,
inference(avatar_contradiction_clause,[],[f2145]) ).
fof(f2709,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0)
| v2_setfam_1(X0) ),
inference(resolution,[],[f1766,f447]) ).
fof(f2710,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(duplicate_literal_removal,[],[f2709]) ).
fof(f2711,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2710,f446]) ).
fof(f2712,plain,
! [X0] :
( ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2711,f521]) ).
fof(f2713,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2712,f524]) ).
fof(f2714,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2713,f757]) ).
fof(f2715,plain,
! [X0] :
( v3_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2714,f759]) ).
fof(f2716,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0)
| v2_setfam_1(X0) ),
inference(resolution,[],[f1792,f447]) ).
fof(f2717,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(duplicate_literal_removal,[],[f2716]) ).
fof(f2718,plain,
! [X0] :
( ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2717,f446]) ).
fof(f2719,plain,
! [X0] :
( ~ v2_altcat_1(k5_waybel34(X0))
| ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2718,f521]) ).
fof(f2720,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2719,f524]) ).
fof(f2721,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2720,f757]) ).
fof(f2722,plain,
! [X0] :
( m1_altcat_2(k11_waybel34(X0),k5_waybel34(X0))
| l2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f2721,f759]) ).
fof(f2802,plain,
! [X0,X1] :
( ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| ~ v3_struct_0(k8_waybel34(X1))
| l2_altcat_1(X0)
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1)
| v1_xboole_0(X1) ),
inference(resolution,[],[f1759,f444]) ).
fof(f2803,plain,
! [X0,X1] :
( ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1)
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f2802,f712]) ).
fof(f2804,plain,
! [X0,X1] :
( ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v11_altcat_1(X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| v3_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f2803,f370]) ).
fof(f2805,plain,
! [X0,X1] :
( ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| ~ v3_struct_0(k8_waybel34(X1))
| l2_altcat_1(X0)
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1)
| v1_xboole_0(X1) ),
inference(resolution,[],[f1785,f444]) ).
fof(f2806,plain,
! [X0,X1] :
( ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v3_altcat_2(k8_waybel34(X1),X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1)
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f2805,f712]) ).
fof(f2807,plain,
! [X0,X1] :
( ~ v3_altcat_2(k8_waybel34(X1),X0)
| ~ v2_altcat_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(X1),X0)
| ~ v11_altcat_1(X0)
| v12_altcat_1(X0)
| l2_altcat_1(X0)
| m1_altcat_2(k10_waybel34(X1),X0)
| v2_setfam_1(X1) ),
inference(forward_subsumption_resolution,[],[f2806,f370]) ).
fof(f3181,plain,
( ~ r3_yellow20(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0),k11_waybel34(sK0),k10_waybel34(sK0))
| ~ v3_struct_0(k11_waybel34(sK0))
| ~ v2_altcat_1(k11_waybel34(sK0))
| ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_struct_0(k10_waybel34(sK0))
| ~ v2_altcat_1(k10_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(resolution,[],[f1886,f821]) ).
fof(f3182,plain,
( ~ v3_struct_0(k11_waybel34(sK0))
| ~ v2_altcat_1(k11_waybel34(sK0))
| ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_struct_0(k10_waybel34(sK0))
| ~ v2_altcat_1(k10_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3181,f621]) ).
fof(f3183,plain,
( ~ v2_altcat_1(k11_waybel34(sK0))
| ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_struct_0(k10_waybel34(sK0))
| ~ v2_altcat_1(k10_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3182,f694]) ).
fof(f3184,plain,
( ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_struct_0(k10_waybel34(sK0))
| ~ v2_altcat_1(k10_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3183,f415]) ).
fof(f3185,plain,
( ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v2_altcat_1(k10_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3184,f692]) ).
fof(f3186,plain,
( ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| v2_setfam_1(sK0)
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3185,f410]) ).
fof(f3187,plain,
( ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f3186,f327]) ).
fof(f3189,definition,
( spl32_139
<=> m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_139])],[avatar_definition]) ).
fof(f3191,plain,
( ~ m1_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| spl32_139 ),
inference(avatar_component_clause,[],[f3189]) ).
fof(f3193,definition,
( spl32_140
<=> v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_140])],[avatar_definition]) ).
fof(f3195,plain,
( ~ v3_altcat_2(k10_waybel34(sK0),k4_waybel34(sK0))
| spl32_140 ),
inference(avatar_component_clause,[],[f3193]) ).
fof(f3197,definition,
( spl32_141
<=> m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_141])],[avatar_definition]) ).
fof(f3199,plain,
( ~ m1_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| spl32_141 ),
inference(avatar_component_clause,[],[f3197]) ).
fof(f3201,definition,
( spl32_142
<=> v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_142])],[avatar_definition]) ).
fof(f3203,plain,
( ~ v3_altcat_2(k11_waybel34(sK0),k5_waybel34(sK0))
| spl32_142 ),
inference(avatar_component_clause,[],[f3201]) ).
fof(f3204,plain,
( ~ spl32_139
| ~ spl32_140
| ~ spl32_141
| ~ spl32_142
| ~ spl32_29 ),
inference(avatar_split_clause,[],[f3187,f1885,f3201,f3197,f3193,f3189]) ).
fof(f5554,plain,
! [X0] :
( ~ v2_altcat_1(k4_waybel34(X0))
| ~ v3_struct_0(k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(resolution,[],[f2804,f442]) ).
fof(f5555,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5554,f506]) ).
fof(f5556,plain,
! [X0] :
( ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5555,f748]) ).
fof(f5557,plain,
! [X0] :
( ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5556,f441]) ).
fof(f5558,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5557,f503]) ).
fof(f5559,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5558,f750]) ).
fof(f5560,plain,
! [X0] :
( v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5559,f702]) ).
fof(f5561,plain,
! [X0] :
( v3_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f5560,f370]) ).
fof(f5563,plain,
! [X0] :
( ~ v2_altcat_1(k4_waybel34(X0))
| ~ v3_struct_0(k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(resolution,[],[f2807,f442]) ).
fof(f5564,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5563,f506]) ).
fof(f5565,plain,
! [X0] :
( ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5564,f748]) ).
fof(f5566,plain,
! [X0] :
( ~ v11_altcat_1(k4_waybel34(X0))
| v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5565,f441]) ).
fof(f5567,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5566,f503]) ).
fof(f5568,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5567,f750]) ).
fof(f5569,plain,
! [X0] :
( m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f5568,f702]) ).
fof(f5570,plain,
! [X0] :
( m1_altcat_2(k10_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(forward_subsumption_resolution,[],[f5569,f370]) ).
fof(f8763,plain,
( v2_setfam_1(sK0)
| spl32_139 ),
inference(resolution,[],[f5570,f3191]) ).
fof(f8772,plain,
( $false
| spl32_139 ),
inference(forward_subsumption_resolution,[],[f8763,f327]) ).
fof(f8773,plain,
spl32_139,
inference(avatar_contradiction_clause,[],[f8772]) ).
fof(f8813,plain,
( v2_setfam_1(sK0)
| spl32_140 ),
inference(resolution,[],[f3195,f5561]) ).
fof(f8814,plain,
( $false
| spl32_140 ),
inference(forward_subsumption_resolution,[],[f8813,f327]) ).
fof(f8815,plain,
spl32_140,
inference(avatar_contradiction_clause,[],[f8814]) ).
fof(f9017,plain,
( l2_altcat_1(k5_waybel34(sK0))
| v2_setfam_1(sK0)
| spl32_141 ),
inference(resolution,[],[f3199,f2722]) ).
fof(f9018,plain,
( v2_setfam_1(sK0)
| spl32_25
| spl32_141 ),
inference(forward_subsumption_resolution,[],[f9017,f1870]) ).
fof(f9019,plain,
( $false
| spl32_25
| spl32_141 ),
inference(forward_subsumption_resolution,[],[f9018,f327]) ).
fof(f9020,plain,
( spl32_25
| spl32_141 ),
inference(avatar_contradiction_clause,[],[f9019]) ).
fof(f9083,plain,
( l2_altcat_1(k5_waybel34(sK0))
| v2_setfam_1(sK0)
| spl32_142 ),
inference(resolution,[],[f3203,f2715]) ).
fof(f9084,plain,
( v2_setfam_1(sK0)
| spl32_25
| spl32_142 ),
inference(forward_subsumption_resolution,[],[f9083,f1870]) ).
fof(f9085,plain,
( $false
| spl32_25
| spl32_142 ),
inference(forward_subsumption_resolution,[],[f9084,f327]) ).
fof(f9086,plain,
( spl32_25
| spl32_142 ),
inference(avatar_contradiction_clause,[],[f9085]) ).
cnf(s9,plain,
spl32_8,
inference(sat_conversion,[],[f1076]) ).
cnf(s10,plain,
spl32_10,
inference(sat_conversion,[],[f1080]) ).
cnf(s13,plain,
( ~ spl32_8
| ~ spl32_10
| spl32_18
| spl32_19
| spl32_20
| spl32_21
| ~ spl32_22
| ~ spl32_23
| spl32_24
| spl32_25
| ~ spl32_26
| ~ spl32_27
| spl32_28
| spl32_29 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s15,plain,
spl32_22,
inference(sat_conversion,[],[f1923]) ).
cnf(s16,plain,
spl32_23,
inference(sat_conversion,[],[f1949]) ).
cnf(s17,plain,
spl32_26,
inference(sat_conversion,[],[f1965]) ).
cnf(s18,plain,
spl32_27,
inference(sat_conversion,[],[f1969]) ).
cnf(s19,plain,
~ spl32_18,
inference(sat_conversion,[],[f1982]) ).
cnf(s24,plain,
~ spl32_24,
inference(sat_conversion,[],[f2060]) ).
cnf(s25,plain,
~ spl32_25,
inference(sat_conversion,[],[f2076]) ).
cnf(s27,plain,
~ spl32_28,
inference(sat_conversion,[],[f2111]) ).
cnf(s28,plain,
~ spl32_19,
inference(sat_conversion,[],[f2119]) ).
cnf(s29,plain,
~ spl32_20,
inference(sat_conversion,[],[f2128]) ).
cnf(s31,plain,
~ spl32_21,
inference(sat_conversion,[],[f2146]) ).
cnf(s101,plain,
( ~ spl32_29
| ~ spl32_139
| ~ spl32_140
| ~ spl32_141
| ~ spl32_142 ),
inference(sat_conversion,[],[f3204]) ).
cnf(s518,plain,
spl32_139,
inference(sat_conversion,[],[f8773]) ).
cnf(s521,plain,
spl32_140,
inference(sat_conversion,[],[f8815]) ).
cnf(s548,plain,
( spl32_25
| spl32_141 ),
inference(sat_conversion,[],[f9020]) ).
cnf(s554,plain,
( spl32_25
| spl32_142 ),
inference(sat_conversion,[],[f9086]) ).
cnf(s592,plain,
( ~ spl32_29
| ~ spl32_141
| ~ spl32_142 ),
inference(rat,[],[s101,s521,s518]) ).
cnf(s616,plain,
spl32_142,
inference(rat,[],[s554,s25]) ).
cnf(s617,plain,
spl32_141,
inference(rat,[],[s548,s25]) ).
cnf(s619,plain,
~ spl32_29,
inference(rat,[],[s592,s616,s617]) ).
cnf(s637,plain,
( ~ spl32_8
| ~ spl32_10 ),
inference(rat,[],[s13,s619,s27,s18,s17,s25,s24,s16,s15,s31,s29,s28,s19]) ).
cnf(s640,plain,
~ spl32_8,
inference(rat,[],[s637,s10]) ).
cnf(s642,plain,
$false,
inference(rat,[],[s9,s640]) ).
fof(f9087,plain,
$false,
inference(avatar_sat_refutation,[],[s642]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT377+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 15:10:39 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.14/0.41 Running first-order model finding
% 0.14/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.30/0.69 % (1353741)Will run a generic schedule for satisfiability detection.
% 1.30/0.69 % (1353749)dis+10_1_sil=32000:sp=arity:random_seed=2286480002:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.30/0.69 % (1353747)% WARNING: option uhcvi not known.
% 1.30/0.69 % (1353748)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2937350494:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.30/0.69 % (1353746)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=473220436_2999 on theBenchmark for (2999ds/0Mi)
% 1.30/0.69 % (1353747)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3147152311:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.30/0.69 % (1353750)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3950320397:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.30/0.69 % (1353752)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1853061144:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.30/0.69 % (1353751)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2794197142:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.30/0.69 % TRYING [1]
% 1.30/0.69 % TRYING [2]
% 1.30/0.69 % (1353749)Instruction limit reached!
% 1.30/0.69 % (1353749)------------------------------
% 1.30/0.69 % (1353749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353749)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353749)Termination reason: Instruction limit
% 1.30/0.69 % (1353749)Termination phase: Saturation
% 1.30/0.69 % (1353749)Time elapsed: 0.035 s
% 1.30/0.69 % (1353749)Peak memory usage: 13 MB
% 1.30/0.69 % (1353749)Instructions burned: 103 (million)
% 1.30/0.69 % TRYING [3]
% 1.30/0.69 % (1353760)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=17114339:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.30/0.69 % TRYING [1]
% 1.30/0.69 % TRYING [2]
% 1.30/0.69 % TRYING [3]
% 1.30/0.69 % (1353750)Instruction limit reached!
% 1.30/0.69 % (1353750)------------------------------
% 1.30/0.69 % (1353750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353750)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353750)Termination reason: Instruction limit
% 1.30/0.69 % (1353750)Termination phase: Saturation
% 1.30/0.69 % (1353750)Time elapsed: 0.065 s
% 1.30/0.69 % (1353750)Peak memory usage: 13 MB
% 1.30/0.69 % (1353750)Instructions burned: 116 (million)
% 1.30/0.69 % (1353751)Instruction limit reached!
% 1.30/0.69 % (1353751)------------------------------
% 1.30/0.69 % (1353751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353751)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353751)Termination reason: Instruction limit
% 1.30/0.69 % (1353751)Termination phase: Saturation
% 1.30/0.69 % (1353751)Time elapsed: 0.076 s
% 1.30/0.69 % (1353751)Peak memory usage: 13 MB
% 1.30/0.69 % (1353751)Instructions burned: 132 (million)
% 1.30/0.69 % (1353762)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1153986545:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.30/0.69 % (1353752)Instruction limit reached!
% 1.30/0.69 % (1353752)------------------------------
% 1.30/0.69 % (1353752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353752)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353752)Termination reason: Instruction limit
% 1.30/0.69 % (1353752)Termination phase: Saturation
% 1.30/0.69 % (1353752)Time elapsed: 0.091 s
% 1.30/0.69 % (1353752)Peak memory usage: 15 MB
% 1.30/0.69 % (1353752)Instructions burned: 159 (million)
% 1.30/0.69 % (1353763)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4069912386:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.30/0.69 % (1353765)ott-21_1_sil=16000:fs=off:random_seed=3029189396:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.30/0.69 % (1353762)Instruction limit reached!
% 1.30/0.69 % (1353762)------------------------------
% 1.30/0.69 % (1353762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353762)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353762)Termination reason: Instruction limit
% 1.30/0.69 % (1353762)Termination phase: Saturation
% 1.30/0.69 % (1353762)Time elapsed: 0.080 s
% 1.30/0.69 % (1353762)Peak memory usage: 14 MB
% 1.30/0.69 % (1353762)Instructions burned: 132 (million)
% 1.30/0.69 % (1353768)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3326536504:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.30/0.69 % (1353765)Instruction limit reached!
% 1.30/0.69 % (1353765)------------------------------
% 1.30/0.69 % (1353765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353765)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353765)Termination reason: Instruction limit
% 1.30/0.69 % (1353765)Termination phase: Saturation
% 1.30/0.69 % (1353765)Time elapsed: 0.097 s
% 1.30/0.69 % (1353765)Peak memory usage: 13 MB
% 1.30/0.69 % (1353765)Instructions burned: 180 (million)
% 1.30/0.69 % (1353760)Instruction limit reached!
% 1.30/0.69 % (1353760)------------------------------
% 1.30/0.69 % (1353760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.69 % (1353760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.69 % (1353760)CaDiCaL version: 2.1.3
% 1.30/0.69 % (1353760)Termination reason: Instruction limit
% 1.30/0.69 % (1353760)Termination phase: Finite model building SAT solving
% 1.30/0.69 % (1353760)Time elapsed: 0.182 s
% 1.30/0.69 % (1353760)Peak memory usage: 37 MB
% 1.30/0.69 % (1353760)Instructions burned: 715 (million)
% 1.30/0.69 % (1353747) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1353741-1353747"...
% 1.30/0.69 % (1353770)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=9933563:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.30/0.69 % (1353747)...printing done.
% 1.30/0.69 % (1353747)Refutation found. Thanks to Tanya!
% 1.30/0.69 % SZS status Theorem for theBenchmark
% 1.30/0.69 % SZS output start Proof for theBenchmark
% See solution above
% 1.30/0.70 % (1353747)------------------------------
% 1.30/0.70 % (1353747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.30/0.70 % (1353747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/0.70 % (1353747)CaDiCaL version: 2.1.3
% 1.30/0.70 % (1353747)Termination reason: Refutation
% 1.30/0.70 % (1353747)Time elapsed: 0.231 s
% 1.30/0.70 % (1353747)Peak memory usage: 17 MB
% 1.30/0.70 % (1353747)Instructions burned: 375 (million)
% 1.30/0.70 % (1353741)Success in time 0.272 s
% 1.30/0.70 % Vampire exiting
%------------------------------------------------------------------------------