%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT376+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:01 PM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 37
% Syntax : Number of formulae : 169 ( 20 unt; 24 def)
% Number of atoms : 580 ( 6 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 606 ( 195 ~; 242 |; 125 &)
% ( 24 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 54 ( 52 usr; 25 prp; 0-5 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-3 aty)
% Number of variables : 75 ( 74 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A)) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f29,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( l2_altcat_1(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( l2_altcat_1(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ( m1_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v6_altcat_1(k8_waybel34(A))
& v2_altcat_1(k8_waybel34(A))
& ~ v3_struct_0(k8_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( m1_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v6_altcat_1(k9_waybel34(A))
& v2_altcat_1(k9_waybel34(A))
& ~ v3_struct_0(k9_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v3_yellow21(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v1_yellow21(k4_waybel34(A))
& v4_yellow18(k4_waybel34(A))
& v3_yellow18(k4_waybel34(A))
& v2_yellow18(k4_waybel34(A))
& v1_altcat_2(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v9_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v3_yellow21(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v1_yellow21(k5_waybel34(A))
& v4_yellow18(k5_waybel34(A))
& v3_yellow18(k5_waybel34(A))
& v2_yellow18(k5_waybel34(A))
& v1_altcat_2(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v9_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ( k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A)
& k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [A] :
( ( l2_altcat_1(A)
& v12_altcat_1(A)
& v11_altcat_1(A)
& v2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l2_altcat_1(B)
& v12_altcat_1(B)
& v11_altcat_1(B)
& v2_altcat_1(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_functor0(C,A,B)
& v16_functor0(C,A,B) )
=> ( v21_functor0(C,A,B)
=> ! [D] :
( ( m1_altcat_2(D,A)
& v3_altcat_2(D,A)
& v2_altcat_1(D)
& ~ v3_struct_0(D) )
=> ! [E] :
( ( m1_altcat_2(E,B)
& v3_altcat_2(E,B)
& v2_altcat_1(E)
& ~ v3_struct_0(E) )
=> ( r3_yellow20(A,B,C,D,E)
=> r3_yellow20(B,A,k15_functor0(A,B,C),E,D) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k8_waybel34(A),k9_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,plain,
? [A] :
( ~ r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A))
& ~ v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f130,plain,
( ~ r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))
& ~ v2_setfam_1(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f129]) ).
fof(f131,plain,
~ v2_setfam_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
~ r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f231,plain,
! [A] :
( ~ v1_xboole_0(A)
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f232,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f318,plain,
! [A] :
( ( l2_altcat_1(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f325,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f326,plain,
! [A] :
( ( l2_altcat_1(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f333,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f334,plain,
! [A] :
( ( m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f336,plain,
! [X0] :
( v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f337,plain,
! [X0] :
( m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f342,plain,
! [A] :
( ( m1_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))
& v6_altcat_1(k8_waybel34(A))
& v2_altcat_1(k8_waybel34(A))
& ~ v3_struct_0(k8_waybel34(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f343,plain,
! [X0] :
( ~ v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f344,plain,
! [X0] :
( v2_altcat_1(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f346,plain,
! [X0] :
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f347,plain,
! [X0] :
( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f348,plain,
! [A] :
( ( m1_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))
& v6_altcat_1(k9_waybel34(A))
& v2_altcat_1(k9_waybel34(A))
& ~ v3_struct_0(k9_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f349,plain,
! [X0] :
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f350,plain,
! [X0] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f352,plain,
! [X0] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f353,plain,
! [X0] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f422,plain,
! [A] :
( ( v3_yellow21(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v1_yellow21(k4_waybel34(A))
& v4_yellow18(k4_waybel34(A))
& v3_yellow18(k4_waybel34(A))
& v2_yellow18(k4_waybel34(A))
& v1_altcat_2(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v9_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& ~ v3_struct_0(k4_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f423,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f424,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f427,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f428,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f442,plain,
! [A] :
( ( v3_yellow21(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v1_yellow21(k5_waybel34(A))
& v4_yellow18(k5_waybel34(A))
& v3_yellow18(k5_waybel34(A))
& v2_yellow18(k5_waybel34(A))
& v1_altcat_2(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v9_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& ~ v3_struct_0(k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f93]) ).
fof(f443,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f447,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f448,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f460,plain,
! [A] :
( ( v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f468,plain,
! [X0] :
( v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f576,plain,
! [A] :
( ( k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A)
& k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A) )
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f118]) ).
fof(f577,plain,
! [X0] :
( k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f576]) ).
fof(f590,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( r3_yellow20(B,A,k15_functor0(A,B,C),E,D)
| ~ r3_yellow20(A,B,C,D,E)
| ~ m1_altcat_2(E,B)
| ~ v3_altcat_2(E,B)
| ~ v2_altcat_1(E)
| v3_struct_0(E) )
| ~ m1_altcat_2(D,A)
| ~ v3_altcat_2(D,A)
| ~ v2_altcat_1(D)
| v3_struct_0(D) )
| ~ v21_functor0(C,A,B)
| ~ m2_functor0(C,A,B)
| ~ v16_functor0(C,A,B) )
| ~ l2_altcat_1(B)
| ~ v12_altcat_1(B)
| ~ v11_altcat_1(B)
| ~ v2_altcat_1(B)
| v3_struct_0(B) )
| ~ l2_altcat_1(A)
| ~ v12_altcat_1(A)
| ~ v11_altcat_1(A)
| ~ v2_altcat_1(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f123]) ).
fof(f591,plain,
! [X0,X1,X2,X3,X4] :
( r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| ~ r3_yellow20(X0,X1,X2,X3,X4)
| ~ m1_altcat_2(X4,X1)
| ~ v3_altcat_2(X4,X1)
| ~ v2_altcat_1(X4)
| v3_struct_0(X4)
| ~ m1_altcat_2(X3,X0)
| ~ v3_altcat_2(X3,X0)
| ~ v2_altcat_1(X3)
| v3_struct_0(X3)
| ~ v21_functor0(X2,X0,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ l2_altcat_1(X1)
| ~ v12_altcat_1(X1)
| ~ v11_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ l2_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f590]) ).
fof(f592,plain,
! [A] :
( r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k8_waybel34(A),k9_waybel34(A))
| v2_setfam_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f593,plain,
! [X0] :
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k8_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f618,plain,
v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)),
inference(resolution,[status(thm)],[f336,f131]) ).
fof(f652,plain,
k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)) = k7_waybel34(sK0_skl),
inference(resolution,[status(thm)],[f577,f131]) ).
fof(f683,definition,
( sQ7_spl
<=> v3_struct_0(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( ~ sQ7_spl
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f686,definition,
( sQ8_spl
<=> v2_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( sQ8_spl
| ~ v2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,definition,
( sQ9_spl
<=> v11_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ9_spl
| ~ v11_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,definition,
( sQ10_spl
<=> v12_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( sQ10_spl
| ~ v12_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f692]) ).
fof(f695,definition,
( sQ11_spl
<=> l2_altcat_1(k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f697,plain,
( sQ11_spl
| ~ l2_altcat_1(k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f695]) ).
fof(f713,definition,
( sQ15_spl
<=> v3_struct_0(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( ~ sQ15_spl
| v3_struct_0(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f713]) ).
fof(f716,definition,
( sQ16_spl
<=> v2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f718,plain,
( sQ16_spl
| ~ v2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f716]) ).
fof(f719,definition,
( sQ17_spl
<=> v11_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f721,plain,
( sQ17_spl
| ~ v11_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f719]) ).
fof(f722,definition,
( sQ18_spl
<=> v12_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( sQ18_spl
| ~ v12_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f722]) ).
fof(f725,definition,
( sQ19_spl
<=> l2_altcat_1(k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f727,plain,
( sQ19_spl
| ~ l2_altcat_1(k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f725]) ).
fof(f740,plain,
! [X0,X1] :
( r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),X1,X0)
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)
| ~ m1_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k5_waybel34(sK0_skl))
| ~ v12_altcat_1(k5_waybel34(sK0_skl))
| ~ v11_altcat_1(k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k5_waybel34(sK0_skl))
| v3_struct_0(k5_waybel34(sK0_skl))
| ~ l2_altcat_1(k4_waybel34(sK0_skl))
| ~ v12_altcat_1(k4_waybel34(sK0_skl))
| ~ v11_altcat_1(k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k4_waybel34(sK0_skl))
| v3_struct_0(k4_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f618,f591]) ).
fof(f743,definition,
( sQ23_spl
<=> m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( sQ23_spl
| ~ m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f746,definition,
( sQ24_spl
<=> v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f748,plain,
( sQ24_spl
| ~ v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f749,definition,
! [X0,X1] :
( sQ25_spl
<=> ( r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),X1,X0)
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)
| ~ m1_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f750,plain,
! [X0,X1] :
( ~ sQ25_spl
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl)),X1,X0)
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)
| ~ m1_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f749]) ).
fof(f752,plain,
( sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| sQ15_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f740,f683,f686,f689,f692,f695,f713,f716,f719,f722,f725,f743,f746,f749]) ).
fof(f761,plain,
( sQ11_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f697,f325]) ).
fof(f873,plain,
( sQ10_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f694,f428]) ).
fof(f879,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f873,f131]) ).
fof(f880,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f879]) ).
fof(f881,plain,
( sQ9_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f691,f427]) ).
fof(f888,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f881,f131]) ).
fof(f889,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f888]) ).
fof(f890,plain,
( sQ8_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f688,f424]) ).
fof(f892,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f890,f131]) ).
fof(f893,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f892]) ).
fof(f894,plain,
( ~ sQ7_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f684,f423]) ).
fof(f896,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f894,f131]) ).
fof(f897,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f896]) ).
fof(f898,plain,
( sQ19_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f727,f333]) ).
fof(f899,plain,
( sQ18_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f724,f448]) ).
fof(f905,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f899,f131]) ).
fof(f906,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f905]) ).
fof(f907,plain,
( sQ17_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f721,f447]) ).
fof(f914,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f131]) ).
fof(f915,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f914]) ).
fof(f916,plain,
( sQ16_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f718,f444]) ).
fof(f918,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f916,f131]) ).
fof(f919,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f918]) ).
fof(f920,plain,
( ~ sQ15_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f714,f443]) ).
fof(f922,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f920,f131]) ).
fof(f923,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f922]) ).
fof(f924,plain,
( sQ23_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f745,f337]) ).
fof(f925,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f924,f131]) ).
fof(f926,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f925]) ).
fof(f1027,plain,
~ v1_xboole_0(sK0_skl),
inference(resolution,[status(thm)],[f232,f131]) ).
fof(f1028,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1027,f761]) ).
fof(f1029,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1028]) ).
fof(f1030,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f898,f1027]) ).
fof(f1031,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1030]) ).
fof(f1033,definition,
( sQ66_spl
<=> m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1035,plain,
( sQ66_spl
| ~ m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1033]) ).
fof(f1036,definition,
( sQ67_spl
<=> v3_struct_0(k8_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( ~ sQ67_spl
| v3_struct_0(k8_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1039,definition,
( sQ68_spl
<=> v2_altcat_1(k8_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
( sQ68_spl
| ~ v2_altcat_1(k8_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1045,definition,
( sQ70_spl
<=> v1_xboole_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1046,plain,
( ~ sQ70_spl
| v1_xboole_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1045]) ).
fof(f1049,plain,
( ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1046,f1027]) ).
fof(f1050,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1049]) ).
fof(f1057,definition,
( sQ71_spl
<=> v2_setfam_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ71_spl
| v2_setfam_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f1057]) ).
fof(f1062,plain,
( ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f131]) ).
fof(f1063,plain,
~ sQ71_spl,
inference(contradiction_clause,[status(thm)],[f1062]) ).
fof(f1068,plain,
( sQ24_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f748,f468]) ).
fof(f1069,plain,
( sQ24_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1068,f1057,f746]) ).
fof(f1070,plain,
! [X0,X1] :
( ~ sQ25_spl
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)
| ~ m1_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X1,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ~ m1_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k4_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(forward_demodulation,[status(thm)],[f652,f750]) ).
fof(f1094,definition,
( sQ72_spl
<=> m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1096,plain,
( sQ72_spl
| ~ m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1094]) ).
fof(f1097,definition,
( sQ73_spl
<=> v3_struct_0(k9_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
( ~ sQ73_spl
| v3_struct_0(k9_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1097]) ).
fof(f1100,definition,
( sQ74_spl
<=> v2_altcat_1(k9_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
( sQ74_spl
| ~ v2_altcat_1(k9_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1100]) ).
fof(f1107,plain,
! [X0] :
( ~ sQ25_spl
| v1_xboole_0(sK0_skl)
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl))
| ~ v2_altcat_1(k8_waybel34(sK0_skl))
| v3_struct_0(k8_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1070,f346]) ).
fof(f1108,definition,
! [X0] :
( sQ76_spl
<=> ( r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1109,plain,
! [X0] :
( ~ sQ76_spl
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v3_altcat_2(X0,k5_waybel34(sK0_skl))
| ~ v2_altcat_1(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f1108]) ).
fof(f1111,plain,
( ~ sQ25_spl
| sQ70_spl
| sQ76_spl
| ~ sQ66_spl
| ~ sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1107,f1036,f1039,f1033,f1108,f1045,f749]) ).
fof(f1112,plain,
( ~ sQ76_spl
| v2_setfam_1(sK0_skl)
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))
| ~ m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl))
| ~ v2_altcat_1(k9_waybel34(sK0_skl))
| v3_struct_0(k9_waybel34(sK0_skl)) ),
inference(resolution,[status(thm)],[f1109,f352]) ).
fof(f1113,definition,
( sQ77_spl
<=> r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1115,plain,
( sQ77_spl
| ~ r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1113]) ).
fof(f1116,definition,
( sQ78_spl
<=> r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1117,plain,
( ~ sQ78_spl
| r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1116]) ).
fof(f1119,plain,
( ~ sQ76_spl
| sQ71_spl
| sQ78_spl
| ~ sQ77_spl
| ~ sQ72_spl
| ~ sQ74_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f1112,f1097,f1100,f1094,f1113,f1116,f1057,f1108]) ).
fof(f1143,plain,
( sQ68_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1041,f344]) ).
fof(f1144,plain,
( sQ68_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1143,f1045,f1039]) ).
fof(f1145,plain,
( ~ sQ67_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1037,f343]) ).
fof(f1146,plain,
( ~ sQ67_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1145,f1045,f1036]) ).
fof(f1147,plain,
( sQ74_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1102,f350]) ).
fof(f1148,plain,
( sQ74_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1147,f1057,f1100]) ).
fof(f1149,plain,
( ~ sQ73_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1098,f349]) ).
fof(f1150,plain,
( ~ sQ73_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1149,f1057,f1097]) ).
fof(f1177,plain,
( sQ66_spl
| v1_xboole_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1035,f347]) ).
fof(f1178,plain,
( sQ66_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1177,f1045,f1033]) ).
fof(f1181,plain,
( sQ72_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1096,f353]) ).
fof(f1182,plain,
( sQ72_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1181,f1057,f1094]) ).
fof(f1332,plain,
( sQ77_spl
| v2_setfam_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1115,f593]) ).
fof(f1334,plain,
( sQ77_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1332,f1057,f1113]) ).
fof(f1335,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1117,f132]) ).
fof(f1336,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1335]) ).
fof(f1337,plain,
$false,
inference(sat_refutation,[status(thm)],[f752,f880,f889,f893,f897,f906,f915,f919,f923,f926,f1029,f1031,f1050,f1063,f1069,f1111,f1119,f1144,f1146,f1148,f1150,f1178,f1182,f1334,f1336]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT376+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 23:56:02 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.44 % Elapsed time: 0.069559 seconds
% 0.08/0.44 % CPU time: 0.252662 seconds
% 0.08/0.44 % Total memory used: 40.221 MB
% 0.08/0.44 % Net memory used: 40.079 MB
%------------------------------------------------------------------------------