%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LAT377+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 : n027.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 215.91s 27.50s
% Output : CNFRefutation 216.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 17
% Syntax : Number of formulae : 170 ( 5 unt; 0 def)
% Number of atoms : 563 ( 4 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 581 ( 188 ~; 261 |; 106 &)
% ( 0 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 1 prp; 0-5 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-3 aty)
% Number of variables : 76 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t59_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k11_waybel34(A),k10_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t59_waybel34) ).
fof(t59_waybel34_negated,plain,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k11_waybel34(A),k10_waybel34(A)) ),
inference(negate_conjecture,[status(cth)],[t59_waybel34]) ).
cnf(0,plain,
~ v2_setfam_1(sK1),
inference(cnf,[status(esa)],[t59_waybel34_negated]) ).
cnf(l0,plain,
~ v2_setfam_1(sK1),
inference(instantiation,[status(thm)],[0]) ).
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(244,plain,
( v2_setfam_1(X0)
| v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc7_waybel34]) ).
cnf(l1,plain,
( v2_setfam_1(sK1)
| v16_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[244]) ).
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(340,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),k10_waybel34(sK1),k11_waybel34(sK1))
| ~ l2_altcat_1(k4_waybel34(sK1))
| ~ l2_altcat_1(k5_waybel34(sK1))
| ~ v3_altcat_2(k10_waybel34(sK1),k4_waybel34(sK1))
| ~ v3_altcat_2(k11_waybel34(sK1),k5_waybel34(sK1))
| ~ v2_altcat_1(k4_waybel34(sK1))
| ~ v2_altcat_1(k5_waybel34(sK1))
| ~ v2_altcat_1(k10_waybel34(sK1))
| ~ v2_altcat_1(k11_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(k10_waybel34(sK1),k4_waybel34(sK1))
| ~ m1_altcat_2(k11_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)),k11_waybel34(sK1),k10_waybel34(sK1))
| v3_struct_0(k4_waybel34(sK1))
| v3_struct_0(k5_waybel34(sK1))
| v3_struct_0(k10_waybel34(sK1))
| v3_struct_0(k11_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[340]) ).
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(203,plain,
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[fc5_waybel34]) ).
cnf(l1775,plain,
( ~ v3_struct_0(k4_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[203]) ).
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(137,plain,
( v1_xboole_0(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l1655,plain,
( v1_xboole_0(sK1)
| v12_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[137]) ).
fof(t58_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k10_waybel34(A),k11_waybel34(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_waybel34) ).
cnf(341,plain,
( r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k10_waybel34(X0),k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[t58_waybel34]) ).
cnf(l13,plain,
( r3_yellow20(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1),k10_waybel34(sK1),k11_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[341]) ).
fof(t36_altcat_4,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)
& v3_altcat_2(B,A)
& m1_altcat_2(B,A) )
=> ! [C] :
( ( ~ v3_struct_0(C)
& v2_altcat_1(C)
& v3_altcat_2(C,B)
& m1_altcat_2(C,B) )
=> ( ~ v3_struct_0(C)
& v2_altcat_1(C)
& v3_altcat_2(C,A)
& m1_altcat_2(C,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_altcat_4) ).
cnf(335,plain,
( ~ l2_altcat_1(X0)
| ~ v3_altcat_2(X1,X0)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X2)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ m1_altcat_2(X1,X0)
| ~ m1_altcat_2(X2,X1)
| v3_altcat_2(X2,X0)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v3_struct_0(X2) ),
inference(cnf,[status(esa)],[t36_altcat_4]) ).
cnf(l59,plain,
( ~ l2_altcat_1(k5_waybel34(sK1))
| ~ v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ v3_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1))
| ~ v2_altcat_1(k5_waybel34(sK1))
| ~ v2_altcat_1(k9_waybel34(sK1))
| ~ v2_altcat_1(k11_waybel34(sK1))
| ~ v11_altcat_1(k5_waybel34(sK1))
| ~ v12_altcat_1(k5_waybel34(sK1))
| ~ m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ m1_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1))
| v3_altcat_2(k11_waybel34(sK1),k5_waybel34(sK1))
| v3_struct_0(k5_waybel34(sK1))
| v3_struct_0(k9_waybel34(sK1))
| v3_struct_0(k11_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[335]) ).
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(331,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(l1899,plain,
( v2_setfam_1(sK1)
| k15_functor0(k4_waybel34(sK1),k5_waybel34(sK1),k6_waybel34(sK1)) = k7_waybel34(sK1) ),
inference(instantiation,[status(thm)],[331]) ).
cnf(1,plain,
~ r3_yellow20(k5_waybel34(sK1),k4_waybel34(sK1),k7_waybel34(sK1),k11_waybel34(sK1),k10_waybel34(sK1)),
inference(cnf,[status(esa)],[t59_waybel34_negated]) ).
cnf(l1759,plain,
~ r3_yellow20(k5_waybel34(sK1),k4_waybel34(sK1),k7_waybel34(sK1),k11_waybel34(sK1),k10_waybel34(sK1)),
inference(instantiation,[status(thm)],[1]) ).
fof(dt_k11_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k11_waybel34(A))
& v2_altcat_1(k11_waybel34(A))
& v6_altcat_1(k11_waybel34(A))
& v2_altcat_2(k11_waybel34(A),k9_waybel34(A))
& v3_altcat_2(k11_waybel34(A),k9_waybel34(A))
& m1_altcat_2(k11_waybel34(A),k9_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_waybel34) ).
cnf(116,plain,
( ~ v3_struct_0(k11_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[dt_k11_waybel34]) ).
cnf(l1707,plain,
( ~ v3_struct_0(k11_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[116]) ).
cnf(139,plain,
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l1645,plain,
( l2_altcat_1(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[139]) ).
cnf(117,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k11_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k11_waybel34]) ).
cnf(l27,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k11_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[117]) ).
cnf(l1940,plain,
( v1_xboole_0(sK1)
| v12_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[137]) ).
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(129,plain,
( v1_xboole_0(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l7,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[129]) ).
fof(fc13_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k10_waybel34(A))
& v2_altcat_1(k10_waybel34(A))
& v6_altcat_1(k10_waybel34(A))
& v9_altcat_1(k10_waybel34(A))
& v11_altcat_1(k10_waybel34(A))
& v12_altcat_1(k10_waybel34(A))
& v1_altcat_2(k10_waybel34(A))
& v2_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v3_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v2_yellow18(k10_waybel34(A))
& v3_yellow18(k10_waybel34(A))
& v4_yellow18(k10_waybel34(A))
& v1_yellow21(k10_waybel34(A))
& v2_yellow21(k10_waybel34(A))
& v3_yellow21(k10_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc13_waybel34) ).
cnf(185,plain,
( ~ v3_struct_0(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[fc13_waybel34]) ).
cnf(l1686,plain,
( ~ v3_struct_0(k10_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[185]) ).
cnf(336,plain,
( ~ l2_altcat_1(X0)
| ~ v3_altcat_2(X1,X0)
| ~ v3_altcat_2(X2,X1)
| ~ v2_altcat_1(X0)
| ~ v2_altcat_1(X1)
| ~ v2_altcat_1(X2)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ m1_altcat_2(X1,X0)
| ~ m1_altcat_2(X2,X1)
| v3_struct_0(X0)
| v3_struct_0(X1)
| v3_struct_0(X2)
| m1_altcat_2(X2,X0) ),
inference(cnf,[status(esa)],[t36_altcat_4]) ).
cnf(l1687,plain,
( ~ l2_altcat_1(k5_waybel34(sK1))
| ~ v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ v3_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1))
| ~ v2_altcat_1(k5_waybel34(sK1))
| ~ v2_altcat_1(k9_waybel34(sK1))
| ~ v2_altcat_1(k11_waybel34(sK1))
| ~ v11_altcat_1(k5_waybel34(sK1))
| ~ v12_altcat_1(k5_waybel34(sK1))
| ~ m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1))
| ~ m1_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1))
| v3_struct_0(k5_waybel34(sK1))
| v3_struct_0(k9_waybel34(sK1))
| v3_struct_0(k11_waybel34(sK1))
| m1_altcat_2(k11_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[336]) ).
cnf(133,plain,
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l1696,plain,
( ~ v3_struct_0(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[133]) ).
cnf(l1985,plain,
( ~ v3_struct_0(k11_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[116]) ).
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(142,plain,
( v2_setfam_1(X0)
| m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k6_waybel34]) ).
cnf(l1659,plain,
( v2_setfam_1(sK1)
| m2_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[142]) ).
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(152,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l1760,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[152]) ).
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(223,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc6_waybel34]) ).
cnf(l2136,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[223]) ).
cnf(136,plain,
( v1_xboole_0(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k5_waybel34]) ).
cnf(l25,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[136]) ).
fof(dt_k10_waybel34,plain,
! [A] :
( ~ v2_setfam_1(A)
=> ( ~ v3_struct_0(k10_waybel34(A))
& v2_altcat_1(k10_waybel34(A))
& v6_altcat_1(k10_waybel34(A))
& v2_altcat_2(k10_waybel34(A),k8_waybel34(A))
& v3_altcat_2(k10_waybel34(A),k8_waybel34(A))
& m1_altcat_2(k10_waybel34(A),k8_waybel34(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k10_waybel34) ).
cnf(111,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k10_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k10_waybel34]) ).
cnf(l3,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k10_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[111]) ).
cnf(154,plain,
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l140,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[154]) ).
cnf(l1963,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[154]) ).
cnf(120,plain,
( v2_setfam_1(X0)
| v3_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k11_waybel34]) ).
cnf(l1704,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[120]) ).
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(l1744,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(151,plain,
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l1710,plain,
( ~ v3_struct_0(k9_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[151]) ).
cnf(l1738,plain,
( ~ v3_struct_0(k11_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[116]) ).
cnf(121,plain,
( v2_setfam_1(X0)
| m1_altcat_2(k11_waybel34(X0),k9_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k11_waybel34]) ).
cnf(l1864,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[121]) ).
cnf(155,plain,
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k9_waybel34]) ).
cnf(l1973,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[155]) ).
cnf(l1935,plain,
( ~ v3_struct_0(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[133]) ).
cnf(208,plain,
( v2_setfam_1(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc5_waybel34]) ).
cnf(l1646,plain,
( v2_setfam_1(sK1)
| v12_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[208]) ).
cnf(226,plain,
( v2_setfam_1(X0)
| v11_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc6_waybel34]) ).
cnf(l1974,plain,
( v2_setfam_1(sK1)
| v11_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[226]) ).
cnf(l2020,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(127,plain,
( v1_xboole_0(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l96,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(l62,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1822,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[120]) ).
cnf(l2001,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[136]) ).
cnf(l1747,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k11_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[117]) ).
cnf(l4255,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l117,plain,
( l2_altcat_1(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[139]) ).
cnf(l2153,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k9_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[155]) ).
cnf(l4,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[223]) ).
cnf(132,plain,
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l36,plain,
( l2_altcat_1(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(222,plain,
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[fc6_waybel34]) ).
cnf(l2174,plain,
( ~ v3_struct_0(k5_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[222]) ).
cnf(l1758,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l193,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1933,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k11_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[117]) ).
cnf(l1649,plain,
( ~ l2_altcat_1(k4_waybel34(sK1))
| ~ v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ v3_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1))
| ~ v2_altcat_1(k4_waybel34(sK1))
| ~ v2_altcat_1(k8_waybel34(sK1))
| ~ v2_altcat_1(k10_waybel34(sK1))
| ~ v11_altcat_1(k4_waybel34(sK1))
| ~ v12_altcat_1(k4_waybel34(sK1))
| ~ m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ m1_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1))
| v3_struct_0(k4_waybel34(sK1))
| v3_struct_0(k8_waybel34(sK1))
| v3_struct_0(k10_waybel34(sK1))
| m1_altcat_2(k10_waybel34(sK1),k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[336]) ).
cnf(l2019,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(186,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k10_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc13_waybel34]) ).
cnf(l3717,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k10_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[186]) ).
cnf(110,plain,
( ~ v3_struct_0(k10_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf,[status(esa)],[dt_k10_waybel34]) ).
cnf(l3707,plain,
( ~ v3_struct_0(k10_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l3686,plain,
( v1_xboole_0(sK1)
| v11_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[129]) ).
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(150,plain,
( v1_xboole_0(X0)
| m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l3695,plain,
( v1_xboole_0(sK1)
| m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[150]) ).
cnf(l3732,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(193,plain,
( v2_setfam_1(X0)
| v3_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc13_waybel34]) ).
cnf(l1654,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[193]) ).
cnf(149,plain,
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l1673,plain,
( v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[149]) ).
cnf(l1800,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[127]) ).
cnf(126,plain,
( ~ v3_struct_0(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l3709,plain,
( ~ v3_struct_0(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[126]) ).
cnf(l1672,plain,
( l2_altcat_1(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(l1820,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3762,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l3797,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1945,plain,
( ~ v3_struct_0(k9_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[151]) ).
cnf(227,plain,
( v2_setfam_1(X0)
| v12_altcat_1(k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc6_waybel34]) ).
cnf(l2157,plain,
( v2_setfam_1(sK1)
| v12_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[227]) ).
cnf(l3757,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1742,plain,
( l2_altcat_1(k5_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[139]) ).
cnf(l108,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1781,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l2176,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l95,plain,
( ~ l2_altcat_1(k4_waybel34(sK1))
| ~ v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ v3_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1))
| ~ v2_altcat_1(k4_waybel34(sK1))
| ~ v2_altcat_1(k8_waybel34(sK1))
| ~ v2_altcat_1(k10_waybel34(sK1))
| ~ v11_altcat_1(k4_waybel34(sK1))
| ~ v12_altcat_1(k4_waybel34(sK1))
| ~ m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| ~ m1_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1))
| v3_altcat_2(k10_waybel34(sK1),k4_waybel34(sK1))
| v3_struct_0(k4_waybel34(sK1))
| v3_struct_0(k8_waybel34(sK1))
| v3_struct_0(k10_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[335]) ).
cnf(l2110,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(207,plain,
( v2_setfam_1(X0)
| v11_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc5_waybel34]) ).
cnf(l1888,plain,
( v2_setfam_1(sK1)
| v11_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[207]) ).
cnf(l1946,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[223]) ).
cnf(204,plain,
( v2_setfam_1(X0)
| v2_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc5_waybel34]) ).
cnf(l1761,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[204]) ).
cnf(l1703,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k10_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[186]) ).
cnf(130,plain,
( v1_xboole_0(X0)
| v12_altcat_1(k4_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k4_waybel34]) ).
cnf(l1692,plain,
( v1_xboole_0(sK1)
| v12_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[130]) ).
cnf(l1937,plain,
( v2_setfam_1(sK1)
| v2_altcat_1(k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[152]) ).
cnf(l4463,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l332,plain,
( v3_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[149]) ).
cnf(l1867,plain,
( ~ v3_struct_0(k10_waybel34(sK1))
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l4206,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k11_waybel34(sK1),k9_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[121]) ).
cnf(147,plain,
( v1_xboole_0(X0)
| v2_altcat_1(k8_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l1780,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[147]) ).
cnf(l1621,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l300,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l116,plain,
( l2_altcat_1(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[132]) ).
cnf(l3710,plain,
( v2_setfam_1(sK1)
| v12_altcat_1(k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[208]) ).
cnf(115,plain,
( v2_setfam_1(X0)
| m1_altcat_2(k10_waybel34(X0),k8_waybel34(X0)) ),
inference(cnf,[status(esa)],[dt_k10_waybel34]) ).
cnf(l1700,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[115]) ).
cnf(l1717,plain,
( ~ v3_struct_0(k4_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[126]) ).
cnf(l3712,plain,
( v2_setfam_1(sK1)
| m1_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[115]) ).
cnf(l137,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1901,plain,
( v1_xboole_0(sK1)
| m1_altcat_2(k8_waybel34(sK1),k4_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[150]) ).
cnf(146,plain,
( ~ v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf,[status(esa)],[dt_k8_waybel34]) ).
cnf(l3684,plain,
( ~ v3_struct_0(k8_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[146]) ).
cnf(l2004,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l128,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1909,plain,
( v1_xboole_0(sK1)
| v2_altcat_1(k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[147]) ).
cnf(l1697,plain,
( v2_setfam_1(sK1)
| v3_altcat_2(k10_waybel34(sK1),k8_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l1836,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l1906,plain,
( ~ v3_struct_0(k8_waybel34(sK1))
| v1_xboole_0(sK1) ),
inference(instantiation,[status(thm)],[146]) ).
cnf(l3818,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(245,plain,
( v2_setfam_1(X0)
| v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf,[status(esa)],[fc7_waybel34]) ).
cnf(l1737,plain,
( v2_setfam_1(sK1)
| v21_functor0(k6_waybel34(sK1),k4_waybel34(sK1),k5_waybel34(sK1)) ),
inference(instantiation,[status(thm)],[245]) ).
cnf(l3527,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l5392,plain,
( ~ v1_xboole_0(sK1)
| v2_setfam_1(sK1) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l6076,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,l1775,l1655,l13,l59,l1899,l1759,l1707,l1645,l27,l1940,l7,l1686,l1687,l1696,l1985,l1659,l1760,l2136,l25,l3,l140,l1963,l1704,l1744,l1710,l1738,l1864,l1973,l1935,l1646,l1974,l2020,l96,l62,l1822,l2001,l1747,l4255,l117,l2153,l4,l36,l2174,l1758,l193,l1933,l1649,l2019,l3717,l3707,l3686,l3695,l3732,l1654,l1673,l1800,l3709,l1672,l1820,l3762,l3797,l1945,l2157,l3757,l1742,l108,l1781,l2176,l95,l2110,l1888,l1946,l1761,l1703,l1692,l1937,l4463,l332,l1867,l4206,l1780,l1621,l300,l116,l3710,l1700,l1717,l3712,l137,l1901,l3684,l2004,l128,l1909,l1697,l1836,l1906,l3818,l1737,l3527,l5392,l6076]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT377+1 : TPTP v9.0.0. Released v3.4.0.
% 0.07/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 % Computer : n027.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Mon Jul 21 01:41:04 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.36 % launching worker at depth: 3
% 0.13/0.36 % launching worker at depth: 1
% 0.13/0.36 % launching worker at depth: 4
% 0.13/0.36 % launching worker at depth: 6
% 0.13/0.36 % launching worker at depth: 2
% 0.13/0.36 % launching worker at depth: 5
% 0.13/0.36 % launching worker at depth: 7
% 0.13/0.36 % launching worker at depth: 8
% 0.13/0.36 % launching worker at depth: 9
% 0.20/0.41 % launching worker at depth: 10
% 1.51/0.55 % launching worker at depth: 11
% 27.67/3.82 % launching worker at depth: 12
% 215.91/27.50 % SZS status Theorem for theBenchmark
% 215.91/27.50 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------