%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LAT376+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 10:34:42 PM UTC 2025
% Result : Theorem 8.23s 1.45s
% Output : CNFRefutation 8.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 80 ( 5 unt; 0 def)
% Number of atoms : 272 ( 4 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 278 ( 86 ~; 103 |; 69 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 1 prp; 0-5 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-3 aty)
% Number of variables : 47 ( 0 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t57_waybel34,plain,
! [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',t57_waybel34) ).
fof(t57_waybel34_negated,plain,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A)) ),
inference(negate_conjecture,[status(cth)],[t57_waybel34]) ).
cnf(0,plain,
~ v2_setfam_1(sK1),
inference(cnf,[status(esa)],[t57_waybel34_negated]) ).
cnf(l0,plain,
~ v2_setfam_1(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(dt_k9_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k9_waybel34(A))
& v2_altcat_1(k9_waybel34(A))
& v6_altcat_1(k9_waybel34(A))
& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))
& m1_altcat_2(k9_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_waybel34) ).
cnf(139,plain,
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l1,plain,
( ~ v3_struct_0(k9_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[139]) ).
fof(t52_yellow20,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v2_altcat_1(A)
& v11_altcat_1(A)
& v12_altcat_1(A)
& l2_altcat_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_altcat_1(B)
& v11_altcat_1(B)
& v12_altcat_1(B)
& l2_altcat_1(B) )
=> ! [C] :
( ( v16_functor0(C,A,B)
& m2_functor0(C,A,B) )
=> ( v21_functor0(C,A,B)
=> ! [D] :
( ( ~ v3_struct_0(D)
& v2_altcat_1(D)
& v3_altcat_2(D,A)
& m1_altcat_2(D,A) )
=> ! [E] :
( ( ~ v3_struct_0(E)
& v2_altcat_1(E)
& v3_altcat_2(E,B)
& m1_altcat_2(E,B) )
=> ( 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',t52_yellow20) ).
cnf(302,plain,
( ~ r3_yellow20(X0,X1,X2,X3,X4)
| ~ l2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ v3_altcat_2(X3,X0)
| ~ v3_altcat_2(X4,X1)
| ~ v2_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X3)
| ~ v2_altcat_1(X4)
| ~ v11_altcat_1(X0)
| ~ v11_altcat_1(X1)
| ~ v12_altcat_1(X0)
| ~ v12_altcat_1(X1)
| ~ m1_altcat_2(X3,X0)
| ~ m1_altcat_2(X4,X1)
| ~ m2_functor0(X2,X0,X1)
| ~ v16_functor0(X2,X0,X1)
| ~ v21_functor0(X2,X0,X1)
| r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v3_struct_0(X3)
| v3_struct_0(X4) ),
inference(cnf,[status(esa)],[t52_yellow20]) ).
cnf(l2,plain,
( ~ r3_yellow20(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1),k8_waybel34(sK1),k9_waybel34(sK1))
| ~ l2_altcat_1(k4_waybel34(sK1))
| ~ l2_altcat_1(k5_waybel34(sK1))
| ~ v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ v2_altcat_1(k4_waybel34(sK1))
| ~ v2_altcat_1(k5_waybel34(sK1))
| ~ v2_altcat_1(k8_waybel34(sK1))
| ~ v2_altcat_1(k9_waybel34(sK1))
| ~ v11_altcat_1(k4_waybel34(sK1))
| ~ v11_altcat_1(k5_waybel34(sK1))
| ~ v12_altcat_1(k4_waybel34(sK1))
| ~ v12_altcat_1(k5_waybel34(sK1))
| ~ m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ m2_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1))
| ~ v16_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1))
| ~ v21_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1))
| r3_yellow20(k5_waybel34(sK1),k4_waybel34(sK1),k15_functor0(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1)),k9_waybel34(sK1),k8_waybel34(sK1))
| v3_struct_0(k4_waybel34(sK1))
| v3_struct_0(k5_waybel34(sK1))
| v3_struct_0(k8_waybel34(sK1))
| v3_struct_0(k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[302]) ).
cnf(140,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l353,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[140]) ).
fof(dt_k8_waybel34,plain,
! [A] :
( ~ v1_xboole_0(A)
=> ( ~ v3_struct_0(k8_waybel34(A))
& v2_altcat_1(k8_waybel34(A))
& v6_altcat_1(k8_waybel34(A))
& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))
& m1_altcat_2(k8_waybel34(A),k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_waybel34) ).
cnf(134,plain,
( ~ v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l525,plain,
( ~ v3_struct_0(k8_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[134]) ).
cnf(137,plain,
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l357,plain,
( v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[137]) ).
cnf(138,plain,
( v1_xboole_0(X0)
| m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l408,plain,
( v1_xboole_0(sK1)
| m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[138]) ).
fof(fc6_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v9_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v1_altcat_2(k5_waybel34(A))
& v2_yellow18(k5_waybel34(A))
& v3_yellow18(k5_waybel34(A))
& v4_yellow18(k5_waybel34(A))
& v1_yellow21(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& v3_yellow21(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_waybel34) ).
cnf(200,plain,
( v2_setfam_1(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc6_waybel34]) ).
cnf(l414,plain,
( v2_setfam_1(sK1)
| v12_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[200]) ).
fof(dt_k5_waybel34,plain,
! [A] :
( ~ v1_xboole_0(A)
=> ( ~ v3_struct_0(k5_waybel34(A))
& v2_altcat_1(k5_waybel34(A))
& v6_altcat_1(k5_waybel34(A))
& v11_altcat_1(k5_waybel34(A))
& v12_altcat_1(k5_waybel34(A))
& v2_yellow21(k5_waybel34(A))
& l2_altcat_1(k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_waybel34) ).
cnf(127,plain,
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l352,plain,
( l2_altcat_1(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[127]) ).
fof(dt_k4_waybel34,plain,
! [A] :
( ~ v1_xboole_0(A)
=> ( ~ v3_struct_0(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& l2_altcat_1(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_waybel34) ).
cnf(118,plain,
( v1_xboole_0(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l417,plain,
( v1_xboole_0(sK1)
| v12_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[118]) ).
cnf(135,plain,
( v1_xboole_0(X0)
| v2_altcat_1(k8_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l358,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[135]) ).
fof(fc7_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_waybel34) ).
cnf(218,plain,
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc7_waybel34]) ).
cnf(l402,plain,
( v2_setfam_1(sK1)
| v21_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[218]) ).
fof(fc5_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k4_waybel34(A))
& v2_altcat_1(k4_waybel34(A))
& v6_altcat_1(k4_waybel34(A))
& v9_altcat_1(k4_waybel34(A))
& v11_altcat_1(k4_waybel34(A))
& v12_altcat_1(k4_waybel34(A))
& v1_altcat_2(k4_waybel34(A))
& v2_yellow18(k4_waybel34(A))
& v3_yellow18(k4_waybel34(A))
& v4_yellow18(k4_waybel34(A))
& v1_yellow21(k4_waybel34(A))
& v2_yellow21(k4_waybel34(A))
& v3_yellow21(k4_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_waybel34) ).
cnf(176,plain,
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[fc5_waybel34]) ).
cnf(l477,plain,
( ~ v3_struct_0(k4_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[176]) ).
cnf(142,plain,
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l364,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[142]) ).
fof(cc2_setfam_1,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_setfam_1) ).
cnf(63,plain,
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[cc2_setfam_1]) ).
cnf(l401,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(217,plain,
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc7_waybel34]) ).
cnf(l430,plain,
( v2_setfam_1(sK1)
| v16_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[217]) ).
cnf(143,plain,
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l410,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[143]) ).
cnf(124,plain,
( v1_xboole_0(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l395,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[124]) ).
fof(t56_waybel34,plain,
! [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',t56_waybel34) ).
cnf(303,plain,
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k8_waybel34(X0),k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[t56_waybel34]) ).
cnf(l26,plain,
( r3_yellow20(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1),k8_waybel34(sK1),k9_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[303]) ).
cnf(l466,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
fof(dt_k6_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))
& m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_waybel34) ).
cnf(130,plain,
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k6_waybel34]) ).
cnf(l442,plain,
( v2_setfam_1(sK1)
| m2_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[130]) ).
cnf(120,plain,
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l3,plain,
( l2_altcat_1(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[120]) ).
cnf(117,plain,
( v1_xboole_0(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l403,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[117]) ).
cnf(l371,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l445,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(115,plain,
( v1_xboole_0(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l350,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[115]) ).
cnf(121,plain,
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l432,plain,
( ~ v3_struct_0(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[121]) ).
cnf(1,plain,
~ r3_yellow20(k5_waybel34(sK1),k4_waybel34(sK1),k7_waybel34(sK1),k9_waybel34(sK1),k8_waybel34(sK1)),
inference(cnf,[status(esa)],[t57_waybel34_negated]) ).
cnf(l406,plain,
~ r3_yellow20(k5_waybel34(sK1),k4_waybel34(sK1),k7_waybel34(sK1),k9_waybel34(sK1),k8_waybel34(sK1)),
inference(instantiation,[status(thm)],[1]) ).
cnf(122,plain,
( v1_xboole_0(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l369,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[122]) ).
cnf(l398,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l7,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l453,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l428,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l363,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l436,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l542,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
fof(t18_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A)
& k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_waybel34) ).
cnf(295,plain,
( v2_setfam_1(X0)
| k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0)) = k7_waybel34(X0) ),
inference(cnf,[status(esa)],[t18_waybel34]) ).
cnf(l407,plain,
( v2_setfam_1(sK1)
| k15_functor0(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1)) = k7_waybel34(sK1) ),
inference(instantiation,[status(thm)],[295]) ).
cnf(l544,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l353,l525,l357,l408,l414,l352,l417,l358,l402,l477,l364,l401,l430,l410,l395,l26,l466,l442,l3,l403,l371,l445,l350,l432,l406,l369,l398,l7,l453,l428,l363,l436,l542,l407,l544]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT376+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 21 01:40:04 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.19/0.35 % launching worker at depth: 3
% 0.19/0.35 % launching worker at depth: 1
% 0.19/0.35 % launching worker at depth: 7
% 0.19/0.35 % launching worker at depth: 8
% 0.19/0.35 % launching worker at depth: 2
% 0.19/0.35 % launching worker at depth: 6
% 0.19/0.35 % launching worker at depth: 4
% 0.19/0.35 % launching worker at depth: 5
% 0.19/0.35 % launching worker at depth: 9
% 0.19/0.38 % launching worker at depth: 10
% 0.19/0.54 % launching worker at depth: 11
% 8.23/1.45 % SZS status Theorem for theBenchmark
% 8.23/1.45 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------