%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT362+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n014.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 : Wed Apr 9 07:12:05 PM UTC 2025
% Result : Theorem 24.68s 10.70s
% Output : CNFRefutation 24.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 60 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 213 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 238 ( 85 ~; 89 |; 53 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 55 ( 54 usr; 1 prp; 0-6 aty)
% Number of functors : 47 ( 47 usr; 14 con; 0-5 aty)
% Number of variables : 29 ( 28 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ m1_functor0 > m3_pboole > v9_functor0 > v8_functor0 > v6_functor0 > v21_functor0 > v1_funct_2 > v16_functor0 > v14_functor0 > v12_functor0 > v11_functor0 > m2_relset_1 > m2_functor0 > m1_relset_1 > l2_functor0 > l1_functor0 > r2_hidden > r2_functor0 > r1_tarski > m1_subset_1 > m1_pboole > v9_altcat_1 > v6_altcat_1 > v5_membered > v4_yellow18 > v4_ordinal2 > v4_membered > v3_yellow21 > v3_yellow18 > v3_struct_0 > v3_membered > v2_yellow21 > v2_yellow18 > v2_setfam_1 > v2_membered > v2_funct_1 > v2_altcat_1 > v1_yellow21 > v1_xreal_0 > v1_xcmplx_0 > v1_xboole_0 > v1_relat_1 > v1_rat_1 > v1_membered > v1_int_1 > v1_funct_1 > v1_funcop_1 > v1_finset_1 > v1_altcat_2 > v12_altcat_1 > v11_altcat_1 > l2_altcat_1 > l1_struct_0 > l1_altcat_1 > g2_functor0 > u2_functor0 > u1_functor0 > k3_zfmisc_1 > k3_altcat_1 > g2_altcat_1 > k2_zfmisc_1 > k2_altcat_1 > #nlpp > u2_altcat_1 > u1_struct_0 > u1_altcat_1 > k6_waybel34 > k5_waybel34 > k4_waybel34 > k1_zfmisc_1 > k1_xboole_0 > #skF_9 > #skF_21 > #skF_20 > #skF_18 > #skF_17 > #skF_24 > #skF_30 > #skF_15 > #skF_25 > #skF_19 > #skF_31 > #skF_13 > #skF_16 > #skF_12 > #skF_8 > #skF_5 > #skF_28 > #skF_6 > #skF_10 > #skF_3 > #skF_1 > #skF_26 > #skF_23 > #skF_14 > #skF_11 > #skF_22 > #skF_29 > #skF_2 > #skF_7 > #skF_27 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(k4_waybel34,type,
k4_waybel34: $i > $i ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(u2_altcat_1,type,
u2_altcat_1: $i > $i ).
tff(v6_altcat_1,type,
v6_altcat_1: $i > $o ).
tff(m2_functor0,type,
m2_functor0: ( $i * $i * $i ) > $o ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff(m1_functor0,type,
m1_functor0: ( $i * $i * $i * $i * $i * $i ) > $o ).
tff('#skF_20',type,
'#skF_20': $i ).
tff(v1_funct_1,type,
v1_funct_1: $i > $o ).
tff(v2_funct_1,type,
v2_funct_1: $i > $o ).
tff('#skF_18',type,
'#skF_18': $i ).
tff(g2_altcat_1,type,
g2_altcat_1: ( $i * $i * $i ) > $i ).
tff('#skF_17',type,
'#skF_17': $i ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff(v11_functor0,type,
v11_functor0: ( $i * $i * $i ) > $o ).
tff(r2_functor0,type,
r2_functor0: ( $i * $i ) > $o ).
tff(v21_functor0,type,
v21_functor0: ( $i * $i * $i ) > $o ).
tff('#skF_30',type,
'#skF_30': ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(l2_altcat_1,type,
l2_altcat_1: $i > $o ).
tff(v1_int_1,type,
v1_int_1: $i > $o ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(u1_functor0,type,
u1_functor0: ( $i * $i * $i ) > $i ).
tff(m1_pboole,type,
m1_pboole: ( $i * $i ) > $o ).
tff(v16_functor0,type,
v16_functor0: ( $i * $i * $i ) > $o ).
tff(k6_waybel34,type,
k6_waybel34: $i > $i ).
tff(k5_waybel34,type,
k5_waybel34: $i > $i ).
tff(k3_altcat_1,type,
k3_altcat_1: ( $i * $i * $i ) > $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff('#skF_31',type,
'#skF_31': ( $i * $i ) > $i ).
tff(v6_functor0,type,
v6_functor0: ( $i * $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_16',type,
'#skF_16': $i ).
tff(u2_functor0,type,
u2_functor0: ( $i * $i * $i ) > $i ).
tff(v4_ordinal2,type,
v4_ordinal2: $i > $o ).
tff(v4_yellow18,type,
v4_yellow18: $i > $o ).
tff(l1_altcat_1,type,
l1_altcat_1: $i > $o ).
tff(v3_yellow18,type,
v3_yellow18: $i > $o ).
tff('#skF_12',type,
'#skF_12': ( $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i * $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff(v8_functor0,type,
v8_functor0: ( $i * $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff(v3_membered,type,
v3_membered: $i > $o ).
tff(v2_yellow18,type,
v2_yellow18: $i > $o ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(m3_pboole,type,
m3_pboole: ( $i * $i * $i * $i ) > $o ).
tff(g2_functor0,type,
g2_functor0: ( $i * $i * $i * $i ) > $i ).
tff(v1_xreal_0,type,
v1_xreal_0: $i > $o ).
tff(v2_setfam_1,type,
v2_setfam_1: $i > $o ).
tff(k2_altcat_1,type,
k2_altcat_1: ( $i * $i ) > $i ).
tff(l2_functor0,type,
l2_functor0: ( $i * $i * $i ) > $o ).
tff(k3_zfmisc_1,type,
k3_zfmisc_1: ( $i * $i * $i ) > $i ).
tff(v5_membered,type,
v5_membered: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(v9_functor0,type,
v9_functor0: ( $i * $i * $i ) > $o ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff(v14_functor0,type,
v14_functor0: ( $i * $i * $i ) > $o ).
tff(v2_membered,type,
v2_membered: $i > $o ).
tff(v1_membered,type,
v1_membered: $i > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff(v1_xcmplx_0,type,
v1_xcmplx_0: $i > $o ).
tff('#skF_23',type,
'#skF_23': ( $i * $i ) > $i ).
tff(v12_altcat_1,type,
v12_altcat_1: $i > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i * $i ) > $i ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff(l1_functor0,type,
l1_functor0: ( $i * $i * $i ) > $o ).
tff(v9_altcat_1,type,
v9_altcat_1: $i > $o ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff(v1_altcat_2,type,
v1_altcat_2: $i > $o ).
tff(v2_altcat_1,type,
v2_altcat_1: $i > $o ).
tff(v12_functor0,type,
v12_functor0: ( $i * $i * $i ) > $o ).
tff(v2_yellow21,type,
v2_yellow21: $i > $o ).
tff('#skF_29',type,
'#skF_29': $i ).
tff(v1_funcop_1,type,
v1_funcop_1: $i > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(v11_altcat_1,type,
v11_altcat_1: $i > $o ).
tff(v1_rat_1,type,
v1_rat_1: $i > $o ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff('#skF_27',type,
'#skF_27': ( $i * $i ) > $i ).
tff(v4_membered,type,
v4_membered: $i > $o ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v3_yellow21,type,
v3_yellow21: $i > $o ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(v1_finset_1,type,
v1_finset_1: $i > $o ).
tff(u1_altcat_1,type,
u1_altcat_1: $i > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(v1_yellow21,type,
v1_yellow21: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(f_35,negated_conjecture,
~ ! [A] :
( ~ v2_setfam_1(A)
=> r2_functor0(k4_waybel34(A),k5_waybel34(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_waybel34) ).
tff(f_812,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',fc6_waybel34) ).
tff(f_299,axiom,
! [A] :
( ~ v2_setfam_1(A)
=> ~ v1_xboole_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
tff(f_521,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',dt_k4_waybel34) ).
tff(f_539,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
tff(f_548,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',dt_k6_waybel34) ).
tff(f_843,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',fc7_waybel34) ).
tff(f_468,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& v2_altcat_1(A)
& v12_altcat_1(A)
& l2_altcat_1(A) )
=> ! [B] :
( ( ~ v3_struct_0(B)
& v2_altcat_1(B)
& v12_altcat_1(B)
& l2_altcat_1(B) )
=> ( r2_functor0(A,B)
<=> ? [C] :
( m2_functor0(C,A,B)
& v21_functor0(C,A,B)
& v16_functor0(C,A,B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d41_functor0) ).
tff(f_771,axiom,
! [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/sandbox2/benchmark/theBenchmark.p',fc5_waybel34) ).
tff(c_4,plain,
~ v2_setfam_1('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_362,plain,
! [A_178] :
( v2_altcat_1(k5_waybel34(A_178))
| v2_setfam_1(A_178) ),
inference(cnfTransformation,[status(thm)],[f_812]) ).
tff(c_580,plain,
! [A_255] :
( ~ v1_xboole_0(A_255)
| v2_setfam_1(A_255) ),
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_588,plain,
~ v1_xboole_0('#skF_1'),
inference(resolution,[status(thm)],[c_580,c_4]) ).
tff(c_198,plain,
! [A_104] :
( l2_altcat_1(k4_waybel34(A_104))
| v1_xboole_0(A_104) ),
inference(cnfTransformation,[status(thm)],[f_521]) ).
tff(c_354,plain,
! [A_178] :
( v12_altcat_1(k5_waybel34(A_178))
| v2_setfam_1(A_178) ),
inference(cnfTransformation,[status(thm)],[f_812]) ).
tff(c_202,plain,
! [A_104] :
( v12_altcat_1(k4_waybel34(A_104))
| v1_xboole_0(A_104) ),
inference(cnfTransformation,[status(thm)],[f_521]) ).
tff(c_212,plain,
! [A_105] :
( l2_altcat_1(k5_waybel34(A_105))
| v1_xboole_0(A_105) ),
inference(cnfTransformation,[status(thm)],[f_539]) ).
tff(c_208,plain,
! [A_104] :
( v2_altcat_1(k4_waybel34(A_104))
| v1_xboole_0(A_104) ),
inference(cnfTransformation,[status(thm)],[f_521]) ).
tff(c_226,plain,
! [A_106] :
( m2_functor0(k6_waybel34(A_106),k4_waybel34(A_106),k5_waybel34(A_106))
| v2_setfam_1(A_106) ),
inference(cnfTransformation,[status(thm)],[f_548]) ).
tff(c_374,plain,
! [A_182] :
( v16_functor0(k6_waybel34(A_182),k4_waybel34(A_182),k5_waybel34(A_182))
| v2_setfam_1(A_182) ),
inference(cnfTransformation,[status(thm)],[f_843]) ).
tff(c_372,plain,
! [A_182] :
( v21_functor0(k6_waybel34(A_182),k4_waybel34(A_182),k5_waybel34(A_182))
| v2_setfam_1(A_182) ),
inference(cnfTransformation,[status(thm)],[f_843]) ).
tff(c_3930,plain,
! [A_976,B_977,C_978] :
( r2_functor0(A_976,B_977)
| ~ v16_functor0(C_978,A_976,B_977)
| ~ v21_functor0(C_978,A_976,B_977)
| ~ m2_functor0(C_978,A_976,B_977)
| ~ l2_altcat_1(B_977)
| ~ v12_altcat_1(B_977)
| ~ v2_altcat_1(B_977)
| v3_struct_0(B_977)
| ~ l2_altcat_1(A_976)
| ~ v12_altcat_1(A_976)
| ~ v2_altcat_1(A_976)
| v3_struct_0(A_976) ),
inference(cnfTransformation,[status(thm)],[f_468]) ).
tff(c_7643,plain,
! [A_1373] :
( r2_functor0(k4_waybel34(A_1373),k5_waybel34(A_1373))
| ~ v16_functor0(k6_waybel34(A_1373),k4_waybel34(A_1373),k5_waybel34(A_1373))
| ~ m2_functor0(k6_waybel34(A_1373),k4_waybel34(A_1373),k5_waybel34(A_1373))
| ~ l2_altcat_1(k5_waybel34(A_1373))
| ~ v12_altcat_1(k5_waybel34(A_1373))
| ~ v2_altcat_1(k5_waybel34(A_1373))
| v3_struct_0(k5_waybel34(A_1373))
| ~ l2_altcat_1(k4_waybel34(A_1373))
| ~ v12_altcat_1(k4_waybel34(A_1373))
| ~ v2_altcat_1(k4_waybel34(A_1373))
| v3_struct_0(k4_waybel34(A_1373))
| v2_setfam_1(A_1373) ),
inference(resolution,[status(thm)],[c_372,c_3930]) ).
tff(c_13161,plain,
! [A_1916] :
( r2_functor0(k4_waybel34(A_1916),k5_waybel34(A_1916))
| ~ m2_functor0(k6_waybel34(A_1916),k4_waybel34(A_1916),k5_waybel34(A_1916))
| ~ l2_altcat_1(k5_waybel34(A_1916))
| ~ v12_altcat_1(k5_waybel34(A_1916))
| ~ v2_altcat_1(k5_waybel34(A_1916))
| v3_struct_0(k5_waybel34(A_1916))
| ~ l2_altcat_1(k4_waybel34(A_1916))
| ~ v12_altcat_1(k4_waybel34(A_1916))
| ~ v2_altcat_1(k4_waybel34(A_1916))
| v3_struct_0(k4_waybel34(A_1916))
| v2_setfam_1(A_1916) ),
inference(resolution,[status(thm)],[c_374,c_7643]) ).
tff(c_16588,plain,
! [A_2476] :
( r2_functor0(k4_waybel34(A_2476),k5_waybel34(A_2476))
| ~ l2_altcat_1(k5_waybel34(A_2476))
| ~ v12_altcat_1(k5_waybel34(A_2476))
| ~ v2_altcat_1(k5_waybel34(A_2476))
| v3_struct_0(k5_waybel34(A_2476))
| ~ l2_altcat_1(k4_waybel34(A_2476))
| ~ v12_altcat_1(k4_waybel34(A_2476))
| ~ v2_altcat_1(k4_waybel34(A_2476))
| v3_struct_0(k4_waybel34(A_2476))
| v2_setfam_1(A_2476) ),
inference(resolution,[status(thm)],[c_226,c_13161]) ).
tff(c_2,plain,
~ r2_functor0(k4_waybel34('#skF_1'),k5_waybel34('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_16593,plain,
( ~ l2_altcat_1(k5_waybel34('#skF_1'))
| ~ v12_altcat_1(k5_waybel34('#skF_1'))
| ~ v2_altcat_1(k5_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1'))
| ~ l2_altcat_1(k4_waybel34('#skF_1'))
| ~ v12_altcat_1(k4_waybel34('#skF_1'))
| ~ v2_altcat_1(k4_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1'))
| v2_setfam_1('#skF_1') ),
inference(resolution,[status(thm)],[c_16588,c_2]) ).
tff(c_16597,plain,
( ~ l2_altcat_1(k5_waybel34('#skF_1'))
| ~ v12_altcat_1(k5_waybel34('#skF_1'))
| ~ v2_altcat_1(k5_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1'))
| ~ l2_altcat_1(k4_waybel34('#skF_1'))
| ~ v12_altcat_1(k4_waybel34('#skF_1'))
| ~ v2_altcat_1(k4_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1')) ),
inference(negUnitSimplification,[status(thm)],[c_4,c_16593]) ).
tff(c_16598,plain,
~ v2_altcat_1(k4_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16597]) ).
tff(c_16601,plain,
v1_xboole_0('#skF_1'),
inference(resolution,[status(thm)],[c_208,c_16598]) ).
tff(c_16608,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_588,c_16601]) ).
tff(c_16609,plain,
( ~ v12_altcat_1(k4_waybel34('#skF_1'))
| ~ l2_altcat_1(k4_waybel34('#skF_1'))
| ~ v2_altcat_1(k5_waybel34('#skF_1'))
| ~ v12_altcat_1(k5_waybel34('#skF_1'))
| ~ l2_altcat_1(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16597]) ).
tff(c_16691,plain,
~ l2_altcat_1(k5_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16609]) ).
tff(c_16694,plain,
v1_xboole_0('#skF_1'),
inference(resolution,[status(thm)],[c_212,c_16691]) ).
tff(c_16698,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_588,c_16694]) ).
tff(c_16699,plain,
( ~ v12_altcat_1(k5_waybel34('#skF_1'))
| ~ v2_altcat_1(k5_waybel34('#skF_1'))
| ~ l2_altcat_1(k4_waybel34('#skF_1'))
| ~ v12_altcat_1(k4_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16609]) ).
tff(c_16705,plain,
~ v12_altcat_1(k4_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16699]) ).
tff(c_16708,plain,
v1_xboole_0('#skF_1'),
inference(resolution,[status(thm)],[c_202,c_16705]) ).
tff(c_16715,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_588,c_16708]) ).
tff(c_16716,plain,
( ~ l2_altcat_1(k4_waybel34('#skF_1'))
| ~ v2_altcat_1(k5_waybel34('#skF_1'))
| ~ v12_altcat_1(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16699]) ).
tff(c_16732,plain,
~ v12_altcat_1(k5_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16716]) ).
tff(c_16735,plain,
v2_setfam_1('#skF_1'),
inference(resolution,[status(thm)],[c_354,c_16732]) ).
tff(c_16742,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_16735]) ).
tff(c_16743,plain,
( ~ v2_altcat_1(k5_waybel34('#skF_1'))
| ~ l2_altcat_1(k4_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16716]) ).
tff(c_16745,plain,
~ l2_altcat_1(k4_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16743]) ).
tff(c_16748,plain,
v1_xboole_0('#skF_1'),
inference(resolution,[status(thm)],[c_198,c_16745]) ).
tff(c_16752,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_588,c_16748]) ).
tff(c_16753,plain,
( ~ v2_altcat_1(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1'))
| v3_struct_0(k5_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16743]) ).
tff(c_16759,plain,
~ v2_altcat_1(k5_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16753]) ).
tff(c_16776,plain,
v2_setfam_1('#skF_1'),
inference(resolution,[status(thm)],[c_362,c_16759]) ).
tff(c_16783,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_16776]) ).
tff(c_16784,plain,
( v3_struct_0(k5_waybel34('#skF_1'))
| v3_struct_0(k4_waybel34('#skF_1')) ),
inference(splitRight,[status(thm)],[c_16753]) ).
tff(c_16786,plain,
v3_struct_0(k4_waybel34('#skF_1')),
inference(splitLeft,[status(thm)],[c_16784]) ).
tff(c_326,plain,
! [A_177] :
( ~ v3_struct_0(k4_waybel34(A_177))
| v2_setfam_1(A_177) ),
inference(cnfTransformation,[status(thm)],[f_771]) ).
tff(c_16789,plain,
v2_setfam_1('#skF_1'),
inference(resolution,[status(thm)],[c_16786,c_326]) ).
tff(c_16796,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_16789]) ).
tff(c_16797,plain,
v3_struct_0(k5_waybel34('#skF_1')),
inference(splitRight,[status(thm)],[c_16784]) ).
tff(c_364,plain,
! [A_178] :
( ~ v3_struct_0(k5_waybel34(A_178))
| v2_setfam_1(A_178) ),
inference(cnfTransformation,[status(thm)],[f_812]) ).
tff(c_16801,plain,
v2_setfam_1('#skF_1'),
inference(resolution,[status(thm)],[c_16797,c_364]) ).
tff(c_16808,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_16801]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : LAT362+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 04:46:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 24.68/10.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.68/10.70
% 24.68/10.70 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------