%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT361+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n006.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:38 PM UTC 2026
% Result : Theorem 8.47s 1.90s
% Output : CNFRefutation 8.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 14
% Syntax : Number of formulae : 165 ( 13 unt; 0 def)
% Number of atoms : 696 ( 103 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 862 ( 331 ~; 396 |; 106 &)
% ( 0 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-5 aty)
% Number of variables : 188 ( 0 sgn 187 !; 1 ?; 97 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( k13_functor0(k4_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0),k6_waybel34(X0),k7_waybel34(X0)) = k12_functor0(k4_waybel34(X0))
& k13_functor0(k5_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0),k7_waybel34(X0),k6_waybel34(X0)) = k12_functor0(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> ( k13_functor0(k4_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0),k6_waybel34(X0),k7_waybel34(X0)) = k12_functor0(k4_waybel34(X0))
& k13_functor0(k5_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0),k7_waybel34(X0),k6_waybel34(X0)) = k12_functor0(k5_waybel34(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( l2_functor0(X2,X0,X1)
& l1_altcat_1(X1)
& l1_altcat_1(X0) )
=> ( v9_functor0(X2,X0,X1)
=> X2 = g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',abstractness_v9_functor0) ).
fof(f26,axiom,
! [X0] :
( l2_altcat_1(X0)
=> ( ( v12_altcat_1(X0)
& ~ v3_struct_0(X0) )
=> ( v1_altcat_2(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_functor0) ).
fof(f29,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f52,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/sandbox/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f53,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/sandbox/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f54,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/sandbox/benchmark/theBenchmark.p',dt_k6_waybel34) ).
fof(f55,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v16_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_waybel34) ).
fof(f59,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f65,axiom,
! [X0,X1] :
( ( l2_altcat_1(X1)
& v12_altcat_1(X1)
& ~ v3_struct_0(X1)
& l2_altcat_1(X0)
& v12_altcat_1(X0)
& v2_altcat_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X2] :
( m2_functor0(X2,X0,X1)
=> l2_functor0(X2,X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_functor0) ).
fof(f101,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/sandbox/benchmark/theBenchmark.p',fc7_waybel34) ).
fof(f102,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v16_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v14_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v12_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v11_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v8_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v6_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc8_waybel34) ).
fof(f129,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/sandbox/benchmark/theBenchmark.p',t18_waybel34) ).
fof(f131,axiom,
! [X0] :
( ( l2_altcat_1(X0)
& v1_altcat_2(X0)
& v12_altcat_1(X0)
& v2_altcat_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l2_altcat_1(X1)
& v1_altcat_2(X1)
& v12_altcat_1(X1)
& v2_altcat_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( l2_functor0(X2,X0,X1)
& v8_functor0(X2,X0,X1) )
=> ( v21_functor0(X2,X0,X1)
=> ! [X3] :
( ( l2_functor0(X3,X1,X0)
& v8_functor0(X3,X1,X0) )
=> ( g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3)) = k15_functor0(X0,X1,X2)
=> k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_functor1) ).
fof(f139,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(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(pure_predicate_removal,[],[f52]) ).
fof(f140,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(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(pure_predicate_removal,[],[f53]) ).
fof(f141,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k4_waybel34(X0))
& v12_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,[],[f139]) ).
fof(f142,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k5_waybel34(X0))
& v12_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,[],[f140]) ).
fof(f143,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f141]) ).
fof(f144,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f142]) ).
fof(f145,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ( k13_functor0(k4_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0),k6_waybel34(X0),k7_waybel34(X0)) != k12_functor0(k4_waybel34(X0))
| k13_functor0(k5_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0),k7_waybel34(X0),k6_waybel34(X0)) != k12_functor0(k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f147,plain,
! [X0] :
( v1_xboole_0(X0)
| ( l2_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f144]) ).
fof(f149,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f150,plain,
! [X0] :
( v1_xboole_0(X0)
| ( l2_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& ~ v3_struct_0(k4_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f143]) ).
fof(f151,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,[],[f129]) ).
fof(f152,plain,
! [X0] :
( v2_setfam_1(X0)
| ( v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v16_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v14_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v12_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v11_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v8_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v6_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f102]) ).
fof(f153,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v16_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
& v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f55]) ).
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))
& 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)) ) ),
inference(ennf_transformation,[],[f101]) ).
fof(f155,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,[],[f54]) ).
fof(f170,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ~ v1_altcat_2(X1)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ! [X3] :
( ~ l2_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| k15_functor0(X0,X1,X2) != g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3))
| k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1) ) ) ) ),
inference(ennf_transformation,[],[f131]) ).
fof(f171,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ~ v1_altcat_2(X1)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ! [X3] :
( ~ l2_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| k15_functor0(X0,X1,X2) != g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3))
| k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1) ) ) ) ),
inference(flattening,[],[f170]) ).
fof(f176,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f177,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v3_struct_0(X0)
| ( v1_altcat_2(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f26]) ).
fof(f178,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v3_struct_0(X0)
| ( v1_altcat_2(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f177]) ).
fof(f202,plain,
! [X0,X1] :
( ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( ~ m2_functor0(X2,X0,X1)
| l2_functor0(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f203,plain,
! [X0,X1] :
( ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( ~ m2_functor0(X2,X0,X1)
| l2_functor0(X2,X0,X1) ) ),
inference(flattening,[],[f202]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| ~ l1_altcat_1(X0)
| ~ v9_functor0(X2,X0,X1)
| X2 = g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f215,plain,
! [X0,X1,X2] :
( ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| ~ l1_altcat_1(X0)
| ~ v9_functor0(X2,X0,X1)
| X2 = g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) ),
inference(flattening,[],[f214]) ).
fof(f253,plain,
( ~ v2_setfam_1(sK0)
& ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),k6_waybel34(sK0),k7_waybel34(sK0)) != k12_functor0(k4_waybel34(sK0))
| k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),k7_waybel34(sK0),k6_waybel34(sK0)) != k12_functor0(k5_waybel34(sK0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f145]) ).
fof(f279,plain,
~ v2_setfam_1(sK0),
inference(cnf_transformation,[],[f253]) ).
fof(f280,plain,
( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),k6_waybel34(sK0),k7_waybel34(sK0)) != k12_functor0(k4_waybel34(sK0))
| k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),k7_waybel34(sK0),k6_waybel34(sK0)) != k12_functor0(k5_waybel34(sK0)) ),
inference(cnf_transformation,[],[f253]) ).
fof(f282,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f283,plain,
! [X0] :
( v1_xboole_0(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f284,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f285,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f289,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f290,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f291,plain,
! [X0] :
( v1_xboole_0(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f292,plain,
! [X0] :
( v1_xboole_0(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f293,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f294,plain,
! [X0] :
( v2_setfam_1(X0)
| k6_waybel34(X0) = k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f295,plain,
! [X0] :
( v2_setfam_1(X0)
| k7_waybel34(X0) = k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f296,plain,
! [X0] :
( v2_setfam_1(X0)
| v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f152]) ).
fof(f302,plain,
! [X0] :
( v2_setfam_1(X0)
| v8_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f152]) ).
fof(f304,plain,
! [X0] :
( v2_setfam_1(X0)
| m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f306,plain,
! [X0] :
( v2_setfam_1(X0)
| v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f307,plain,
! [X0] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f313,plain,
! [X0] :
( v2_setfam_1(X0)
| v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f315,plain,
! [X0] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f155]) ).
fof(f317,plain,
! [X0] :
( v2_setfam_1(X0)
| v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f155]) ).
fof(f332,plain,
! [X2,X3,X0,X1] :
( ~ l2_altcat_1(X0)
| ~ v1_altcat_2(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X1)
| ~ v1_altcat_2(X1)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| ~ l2_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| k15_functor0(X0,X1,X2) != g2_functor0(X1,X0,u1_functor0(X1,X0,X3),u2_functor0(X1,X0,X3))
| k13_functor0(X1,X0,X1,X3,X2) = k12_functor0(X1) ),
inference(cnf_transformation,[],[f171]) ).
fof(f338,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f339,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v3_struct_0(X0)
| v1_altcat_2(X0) ),
inference(cnf_transformation,[],[f178]) ).
fof(f375,plain,
! [X2,X0,X1] :
( ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ m2_functor0(X2,X0,X1)
| l2_functor0(X2,X0,X1) ),
inference(cnf_transformation,[],[f203]) ).
fof(f390,plain,
! [X2,X0,X1] :
( ~ l2_functor0(X2,X0,X1)
| ~ l1_altcat_1(X1)
| ~ l1_altcat_1(X0)
| ~ v9_functor0(X2,X0,X1)
| g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) = X2 ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_49,negated_conjecture,
( ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),k6_waybel34(sK0),k7_waybel34(sK0)) != k12_functor0(k4_waybel34(sK0)) )
| ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),k7_waybel34(sK0),k6_waybel34(sK0)) != k12_functor0(k5_waybel34(sK0)) ) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_50,negated_conjecture,
~ v2_setfam_1(sK0),
inference(cnf_transformation,[],[f279]) ).
tcf(c_52,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_53,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_54,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_55,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_59,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_60,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ v3_struct_0(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_61,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_62,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_63,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l2_altcat_1(k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_64,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_65,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) ) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_67,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v8_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_73,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_74,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_76,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_78,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v8_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_84,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_85,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_87,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ v1_altcat_2(X1)
| ~ v1_altcat_2(X0)
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ v21_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| ~ v8_functor0(X2,X0,X1)
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) ) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_108,plain,
! [X0: $i] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_109,plain,
! [X0: $i] :
( v1_altcat_2(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| l2_functor0(X0,X1,X2)
| ~ l2_altcat_1(X2)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X2)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| ~ m2_functor0(X0,X1,X2) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( g2_functor0(X1,X2,u1_functor0(X1,X2,X0),u2_functor0(X1,X2,X0)) = X0 )
| ~ l1_altcat_1(X2)
| ~ l1_altcat_1(X1)
| ~ l2_functor0(X0,X1,X2)
| ~ v9_functor0(X0,X1,X2) ),
inference(cnf_transformation,[],[f390]) ).
tcf(c_217,plain,
( v1_xboole_0(sK0)
| l2_altcat_1(k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_218,plain,
( v1_xboole_0(sK0)
| v12_altcat_1(k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_219,plain,
( v1_xboole_0(sK0)
| v2_altcat_1(k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_220,plain,
( v2_setfam_1(sK0)
| ~ v1_xboole_0(sK0) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_221,plain,
( v1_xboole_0(sK0)
| l2_altcat_1(k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_222,plain,
( v1_xboole_0(sK0)
| v12_altcat_1(k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_223,plain,
( v1_xboole_0(sK0)
| v2_altcat_1(k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_226,plain,
( v1_xboole_0(sK0)
| ~ v3_struct_0(k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_229,plain,
( v1_xboole_0(sK0)
| ~ v3_struct_0(k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_244,plain,
( v2_setfam_1(sK0)
| v8_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_253,plain,
( v2_setfam_1(sK0)
| v8_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ v1_altcat_2(X1)
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) )
| ~ v8_functor0(X2,X0,X1)
| ~ v8_functor0(X3,X1,X0)
| ~ v21_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ l2_functor0(X3,X1,X0)
| ~ v2_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ l2_altcat_1(X1) ),
inference(global_subsumption_just,[status(thm)],[c_102,c_109,c_102]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ v1_altcat_2(X1)
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ v21_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| ~ v8_functor0(X2,X0,X1)
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) ) ),
inference(renaming,[status(thm)],[c_358]) ).
tcf(c_434,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_64]) ).
tcf(c_435,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_434]) ).
tcf(c_436,plain,
! [X0: $i] :
( ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) )
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_65]) ).
tcf(c_437,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) ) ),
inference(renaming,[status(thm)],[c_436]) ).
tcf(c_442,plain,
! [X0: $i] :
( v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_74]) ).
tcf(c_443,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_442]) ).
tcf(c_452,plain,
! [X0: $i] :
( v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_73]) ).
tcf(c_453,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_452]) ).
tcf(c_454,plain,
! [X0: $i] :
( m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_76]) ).
tcf(c_455,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_454]) ).
tcf(c_460,plain,
! [X0: $i] :
( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_85]) ).
tcf(c_461,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_460]) ).
tcf(c_470,plain,
! [X0: $i] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_84]) ).
tcf(c_471,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_470]) ).
tcf(c_472,plain,
! [X0: $i] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_87]) ).
tcf(c_473,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(renaming,[status(thm)],[c_472]) ).
tcf(c_1117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ v21_functor0(X3,X1,X0)
| ~ v8_functor0(X3,X1,X0)
| ~ v8_functor0(X2,X0,X1)
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_359,c_109]) ).
tcf(c_3549,plain,
! [X0: $i] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_473]) ).
tcf(c_3550,plain,
m2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3549]) ).
tcf(c_3554,plain,
! [X0: $i] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_471]) ).
tcf(c_3555,plain,
v21_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3554]) ).
tcf(c_3579,plain,
! [X0: $i] :
( v9_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_461]) ).
tcf(c_3580,plain,
v9_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3579]) ).
tcf(c_3594,plain,
! [X0: $i] :
( m2_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_455]) ).
tcf(c_3595,plain,
m2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3594]) ).
tcf(c_3599,plain,
! [X0: $i] :
( v21_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_453]) ).
tcf(c_3600,plain,
v21_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3599]) ).
tcf(c_3624,plain,
! [X0: $i] :
( v9_functor0(k7_waybel34(X0),k5_waybel34(X0),k4_waybel34(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_443]) ).
tcf(c_3625,plain,
v9_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)),
inference(unflattening,[status(thm)],[c_3624]) ).
tcf(c_3639,plain,
! [X0: $i] :
( ( k15_functor0(k5_waybel34(X0),k4_waybel34(X0),k7_waybel34(X0)) = k6_waybel34(X0) )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_437]) ).
tcf(c_3640,plain,
k15_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)) = k6_waybel34(sK0),
inference(unflattening,[status(thm)],[c_3639]) ).
tcf(c_3644,plain,
! [X0: $i] :
( ( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_435]) ).
tcf(c_3645,plain,
k15_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)) = k7_waybel34(sK0),
inference(unflattening,[status(thm)],[c_3644]) ).
tcf(c_4075,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X3,X1,X0)
| ~ v8_functor0(X2,X0,X1)
| ( k6_waybel34(sK0) != X3 )
| ( k4_waybel34(sK0) != X1 )
| ( k5_waybel34(sK0) != X0 )
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) ) ),
inference(resolution_lifted,[status(thm)],[c_1117,c_3555]) ).
tcf(c_4076,plain,
! [X0: $i] :
( v3_struct_0(k4_waybel34(sK0))
| v3_struct_0(k5_waybel34(sK0))
| ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),X0,k6_waybel34(sK0)) = k12_functor0(k5_waybel34(sK0)) )
| ~ l2_altcat_1(k4_waybel34(sK0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ v12_altcat_1(k4_waybel34(sK0))
| ~ v12_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0))
| ~ l2_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0)) != k15_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)) ) ),
inference(unflattening,[status(thm)],[c_4075]) ).
tcf(c_4078,plain,
! [X0: $i] :
( ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),X0,k6_waybel34(sK0)) = k12_functor0(k5_waybel34(sK0)) )
| ~ l2_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0)) != k15_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)) ) ),
inference(global_subsumption_just,[status(thm)],[c_4076,c_50,c_217,c_218,c_219,c_220,c_221,c_222,c_223,c_226,c_229,c_244,c_4076]) ).
tcf(c_4096,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k13_functor0(X0,X1,X0,X2,X3) = k12_functor0(X0) )
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X0)
| ~ l2_functor0(X3,X1,X0)
| ~ l2_functor0(X2,X0,X1)
| ~ v8_functor0(X3,X1,X0)
| ~ v8_functor0(X2,X0,X1)
| ( k7_waybel34(sK0) != X3 )
| ( k4_waybel34(sK0) != X0 )
| ( k5_waybel34(sK0) != X1 )
| ( g2_functor0(X0,X1,u1_functor0(X0,X1,X2),u2_functor0(X0,X1,X2)) != k15_functor0(X1,X0,X3) ) ),
inference(resolution_lifted,[status(thm)],[c_1117,c_3600]) ).
tcf(c_4097,plain,
! [X0: $i] :
( v3_struct_0(k4_waybel34(sK0))
| v3_struct_0(k5_waybel34(sK0))
| ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),X0,k7_waybel34(sK0)) = k12_functor0(k4_waybel34(sK0)) )
| ~ l2_altcat_1(k4_waybel34(sK0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ v12_altcat_1(k4_waybel34(sK0))
| ~ v12_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0))
| ~ l2_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0)) != k15_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)) ) ),
inference(unflattening,[status(thm)],[c_4096]) ).
tcf(c_4099,plain,
! [X0: $i] :
( ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),X0,k7_waybel34(sK0)) = k12_functor0(k4_waybel34(sK0)) )
| ~ l2_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0)) != k15_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)) ) ),
inference(global_subsumption_just,[status(thm)],[c_4097,c_50,c_217,c_218,c_219,c_220,c_221,c_222,c_223,c_226,c_229,c_253,c_4097]) ).
tcf(c_4818,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( g2_functor0(X1,X2,u1_functor0(X1,X2,X0),u2_functor0(X1,X2,X0)) = X0 )
| ~ l1_altcat_1(X2)
| ~ l1_altcat_1(X1)
| ~ l2_functor0(X0,X1,X2)
| ( k6_waybel34(sK0) != X0 )
| ( k4_waybel34(sK0) != X1 )
| ( k5_waybel34(sK0) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_159,c_3580]) ).
tcf(c_4819,plain,
( ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0))) = k6_waybel34(sK0) )
| ~ l1_altcat_1(k4_waybel34(sK0))
| ~ l1_altcat_1(k5_waybel34(sK0))
| ~ l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)) ),
inference(unflattening,[status(thm)],[c_4818]) ).
tcf(c_4832,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( g2_functor0(X1,X2,u1_functor0(X1,X2,X0),u2_functor0(X1,X2,X0)) = X0 )
| ~ l1_altcat_1(X2)
| ~ l1_altcat_1(X1)
| ~ l2_functor0(X0,X1,X2)
| ( k7_waybel34(sK0) != X0 )
| ( k4_waybel34(sK0) != X2 )
| ( k5_waybel34(sK0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_159,c_3625]) ).
tcf(c_4833,plain,
( ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0))) = k7_waybel34(sK0) )
| ~ l1_altcat_1(k4_waybel34(sK0))
| ~ l1_altcat_1(k5_waybel34(sK0))
| ~ l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)) ),
inference(unflattening,[status(thm)],[c_4832]) ).
tcf(c_7082,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| l2_functor0(X0,X1,X2)
| ~ l2_altcat_1(X2)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X2)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| ( k6_waybel34(sK0) != X0 )
| ( k4_waybel34(sK0) != X1 )
| ( k5_waybel34(sK0) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_144,c_3550]) ).
tcf(c_7083,plain,
( v3_struct_0(k4_waybel34(sK0))
| v3_struct_0(k5_waybel34(sK0))
| l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ l2_altcat_1(k4_waybel34(sK0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ v12_altcat_1(k4_waybel34(sK0))
| ~ v12_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k4_waybel34(sK0)) ),
inference(unflattening,[status(thm)],[c_7082]) ).
tcf(c_7084,plain,
l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0)),
inference(global_subsumption_just,[status(thm)],[c_7083,c_50,c_217,c_218,c_219,c_220,c_221,c_222,c_226,c_229,c_7083]) ).
tcf(c_7093,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| l2_functor0(X0,X1,X2)
| ~ l2_altcat_1(X2)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X2)
| ~ v12_altcat_1(X1)
| ~ v2_altcat_1(X1)
| ( k7_waybel34(sK0) != X0 )
| ( k4_waybel34(sK0) != X2 )
| ( k5_waybel34(sK0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_144,c_3595]) ).
tcf(c_7094,plain,
( v3_struct_0(k4_waybel34(sK0))
| v3_struct_0(k5_waybel34(sK0))
| l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ~ l2_altcat_1(k4_waybel34(sK0))
| ~ l2_altcat_1(k5_waybel34(sK0))
| ~ v12_altcat_1(k4_waybel34(sK0))
| ~ v12_altcat_1(k5_waybel34(sK0))
| ~ v2_altcat_1(k5_waybel34(sK0)) ),
inference(unflattening,[status(thm)],[c_7093]) ).
tcf(c_7095,plain,
l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0)),
inference(global_subsumption_just,[status(thm)],[c_7094,c_50,c_217,c_218,c_220,c_221,c_222,c_223,c_226,c_229,c_7094]) ).
tcf(c_7222,plain,
! [X0: $i] :
( ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),X0,k6_waybel34(sK0)) = k12_functor0(k5_waybel34(sK0)) )
| ~ l2_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0)) != k15_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4078,c_7084]) ).
tcf(c_7225,plain,
! [X0: $i] :
( ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),X0,k7_waybel34(sK0)) = k12_functor0(k4_waybel34(sK0)) )
| ~ l2_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0)) != k15_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4099,c_7095]) ).
tcf(c_10245,plain,
! [X0: $i] :
( ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),X0,k7_waybel34(sK0)) = k12_functor0(k4_waybel34(sK0)) )
| ~ l2_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(X0,k4_waybel34(sK0),k5_waybel34(sK0))
| ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),X0)) != k6_waybel34(sK0) ) ),
inference(light_normalisation,[status(thm)],[c_7225,c_3640]) ).
tcf(c_10258,plain,
! [X0: $i] :
( ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),X0,k6_waybel34(sK0)) = k12_functor0(k5_waybel34(sK0)) )
| ~ l2_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(X0,k5_waybel34(sK0),k4_waybel34(sK0))
| ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),X0)) != k7_waybel34(sK0) ) ),
inference(light_normalisation,[status(thm)],[c_7222,c_3645]) ).
tcf(c_17074,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l1_altcat_1(k5_waybel34(X0)) ),
inference(superposition,[status(thm)],[c_55,c_108]) ).
tcf(c_17075,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l1_altcat_1(k4_waybel34(X0)) ),
inference(superposition,[status(thm)],[c_63,c_108]) ).
tcf(c_17082,plain,
( v1_xboole_0(sK0)
| l1_altcat_1(k4_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_17075]) ).
tcf(c_17083,plain,
( v1_xboole_0(sK0)
| l1_altcat_1(k5_waybel34(sK0)) ),
inference(instantiation,[status(thm)],[c_17074]) ).
tcf(c_19723,plain,
( ( k13_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0),k6_waybel34(sK0),k7_waybel34(sK0)) = k12_functor0(k4_waybel34(sK0)) )
| ~ l2_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ~ v8_functor0(k6_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0))
| ( g2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),u1_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0)),u2_functor0(k4_waybel34(sK0),k5_waybel34(sK0),k6_waybel34(sK0))) != k6_waybel34(sK0) ) ),
inference(instantiation,[status(thm)],[c_10245]) ).
tcf(c_19724,plain,
( ( k13_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k5_waybel34(sK0),k7_waybel34(sK0),k6_waybel34(sK0)) = k12_functor0(k5_waybel34(sK0)) )
| ~ l2_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ~ v8_functor0(k7_waybel34(sK0),k5_waybel34(sK0),k4_waybel34(sK0))
| ( g2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),u1_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0)),u2_functor0(k5_waybel34(sK0),k4_waybel34(sK0),k7_waybel34(sK0))) != k7_waybel34(sK0) ) ),
inference(instantiation,[status(thm)],[c_10258]) ).
tcf(c_19725,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_19724,c_19723,c_17083,c_17082,c_7094,c_7083,c_4833,c_4819,c_49,c_253,c_244,c_229,c_226,c_223,c_222,c_221,c_220,c_219,c_218,c_217,c_50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT361+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.53 % Computer : n006.cluster.edu
% 0.10/0.53 % Model : x86_64 x86_64
% 0.10/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.53 % Memory : 8046.5625MB
% 0.10/0.53 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Wed Sep 23 21:21:28 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.10/0.54 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/0.57 Running first-order theorem proving
% 0.15/0.57 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.58
% 0.15/0.58 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.58
% 0.15/0.58 % Detected problem language: tptp
% 0.15/0.59 % Proving...
% 8.47/1.90 % SZS status Started for theBenchmark.p
% 8.47/1.90 % SZS status Theorem for theBenchmark.p
% 8.47/1.90
% 8.47/1.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.47/1.90
% 8.47/1.90 % ------ iProver source info
% 8.47/1.90
% 8.47/1.90 % git: date: 2026-07-19 20:42:38 +0200
% 8.47/1.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.47/1.90 % git: non_committed_changes: false
% 8.47/1.90
% 8.47/1.90 % ------ Parsing...
% 8.47/1.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.47/1.90
% 8.47/1.90 % ------ Preprocessing... sup_sim: 0 sf_s rm: 18 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 4 sf_s rm: 9 0s sf_e pe_s pe_e %
% 8.47/1.90
% 8.47/1.90 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.47/1.90
% 8.47/1.90 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.47/1.90 % ------ Proving...
% 8.47/1.90 % ------ Problem Properties
% 8.47/1.90
% 8.47/1.90 %
% 8.47/1.90 % clauses 136
% 8.47/1.90 % conjectures 1
% 8.47/1.90 % EPR 19
% 8.47/1.90 % Horn 79
% 8.47/1.90 % unary 41
% 8.47/1.90 % binary 15
% 8.47/1.90 % lits 601
% 8.47/1.90 % lits eq 27
% 8.47/1.90 % fd_pure 0
% 8.47/1.90 % fd_pseudo 0
% 8.47/1.90 % fd_cond 0
% 8.47/1.90 % fd_pseudo_cond 5
% 8.47/1.90 % AC symbols 0
% 8.47/1.90
% 8.47/1.90 % ------ Schedule dynamic 5 is on
% 8.47/1.90
% 8.47/1.90 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.47/1.90
% 8.47/1.90
% 8.47/1.90 % ------
% 8.47/1.90 % Current options:
% 8.47/1.90 % ------
% 8.47/1.90
% 8.47/1.90
% 8.47/1.90 %
% 8.47/1.90
% 8.47/1.90 % ------ Proving...
% 8.47/1.90 %
% 8.47/1.90
% 8.47/1.90 % SZS status Theorem for theBenchmark.p
% 8.47/1.90
% 8.47/1.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.47/1.91
% 8.47/1.91
%------------------------------------------------------------------------------