%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT377+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:59:43 PM UTC 2026
% Result : Theorem 7.68s 1.50s
% Output : CNFRefutation 7.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 24
% Syntax : Number of formulae : 299 ( 67 unt; 8 def)
% Number of atoms : 1301 ( 51 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 1254 ( 445 ~; 531 |; 246 &)
% ( 0 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 41 ( 39 usr; 9 prp; 0-5 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-3 aty)
% Number of variables : 272 ( 0 sgn 271 !; 1 ?; 161 :)
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f44,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v2_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& ~ v3_struct_0(k10_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_waybel34) ).
fof(f45,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v2_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& ~ v3_struct_0(k11_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_waybel34) ).
fof(f53,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f54,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f55,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_waybel34) ).
fof(f57,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& ~ v3_struct_0(k8_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_waybel34) ).
fof(f58,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& ~ v3_struct_0(k9_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_waybel34) ).
fof(f94,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v3_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f96,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v3_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f98,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v12_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v6_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_waybel34) ).
fof(f122,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0)
& k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_waybel34) ).
fof(f125,axiom,
! [X0] :
( ( l2_altcat_1(X0)
& v12_altcat_1(X0)
& v11_altcat_1(X0)
& v2_altcat_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_altcat_2(X1,X0)
& v3_altcat_2(X1,X0)
& v2_altcat_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m1_altcat_2(X2,X1)
& v3_altcat_2(X2,X1)
& v2_altcat_1(X2)
& ~ v3_struct_0(X2) )
=> ( m1_altcat_2(X2,X0)
& v3_altcat_2(X2,X0)
& v2_altcat_1(X2)
& ~ v3_struct_0(X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_altcat_4) ).
fof(f128,axiom,
! [X0] :
( ( l2_altcat_1(X0)
& v12_altcat_1(X0)
& v11_altcat_1(X0)
& v2_altcat_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l2_altcat_1(X1)
& v12_altcat_1(X1)
& v11_altcat_1(X1)
& v2_altcat_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_functor0(X2,X0,X1)
& v16_functor0(X2,X0,X1) )
=> ( v21_functor0(X2,X0,X1)
=> ! [X3] :
( ( m1_altcat_2(X3,X0)
& v3_altcat_2(X3,X0)
& v2_altcat_1(X3)
& ~ v3_struct_0(X3) )
=> ! [X4] :
( ( 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) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t58_waybel34) ).
fof(f136,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& ~ v3_struct_0(k11_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f45]) ).
fof(f139,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& ~ v3_struct_0(k10_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f44]) ).
fof(f147,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v12_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f98]) ).
fof(f154,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f147]) ).
fof(f159,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f154]) ).
fof(f173,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v3_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f94]) ).
fof(f175,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v3_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f187,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ~ r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0),k11_waybel34(X0),k10_waybel34(X0)) ),
inference(ennf_transformation,[],[f2]) ).
fof(f213,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f236,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
& v6_altcat_1(k10_waybel34(X0))
& v2_altcat_1(k10_waybel34(X0))
& ~ v3_struct_0(k10_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f139]) ).
fof(f237,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
& v6_altcat_1(k11_waybel34(X0))
& v2_altcat_1(k11_waybel34(X0))
& ~ v3_struct_0(k11_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f136]) ).
fof(f243,plain,
! [X0] :
( v1_xboole_0(X0)
| ( l2_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f244,plain,
! [X0] :
( v1_xboole_0(X0)
| ( l2_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f245,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f55]) ).
fof(f247,plain,
! [X0] :
( v1_xboole_0(X0)
| ( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& ~ v3_struct_0(k8_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f248,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& ~ v3_struct_0(k9_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f58]) ).
fof(f286,plain,
! [X0] :
( v2_setfam_1(X0)
| ( v3_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f173]) ).
fof(f287,plain,
! [X0] :
( v2_setfam_1(X0)
| ( v3_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f175]) ).
fof(f290,plain,
! [X0] :
( v2_setfam_1(X0)
| ( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v14_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v11_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
& v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f159]) ).
fof(f311,plain,
! [X0] :
( v2_setfam_1(X0)
| ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0)
& k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ) ),
inference(ennf_transformation,[],[f122]) ).
fof(f315,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ( m1_altcat_2(X2,X0)
& v3_altcat_2(X2,X0)
& v2_altcat_1(X2)
& ~ v3_struct_0(X2) ) ) ) ),
inference(ennf_transformation,[],[f125]) ).
fof(f316,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,X0)
| ~ v3_altcat_2(X1,X0)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_altcat_2(X2,X1)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ( m1_altcat_2(X2,X0)
& v3_altcat_2(X2,X0)
& v2_altcat_1(X2)
& ~ v3_struct_0(X2) ) ) ) ),
inference(flattening,[],[f315]) ).
fof(f320,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ! [X3] :
( ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| v3_struct_0(X3)
| ! [X4] :
( ~ 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(ennf_transformation,[],[f128]) ).
fof(f321,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ! [X3] :
( ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| v3_struct_0(X3)
| ! [X4] :
( ~ 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(flattening,[],[f320]) ).
fof(f322,plain,
! [X0] :
( v2_setfam_1(X0)
| r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0)) ),
inference(ennf_transformation,[],[f129]) ).
fof(f339,plain,
( ~ v2_setfam_1(sK6)
& ~ r3_yellow20(k5_waybel34(sK6),k4_waybel34(sK6),k7_waybel34(sK6),k11_waybel34(sK6),k10_waybel34(sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f187]) ).
fof(f380,plain,
~ v2_setfam_1(sK6),
inference(cnf_transformation,[],[f339]) ).
fof(f381,plain,
~ r3_yellow20(k5_waybel34(sK6),k4_waybel34(sK6),k7_waybel34(sK6),k11_waybel34(sK6),k10_waybel34(sK6)),
inference(cnf_transformation,[],[f339]) ).
fof(f434,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f213]) ).
fof(f491,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f492,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f494,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_altcat_1(k10_waybel34(X0)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f495,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k10_waybel34(X0)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f496,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f237]) ).
fof(f497,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f237]) ).
fof(f499,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_altcat_1(k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f237]) ).
fof(f500,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f237]) ).
fof(f505,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f243]) ).
fof(f512,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f244]) ).
fof(f519,plain,
! [X0] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f245]) ).
fof(f525,plain,
! [X0] :
( v1_xboole_0(X0)
| m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f526,plain,
! [X0] :
( v1_xboole_0(X0)
| v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f528,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_altcat_1(k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f529,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f530,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f531,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f533,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f534,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f248]) ).
fof(f593,plain,
! [X0] :
( v2_setfam_1(X0)
| sP4(X0) ),
inference(cnf_transformation,[],[f336]) ).
fof(f612,plain,
! [X0] :
( v2_setfam_1(X0)
| sP5(X0) ),
inference(cnf_transformation,[],[f338]) ).
fof(f615,plain,
! [X0] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f290]) ).
fof(f616,plain,
! [X0] :
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f290]) ).
fof(f695,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(f698,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(f699,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(f704,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(f705,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]) ).
tcf(c_49,negated_conjecture,
~ r3_yellow20(k5_waybel34(sK6),k4_waybel34(sK6),k7_waybel34(sK6),k11_waybel34(sK6),k10_waybel34(sK6)),
inference(cnf_transformation,[],[f381]) ).
tcf(c_50,negated_conjecture,
~ v2_setfam_1(sK6),
inference(cnf_transformation,[],[f380]) ).
tcf(c_96,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f434]) ).
tcf(c_142,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k10_waybel34(X0)) ),
inference(cnf_transformation,[],[f495]) ).
tcf(c_143,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k10_waybel34(X0)) ),
inference(cnf_transformation,[],[f494]) ).
tcf(c_145,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_146,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f491]) ).
tcf(c_147,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f500]) ).
tcf(c_148,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f499]) ).
tcf(c_150,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f497]) ).
tcf(c_151,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f496]) ).
tcf(c_162,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_169,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f512]) ).
tcf(c_172,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f519]) ).
tcf(c_176,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_177,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v2_altcat_1(k8_waybel34(X0)) ),
inference(cnf_transformation,[],[f528]) ).
tcf(c_179,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f526]) ).
tcf(c_180,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f525]) ).
tcf(c_181,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f534]) ).
tcf(c_182,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f533]) ).
tcf(c_184,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f531]) ).
tcf(c_185,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_244,plain,
! [X0: $i] :
( sP4(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f593]) ).
tcf(c_263,plain,
! [X0: $i] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f612]) ).
tcf(c_269,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f616]) ).
tcf(c_270,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f615]) ).
tcf(c_345,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ) ),
inference(cnf_transformation,[],[f695]) ).
tcf(c_349,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v3_struct_0(X0)
| v3_altcat_2(X2,X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X2,X0)
| ~ m1_altcat_2(X0,X1)
| ~ v3_altcat_2(X2,X0)
| ~ v3_altcat_2(X0,X1) ),
inference(cnf_transformation,[],[f699]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v3_struct_0(X0)
| m1_altcat_2(X2,X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X2,X0)
| ~ m1_altcat_2(X0,X1)
| ~ v3_altcat_2(X2,X0)
| ~ v3_altcat_2(X0,X1) ),
inference(cnf_transformation,[],[f698]) ).
tcf(c_353,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v3_struct_0(X4)
| v3_struct_0(X3)
| v3_struct_0(X1)
| v3_struct_0(X0)
| r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X1)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X4)
| ~ v2_altcat_1(X3)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ m1_altcat_2(X4,X1)
| ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X4,X1)
| ~ v3_altcat_2(X3,X0)
| ~ v21_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ r3_yellow20(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f704]) ).
tcf(c_354,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0)) ),
inference(cnf_transformation,[],[f705]) ).
tcf(c_645,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(prop_impl_just,[status(thm)],[c_96]) ).
tcf(c_801,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k10_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_142]) ).
tcf(c_805,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k11_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_147]) ).
tcf(c_819,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_181]) ).
tcf(c_885,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| sP4(X0) ),
inference(prop_impl_just,[status(thm)],[c_244]) ).
tcf(c_886,plain,
! [X0: $i] :
( sP4(X0)
| v2_setfam_1(X0) ),
inference(renaming,[status(thm)],[c_885]) ).
tcf(c_911,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| sP5(X0) ),
inference(prop_impl_just,[status(thm)],[c_263]) ).
tcf(c_912,plain,
! [X0: $i] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(renaming,[status(thm)],[c_911]) ).
tcf(c_929,plain,
! [X0: $i] :
( v2_altcat_1(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_143]) ).
tcf(c_930,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k10_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_929]) ).
tcf(c_933,plain,
! [X0: $i] :
( v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_145]) ).
tcf(c_934,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_933]) ).
tcf(c_935,plain,
! [X0: $i] :
( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_146]) ).
tcf(c_936,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_935]) ).
tcf(c_939,plain,
! [X0: $i] :
( v2_altcat_1(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_148]) ).
tcf(c_940,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k11_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_939]) ).
tcf(c_943,plain,
! [X0: $i] :
( v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_150]) ).
tcf(c_944,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_943]) ).
tcf(c_945,plain,
! [X0: $i] :
( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_151]) ).
tcf(c_946,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_945]) ).
tcf(c_949,plain,
! [X0: $i] :
( v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_269]) ).
tcf(c_950,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_949]) ).
tcf(c_961,plain,
! [X0: $i] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_182]) ).
tcf(c_962,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_961]) ).
tcf(c_965,plain,
! [X0: $i] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_184]) ).
tcf(c_966,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_965]) ).
tcf(c_967,plain,
! [X0: $i] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_185]) ).
tcf(c_968,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_967]) ).
tcf(c_991,plain,
! [X0: $i] :
( ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) )
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_345]) ).
tcf(c_992,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ) ),
inference(renaming,[status(thm)],[c_991]) ).
tcf(c_995,plain,
! [X0: $i] :
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_354]) ).
tcf(c_996,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_995]) ).
tcf(c_6305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v3_struct_0(X5)
| v3_struct_0(X4)
| v3_struct_0(X2)
| v3_struct_0(X1)
| v2_setfam_1(X0)
| r3_yellow20(X2,X1,k15_functor0(X1,X2,X3),X5,X4)
| ~ v12_altcat_1(X2)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X2)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X5)
| ~ v2_altcat_1(X4)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ l2_altcat_1(X2)
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X5,X2)
| ~ m1_altcat_2(X4,X1)
| ~ v3_altcat_2(X5,X2)
| ~ v3_altcat_2(X4,X1)
| ~ v21_functor0(X3,X1,X2)
| ~ m2_functor0(X3,X1,X2)
| ~ r3_yellow20(X1,X2,X3,X4,X5)
| ( k6_waybel34(X0) != X3 )
| ( k4_waybel34(X0) != X1 )
| ( k5_waybel34(X0) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_353,c_950]) ).
tcf(c_6306,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v2_setfam_1(X0)
| v3_struct_0(k4_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)),X2,X1)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2) ),
inference(unflattening,[status(thm)],[c_6305]) ).
tcf(c_9610,plain,
! [X0: $i] :
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_996]) ).
tcf(c_9611,plain,
r3_yellow20(k4_waybel34(sK6),k5_waybel34(sK6),k6_waybel34(sK6),k10_waybel34(sK6),k11_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9610]) ).
tcf(c_9620,plain,
! [X0: $i] :
( ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_992]) ).
tcf(c_9621,plain,
k15_functor0(k4_waybel34(sK6),k5_waybel34(sK6),k6_waybel34(sK6)) = k7_waybel34(sK6),
inference(unflattening,[status(thm)],[c_9620]) ).
tcf(c_9635,plain,
! [X0: $i] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_968]) ).
tcf(c_9636,plain,
m1_altcat_2(k9_waybel34(sK6),k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9635]) ).
tcf(c_9640,plain,
! [X0: $i] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_966]) ).
tcf(c_9641,plain,
v3_altcat_2(k9_waybel34(sK6),k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9640]) ).
tcf(c_9650,plain,
! [X0: $i] :
( v2_altcat_1(k9_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_962]) ).
tcf(c_9651,plain,
v2_altcat_1(k9_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9650]) ).
tcf(c_9655,plain,
! [X0: $i] :
( ~ v3_struct_0(k9_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_819]) ).
tcf(c_9656,plain,
~ v3_struct_0(k9_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9655]) ).
tcf(c_9670,plain,
! [X0: $i] :
( m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_946]) ).
tcf(c_9671,plain,
m1_altcat_2(k11_waybel34(sK6),k9_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9670]) ).
tcf(c_9675,plain,
! [X0: $i] :
( v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_944]) ).
tcf(c_9676,plain,
v3_altcat_2(k11_waybel34(sK6),k9_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9675]) ).
tcf(c_9685,plain,
! [X0: $i] :
( v2_altcat_1(k11_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_940]) ).
tcf(c_9686,plain,
v2_altcat_1(k11_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9685]) ).
tcf(c_9690,plain,
! [X0: $i] :
( ~ v3_struct_0(k11_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_805]) ).
tcf(c_9691,plain,
~ v3_struct_0(k11_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9690]) ).
tcf(c_9695,plain,
! [X0: $i] :
( m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_936]) ).
tcf(c_9696,plain,
m1_altcat_2(k10_waybel34(sK6),k8_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9695]) ).
tcf(c_9700,plain,
! [X0: $i] :
( v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_934]) ).
tcf(c_9701,plain,
v3_altcat_2(k10_waybel34(sK6),k8_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9700]) ).
tcf(c_9710,plain,
! [X0: $i] :
( v2_altcat_1(k10_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_930]) ).
tcf(c_9711,plain,
v2_altcat_1(k10_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9710]) ).
tcf(c_9715,plain,
! [X0: $i] :
( ~ v3_struct_0(k10_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_801]) ).
tcf(c_9716,plain,
~ v3_struct_0(k10_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9715]) ).
tcf(c_9720,plain,
! [X0: $i] :
( ~ v1_xboole_0(X0)
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_645]) ).
tcf(c_9721,plain,
~ v1_xboole_0(sK6),
inference(unflattening,[status(thm)],[c_9720]) ).
tcf(c_23122,definition,
iPr_def_10 = k5_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_23123,definition,
iPr_def_11 = k4_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_23126,definition,
iPr_def_14 = k10_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_23127,definition,
iPr_def_15 = k8_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_23128,definition,
iPr_def_16 = k11_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_23129,definition,
iPr_def_17 = k9_waybel34(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_23135,plain,
~ v1_xboole_0(sK6),
inference(demodulation,[status(thm)],[c_9721]) ).
tcf(c_23136,plain,
~ v3_struct_0(iPr_def_14),
inference(demodulation,[status(thm)],[c_9716,c_23126]) ).
tcf(c_23137,plain,
v2_altcat_1(iPr_def_14),
inference(demodulation,[status(thm)],[c_9711]) ).
tcf(c_23139,plain,
v3_altcat_2(iPr_def_14,iPr_def_15),
inference(demodulation,[status(thm)],[c_9701,c_23127]) ).
tcf(c_23140,plain,
m1_altcat_2(iPr_def_14,iPr_def_15),
inference(demodulation,[status(thm)],[c_9696]) ).
tcf(c_23141,plain,
~ v3_struct_0(iPr_def_16),
inference(demodulation,[status(thm)],[c_9691,c_23128]) ).
tcf(c_23142,plain,
v2_altcat_1(iPr_def_16),
inference(demodulation,[status(thm)],[c_9686]) ).
tcf(c_23144,plain,
v3_altcat_2(iPr_def_16,iPr_def_17),
inference(demodulation,[status(thm)],[c_9676,c_23129]) ).
tcf(c_23145,plain,
m1_altcat_2(iPr_def_16,iPr_def_17),
inference(demodulation,[status(thm)],[c_9671]) ).
tcf(c_23148,plain,
~ v3_struct_0(iPr_def_17),
inference(demodulation,[status(thm)],[c_9656]) ).
tcf(c_23149,plain,
v2_altcat_1(iPr_def_17),
inference(demodulation,[status(thm)],[c_9651]) ).
tcf(c_23151,plain,
v3_altcat_2(iPr_def_17,iPr_def_10),
inference(demodulation,[status(thm)],[c_9641]) ).
tcf(c_23152,plain,
m1_altcat_2(iPr_def_17,iPr_def_10),
inference(demodulation,[status(thm)],[c_9636]) ).
tcf(c_23157,plain,
r3_yellow20(iPr_def_11,iPr_def_10,iPr_def_13,iPr_def_14,iPr_def_16),
inference(demodulation,[status(thm)],[c_9611]) ).
tcf(c_23193,negated_conjecture,
~ r3_yellow20(iPr_def_10,iPr_def_11,iPr_def_12,iPr_def_16,iPr_def_14),
inference(demodulation,[status(thm)],[c_49]) ).
tcf(c_28747,plain,
( v1_xboole_0(sK6)
| l2_altcat_1(iPr_def_11) ),
inference(superposition,[status(thm)],[c_23123,c_162]) ).
tcf(c_28748,plain,
l2_altcat_1(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_28747,c_23135]) ).
tcf(c_28778,plain,
( v1_xboole_0(sK6)
| l2_altcat_1(iPr_def_10) ),
inference(superposition,[status(thm)],[c_23122,c_169]) ).
tcf(c_28779,plain,
l2_altcat_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_28778,c_23135]) ).
tcf(c_28784,plain,
( v1_xboole_0(sK6)
| v2_altcat_1(iPr_def_15) ),
inference(superposition,[status(thm)],[c_23127,c_177]) ).
tcf(c_28785,plain,
v2_altcat_1(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_28784,c_23135]) ).
tcf(c_28943,plain,
( v1_xboole_0(sK6)
| ~ v3_struct_0(iPr_def_15) ),
inference(superposition,[status(thm)],[c_23127,c_176]) ).
tcf(c_28944,plain,
~ v3_struct_0(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_28943,c_23135]) ).
tcf(c_29047,plain,
( v1_xboole_0(sK6)
| v3_altcat_2(k8_waybel34(sK6),iPr_def_11) ),
inference(superposition,[status(thm)],[c_23123,c_179]) ).
tcf(c_29048,plain,
( v1_xboole_0(sK6)
| v3_altcat_2(iPr_def_15,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_29047,c_23127]) ).
tcf(c_29049,plain,
v3_altcat_2(iPr_def_15,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_29048,c_23135]) ).
tcf(c_29057,plain,
( v1_xboole_0(sK6)
| m1_altcat_2(k8_waybel34(sK6),iPr_def_11) ),
inference(superposition,[status(thm)],[c_23123,c_180]) ).
tcf(c_29058,plain,
( v1_xboole_0(sK6)
| m1_altcat_2(iPr_def_15,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_29057,c_23127]) ).
tcf(c_29059,plain,
m1_altcat_2(iPr_def_15,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_29058,c_23135]) ).
tcf(c_34231,plain,
! [X0: $i] :
( v3_struct_0(iPr_def_17)
| v3_struct_0(iPr_def_10)
| v3_struct_0(X0)
| v3_altcat_2(X0,iPr_def_10)
| ~ v12_altcat_1(iPr_def_10)
| ~ v11_altcat_1(iPr_def_10)
| ~ v2_altcat_1(iPr_def_17)
| ~ v2_altcat_1(iPr_def_10)
| ~ l2_altcat_1(iPr_def_10)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(iPr_def_17,iPr_def_10)
| ~ m1_altcat_2(X0,iPr_def_17)
| ~ v3_altcat_2(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_23151,c_349]) ).
tcf(c_34232,plain,
! [X0: $i] :
( v3_struct_0(iPr_def_15)
| v3_struct_0(iPr_def_11)
| v3_struct_0(X0)
| v3_altcat_2(X0,iPr_def_11)
| ~ v12_altcat_1(iPr_def_11)
| ~ v11_altcat_1(iPr_def_11)
| ~ v2_altcat_1(iPr_def_15)
| ~ v2_altcat_1(iPr_def_11)
| ~ l2_altcat_1(iPr_def_11)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(iPr_def_15,iPr_def_11)
| ~ m1_altcat_2(X0,iPr_def_15)
| ~ v3_altcat_2(X0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_29049,c_349]) ).
tcf(c_34352,plain,
! [X0: $i] :
( v3_struct_0(iPr_def_17)
| v3_struct_0(iPr_def_10)
| v3_struct_0(X0)
| m1_altcat_2(X0,iPr_def_10)
| ~ v12_altcat_1(iPr_def_10)
| ~ v11_altcat_1(iPr_def_10)
| ~ v2_altcat_1(iPr_def_17)
| ~ v2_altcat_1(iPr_def_10)
| ~ l2_altcat_1(iPr_def_10)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(iPr_def_17,iPr_def_10)
| ~ m1_altcat_2(X0,iPr_def_17)
| ~ v3_altcat_2(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_23151,c_350]) ).
tcf(c_34353,plain,
! [X0: $i] :
( v3_struct_0(iPr_def_15)
| v3_struct_0(iPr_def_11)
| v3_struct_0(X0)
| m1_altcat_2(X0,iPr_def_11)
| ~ v12_altcat_1(iPr_def_11)
| ~ v11_altcat_1(iPr_def_11)
| ~ v2_altcat_1(iPr_def_15)
| ~ v2_altcat_1(iPr_def_11)
| ~ l2_altcat_1(iPr_def_11)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(iPr_def_15,iPr_def_11)
| ~ m1_altcat_2(X0,iPr_def_15)
| ~ v3_altcat_2(X0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_29049,c_350]) ).
fof(f335,definition,
! [X0] :
( ~ sP4(X0)
| ( v3_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f336,plain,
! [X0] :
( v2_setfam_1(X0)
| sP4(X0) ),
inference(definition_folding,[],[f286,f335]) ).
fof(f337,definition,
! [X0] :
( ~ sP5(X0)
| ( v3_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f338,plain,
! [X0] :
( v2_setfam_1(X0)
| sP5(X0) ),
inference(definition_folding,[],[f287,f337]) ).
fof(f359,plain,
! [X0] :
( ~ sP4(X0)
| ( v3_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(nnf_transformation,[],[f335]) ).
fof(f360,plain,
! [X0] :
( ~ sP5(X0)
| ( v3_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(nnf_transformation,[],[f337]) ).
fof(f587,plain,
! [X0] :
( ~ sP4(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f359]) ).
fof(f588,plain,
! [X0] :
( ~ sP4(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f359]) ).
fof(f591,plain,
! [X0] :
( ~ sP4(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f359]) ).
fof(f592,plain,
! [X0] :
( ~ sP4(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f359]) ).
fof(f606,plain,
! [X0] :
( ~ sP5(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f360]) ).
fof(f607,plain,
! [X0] :
( ~ sP5(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f360]) ).
fof(f610,plain,
! [X0] :
( ~ sP5(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f360]) ).
fof(f611,plain,
! [X0] :
( ~ sP5(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_232,plain,
! [X0: $i] :
( ~ sP4(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f592]) ).
tcf(c_233,plain,
! [X0: $i] :
( v2_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f591]) ).
tcf(c_236,plain,
! [X0: $i] :
( v11_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f588]) ).
tcf(c_237,plain,
! [X0: $i] :
( v12_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f587]) ).
tcf(c_251,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f611]) ).
tcf(c_252,plain,
! [X0: $i] :
( v2_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f610]) ).
tcf(c_255,plain,
! [X0: $i] :
( v11_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f607]) ).
tcf(c_256,plain,
! [X0: $i] :
( v12_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f606]) ).
tcf(c_811,plain,
! [X0: $i] :
( ~ sP4(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_232]) ).
tcf(c_815,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_251]) ).
tcf(c_863,plain,
! [X0: $i] :
( v2_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(prop_impl_just,[status(thm)],[c_233]) ).
tcf(c_867,plain,
! [X0: $i] :
( v11_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(prop_impl_just,[status(thm)],[c_236]) ).
tcf(c_869,plain,
! [X0: $i] :
( v12_altcat_1(k4_waybel34(X0))
| ~ sP4(X0) ),
inference(prop_impl_just,[status(thm)],[c_237]) ).
tcf(c_889,plain,
! [X0: $i] :
( v2_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(prop_impl_just,[status(thm)],[c_252]) ).
tcf(c_893,plain,
! [X0: $i] :
( v11_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(prop_impl_just,[status(thm)],[c_255]) ).
tcf(c_895,plain,
! [X0: $i] :
( v12_altcat_1(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(prop_impl_just,[status(thm)],[c_256]) ).
tcf(c_5369,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v12_altcat_1(k4_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_886,c_869]) ).
tcf(c_5370,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5369]) ).
tcf(c_5378,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v11_altcat_1(k4_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_886,c_867]) ).
tcf(c_5379,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5378]) ).
tcf(c_5405,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k4_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_886,c_863]) ).
tcf(c_5406,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5405]) ).
tcf(c_5414,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k4_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_886,c_811]) ).
tcf(c_5415,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5414]) ).
tcf(c_5501,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v12_altcat_1(k5_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_912,c_895]) ).
tcf(c_5502,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5501]) ).
tcf(c_5510,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v11_altcat_1(k5_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_912,c_893]) ).
tcf(c_5511,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5510]) ).
tcf(c_5537,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k5_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_912,c_889]) ).
tcf(c_5538,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5537]) ).
tcf(c_5546,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k5_waybel34(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_912,c_815]) ).
tcf(c_5547,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(unflattening,[status(thm)],[c_5546]) ).
tcf(c_6308,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v2_setfam_1(X0)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)),X2,X1)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_6306,c_169,c_162,c_96,c_270,c_172,c_5370,c_5379,c_5406,c_5415,c_5502,c_5511,c_5538,c_5547,c_6306]) ).
tcf(c_9412,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| r3_yellow20(k5_waybel34(X0),k4_waybel34(X0),k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)),X2,X1)
| ~ v2_altcat_1(X2)
| ~ v2_altcat_1(X1)
| ~ m1_altcat_2(X2,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| ~ v3_altcat_2(X2,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),X1,X2)
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_6308]) ).
tcf(c_9413,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r3_yellow20(k5_waybel34(sK6),k4_waybel34(sK6),k15_functor0(k4_waybel34(sK6),k5_waybel34(sK6),k6_waybel34(sK6)),X1,X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X1,k5_waybel34(sK6))
| ~ m1_altcat_2(X0,k4_waybel34(sK6))
| ~ v3_altcat_2(X1,k5_waybel34(sK6))
| ~ v3_altcat_2(X0,k4_waybel34(sK6))
| ~ r3_yellow20(k4_waybel34(sK6),k5_waybel34(sK6),k6_waybel34(sK6),X0,X1) ),
inference(unflattening,[status(thm)],[c_9412]) ).
tcf(c_9490,plain,
! [X0: $i] :
( ~ v3_struct_0(k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5547]) ).
tcf(c_9491,plain,
~ v3_struct_0(k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9490]) ).
tcf(c_9495,plain,
! [X0: $i] :
( v2_altcat_1(k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5538]) ).
tcf(c_9496,plain,
v2_altcat_1(k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9495]) ).
tcf(c_9510,plain,
! [X0: $i] :
( v11_altcat_1(k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5511]) ).
tcf(c_9511,plain,
v11_altcat_1(k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9510]) ).
tcf(c_9515,plain,
! [X0: $i] :
( v12_altcat_1(k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5502]) ).
tcf(c_9516,plain,
v12_altcat_1(k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9515]) ).
tcf(c_9550,plain,
! [X0: $i] :
( ~ v3_struct_0(k4_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5415]) ).
tcf(c_9551,plain,
~ v3_struct_0(k4_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9550]) ).
tcf(c_9555,plain,
! [X0: $i] :
( v2_altcat_1(k4_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5406]) ).
tcf(c_9556,plain,
v2_altcat_1(k4_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9555]) ).
tcf(c_9570,plain,
! [X0: $i] :
( v11_altcat_1(k4_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5379]) ).
tcf(c_9571,plain,
v11_altcat_1(k4_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9570]) ).
tcf(c_9575,plain,
! [X0: $i] :
( v12_altcat_1(k4_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_5370]) ).
tcf(c_9576,plain,
v12_altcat_1(k4_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_9575]) ).
tcf(c_17090,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r3_yellow20(k5_waybel34(sK6),k4_waybel34(sK6),k7_waybel34(sK6),X1,X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X1,k5_waybel34(sK6))
| ~ m1_altcat_2(X0,k4_waybel34(sK6))
| ~ v3_altcat_2(X1,k5_waybel34(sK6))
| ~ v3_altcat_2(X0,k4_waybel34(sK6))
| ~ r3_yellow20(k4_waybel34(sK6),k5_waybel34(sK6),k6_waybel34(sK6),X0,X1) ),
inference(light_normalisation,[status(thm)],[c_9413,c_9621]) ).
tcf(c_23134,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r3_yellow20(iPr_def_10,iPr_def_11,iPr_def_12,X1,X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X1,iPr_def_10)
| ~ m1_altcat_2(X0,iPr_def_11)
| ~ v3_altcat_2(X1,iPr_def_10)
| ~ v3_altcat_2(X0,iPr_def_11)
| ~ r3_yellow20(iPr_def_11,iPr_def_10,iPr_def_13,X0,X1) ),
inference(demodulation,[status(thm)],[c_17090]) ).
tcf(c_23164,plain,
v12_altcat_1(iPr_def_11),
inference(demodulation,[status(thm)],[c_9576]) ).
tcf(c_23165,plain,
v11_altcat_1(iPr_def_11),
inference(demodulation,[status(thm)],[c_9571]) ).
tcf(c_23168,plain,
v2_altcat_1(iPr_def_11),
inference(demodulation,[status(thm)],[c_9556]) ).
tcf(c_23169,plain,
~ v3_struct_0(iPr_def_11),
inference(demodulation,[status(thm)],[c_9551]) ).
tcf(c_23176,plain,
v12_altcat_1(iPr_def_10),
inference(demodulation,[status(thm)],[c_9516]) ).
tcf(c_23177,plain,
v11_altcat_1(iPr_def_10),
inference(demodulation,[status(thm)],[c_9511]) ).
tcf(c_23180,plain,
v2_altcat_1(iPr_def_10),
inference(demodulation,[status(thm)],[c_9496]) ).
tcf(c_23181,plain,
~ v3_struct_0(iPr_def_10),
inference(demodulation,[status(thm)],[c_9491]) ).
tcf(c_28688,plain,
( v3_struct_0(iPr_def_16)
| v3_struct_0(iPr_def_14)
| r3_yellow20(iPr_def_10,iPr_def_11,iPr_def_12,iPr_def_16,iPr_def_14)
| ~ v2_altcat_1(iPr_def_16)
| ~ v2_altcat_1(iPr_def_14)
| ~ m1_altcat_2(iPr_def_16,iPr_def_10)
| ~ m1_altcat_2(iPr_def_14,iPr_def_11)
| ~ v3_altcat_2(iPr_def_16,iPr_def_10)
| ~ v3_altcat_2(iPr_def_14,iPr_def_11) ),
inference(superposition,[status(thm)],[c_23157,c_23134]) ).
tcf(c_28689,plain,
( ~ m1_altcat_2(iPr_def_16,iPr_def_10)
| ~ m1_altcat_2(iPr_def_14,iPr_def_11)
| ~ v3_altcat_2(iPr_def_16,iPr_def_10)
| ~ v3_altcat_2(iPr_def_14,iPr_def_11) ),
inference(forward_subsumption_resolution,[status(thm)],[c_28688,c_23141,c_23136,c_23193,c_23142,c_23137]) ).
tcf(c_34233,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_altcat_2(X0,iPr_def_11)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X0,iPr_def_15)
| ~ v3_altcat_2(X0,iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34232,c_28944,c_23169,c_23164,c_23165,c_28785,c_23168,c_28748,c_29059]) ).
tcf(c_34239,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_altcat_2(X0,iPr_def_10)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X0,iPr_def_17)
| ~ v3_altcat_2(X0,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34231,c_23148,c_23181,c_23176,c_23177,c_23149,c_23180,c_28779,c_23152]) ).
tcf(c_34354,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_altcat_2(X0,iPr_def_11)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X0,iPr_def_15)
| ~ v3_altcat_2(X0,iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34353,c_28944,c_23169,c_23164,c_23165,c_28785,c_23168,c_28748,c_29059]) ).
tcf(c_34360,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_altcat_2(X0,iPr_def_10)
| ~ v2_altcat_1(X0)
| ~ m1_altcat_2(X0,iPr_def_17)
| ~ v3_altcat_2(X0,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34352,c_23148,c_23181,c_23176,c_23177,c_23149,c_23180,c_28779,c_23152]) ).
tcf(c_34516,plain,
( v3_struct_0(iPr_def_14)
| v3_altcat_2(iPr_def_14,iPr_def_11)
| ~ v2_altcat_1(iPr_def_14)
| ~ m1_altcat_2(iPr_def_14,iPr_def_15) ),
inference(superposition,[status(thm)],[c_23139,c_34233]) ).
tcf(c_34517,plain,
v3_altcat_2(iPr_def_14,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_34516,c_23136,c_23137,c_23140]) ).
tcf(c_34523,plain,
( ~ m1_altcat_2(iPr_def_16,iPr_def_10)
| ~ m1_altcat_2(iPr_def_14,iPr_def_11)
| ~ v3_altcat_2(iPr_def_16,iPr_def_10) ),
inference(backward_subsumption_resolution,[status(thm)],[c_28689,c_34517]) ).
tcf(c_34590,plain,
( v3_struct_0(iPr_def_16)
| v3_altcat_2(iPr_def_16,iPr_def_10)
| ~ v2_altcat_1(iPr_def_16)
| ~ m1_altcat_2(iPr_def_16,iPr_def_17) ),
inference(superposition,[status(thm)],[c_23144,c_34239]) ).
tcf(c_34591,plain,
v3_altcat_2(iPr_def_16,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_34590,c_23141,c_23142,c_23145]) ).
tcf(c_35043,plain,
( v3_struct_0(iPr_def_14)
| m1_altcat_2(iPr_def_14,iPr_def_11)
| ~ v2_altcat_1(iPr_def_14)
| ~ m1_altcat_2(iPr_def_14,iPr_def_15) ),
inference(superposition,[status(thm)],[c_23139,c_34354]) ).
tcf(c_35044,plain,
m1_altcat_2(iPr_def_14,iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_35043,c_23136,c_23137,c_23140]) ).
tcf(c_35067,plain,
( v3_struct_0(iPr_def_16)
| m1_altcat_2(iPr_def_16,iPr_def_10)
| ~ v2_altcat_1(iPr_def_16)
| ~ m1_altcat_2(iPr_def_16,iPr_def_17) ),
inference(superposition,[status(thm)],[c_23144,c_34360]) ).
tcf(c_35068,plain,
m1_altcat_2(iPr_def_16,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_35067,c_23141,c_23142,c_23145]) ).
tcf(c_35074,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_35068,c_35044,c_34591,c_34523]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT377+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Wed Sep 23 21:28:37 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.32 Running first-order theorem proving
% 0.02/0.32 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.33
% 0.08/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.33
% 0.08/0.33 % Detected problem language: tptp
% 0.08/0.34 % Proving...
% 7.68/1.50 % SZS status Started for theBenchmark.p
% 7.68/1.50 % SZS status Theorem for theBenchmark.p
% 7.68/1.50
% 7.68/1.50 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.68/1.50
% 7.68/1.50 % ------ iProver source info
% 7.68/1.50
% 7.68/1.50 % git: date: 2026-07-19 20:42:38 +0200
% 7.68/1.50 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.68/1.50 % git: non_committed_changes: false
% 7.68/1.50
% 7.68/1.50 % ------ Parsing...
% 7.68/1.50 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.68/1.50
% 7.68/1.50 % ------ Preprocessing... sup_sim: 0 sf_s rm: 55 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 4 sf_s rm: 14 0s sf_e pe_s pe_e %
% 7.68/1.50
% 7.68/1.50 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 7.68/1.50
% 7.68/1.50 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 7.68/1.50 % ------ Proving...
% 7.68/1.50 % ------ Problem Properties
% 7.68/1.50
% 7.68/1.50 %
% 7.68/1.50 % clauses 307
% 7.68/1.50 % conjectures 1
% 7.68/1.50 % EPR 159
% 7.68/1.50 % Horn 249
% 7.68/1.50 % unary 161
% 7.68/1.50 % binary 70
% 7.68/1.50 % lits 807
% 7.68/1.50 % lits eq 33
% 7.68/1.50 % fd_pure 0
% 7.68/1.50 % fd_pseudo 0
% 7.68/1.50 % fd_cond 1
% 7.68/1.50 % fd_pseudo_cond 8
% 7.68/1.50 % AC symbols 0
% 7.68/1.50
% 7.68/1.50 % ------ Schedule dynamic 5 is on
% 7.68/1.50
% 7.68/1.50 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 7.68/1.50
% 7.68/1.50
% 7.68/1.50 % ------
% 7.68/1.50 % Current options:
% 7.68/1.50 % ------
% 7.68/1.50
% 7.68/1.50
% 7.68/1.50 %
% 7.68/1.50
% 7.68/1.50 % ------ Proving...
% 7.68/1.50 %
% 7.68/1.50
% 7.68/1.50 % SZS status Theorem for theBenchmark.p
% 7.68/1.50
% 7.68/1.50 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.68/1.50
% 7.68/1.50
%------------------------------------------------------------------------------