%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LAT369+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 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 : Wed Apr 9 07:12:07 PM UTC 2025
% Result : Theorem 121.28s 97.43s
% Output : CNFRefutation 121.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 24
% Syntax : Number of formulae : 166 ( 59 unt; 0 typ; 0 def)
% Number of atoms : 793 ( 5 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 1028 ( 401 ~; 398 |; 179 &)
% ( 2 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 61 ( 59 usr; 1 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 15 con; 0-3 aty)
% Number of variables : 118 ( 118 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ v5_waybel_1 > v5_orders_3 > v4_waybel_1 > v2_funct_2 > v23_waybel_0 > v22_waybel_0 > v21_waybel_0 > v20_waybel_0 > v1_waybel34 > v1_partfun1 > v1_funct_2 > v19_waybel_0 > v18_waybel_0 > v17_waybel_0 > m2_relset_1 > m1_relset_1 > v8_waybel_1 > v7_yellow_0 > v7_waybel_1 > v6_waybel_1 > v5_yellow_0 > v4_yellow_0 > v4_waybel_0 > v3_waybel_0 > r2_hidden > r1_tarski > m1_yellow_0 > m1_subset_1 > v5_membered > v4_ordinal2 > v4_orders_2 > v4_membered > v3_yellow_0 > v3_struct_0 > v3_orders_2 > v3_membered > v3_lattice3 > v2_yellow_0 > v2_orders_2 > v2_membered > v2_lattice3 > v2_funct_1 > v25_waybel_0 > v24_waybel_0 > v1_yellow_0 > v1_xreal_0 > v1_xcmplx_0 > v1_xboole_0 > v1_relat_1 > v1_rat_1 > v1_orders_2 > v1_membered > v1_lattice3 > v1_int_1 > v1_funct_1 > v1_finset_1 > v11_quantal1 > l1_struct_0 > l1_orders_2 > k3_waybel_1 > k2_yellow_2 > k2_waybel_1 > k2_waybel34 > k1_waybel34 > k8_relat_1 > k2_zfmisc_1 > g1_orders_2 > #nlpp > u1_struct_0 > u1_orders_2 > k7_grcat_1 > k1_zfmisc_1 > k1_xboole_0 > #skF_7 > #skF_21 > #skF_16 > #skF_18 > #skF_11 > #skF_25 > #skF_19 > #skF_31 > #skF_13 > #skF_10 > #skF_29 > #skF_32 > #skF_14 > #skF_2 > #skF_3 > #skF_1 > #skF_8 > #skF_9 > #skF_23 > #skF_28 > #skF_26 > #skF_4 > #skF_17 > #skF_22 > #skF_24 > #skF_27 > #skF_5 > #skF_30 > #skF_15 > #skF_6 > #skF_12 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v1_orders_2,type,
v1_orders_2: $i > $o ).
tff(v5_yellow_0,type,
v5_yellow_0: ( $i * $i ) > $o ).
tff(k8_relat_1,type,
k8_relat_1: ( $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff(k2_waybel_1,type,
k2_waybel_1: ( $i * $i * $i ) > $i ).
tff(m2_relset_1,type,
m2_relset_1: ( $i * $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(v3_orders_2,type,
v3_orders_2: $i > $o ).
tff(v4_waybel_0,type,
v4_waybel_0: ( $i * $i ) > $o ).
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(v3_yellow_0,type,
v3_yellow_0: $i > $o ).
tff(k7_grcat_1,type,
k7_grcat_1: $i > $i ).
tff(r2_hidden,type,
r2_hidden: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(v1_partfun1,type,
v1_partfun1: ( $i * $i * $i ) > $o ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(v1_int_1,type,
v1_int_1: $i > $o ).
tff(k1_xboole_0,type,
k1_xboole_0: $i ).
tff(v4_yellow_0,type,
v4_yellow_0: ( $i * $i ) > $o ).
tff(v21_waybel_0,type,
v21_waybel_0: ( $i * $i * $i ) > $o ).
tff(v7_waybel_1,type,
v7_waybel_1: ( $i * $i ) > $o ).
tff('#skF_19',type,
'#skF_19': $i ).
tff('#skF_31',type,
'#skF_31': ( $i * $i ) > $i ).
tff(v5_orders_3,type,
v5_orders_3: ( $i * $i * $i ) > $o ).
tff(v3_lattice3,type,
v3_lattice3: $i > $o ).
tff(v3_waybel_0,type,
v3_waybel_0: ( $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff(r1_tarski,type,
r1_tarski: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(v22_waybel_0,type,
v22_waybel_0: ( $i * $i * $i ) > $o ).
tff(m1_relset_1,type,
m1_relset_1: ( $i * $i * $i ) > $o ).
tff(v4_ordinal2,type,
v4_ordinal2: $i > $o ).
tff(g1_orders_2,type,
g1_orders_2: ( $i * $i ) > $i ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff('#skF_32',type,
'#skF_32': $i > $i ).
tff(v1_lattice3,type,
v1_lattice3: $i > $o ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(v1_funct_2,type,
v1_funct_2: ( $i * $i * $i ) > $o ).
tff(v8_waybel_1,type,
v8_waybel_1: ( $i * $i ) > $o ).
tff(v2_yellow_0,type,
v2_yellow_0: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff(v20_waybel_0,type,
v20_waybel_0: ( $i * $i * $i ) > $o ).
tff(v3_membered,type,
v3_membered: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(v18_waybel_0,type,
v18_waybel_0: ( $i * $i * $i ) > $o ).
tff(v11_quantal1,type,
v11_quantal1: $i > $o ).
tff(v4_orders_2,type,
v4_orders_2: $i > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(v7_yellow_0,type,
v7_yellow_0: ( $i * $i ) > $o ).
tff(v2_funct_2,type,
v2_funct_2: ( $i * $i * $i ) > $o ).
tff(v1_xreal_0,type,
v1_xreal_0: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(v5_membered,type,
v5_membered: $i > $o ).
tff(k1_zfmisc_1,type,
k1_zfmisc_1: $i > $i ).
tff(m1_yellow_0,type,
m1_yellow_0: ( $i * $i ) > $o ).
tff(v2_orders_2,type,
v2_orders_2: $i > $o ).
tff(l1_struct_0,type,
l1_struct_0: $i > $o ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff(v2_membered,type,
v2_membered: $i > $o ).
tff(v1_membered,type,
v1_membered: $i > $o ).
tff(l1_orders_2,type,
l1_orders_2: $i > $o ).
tff('#skF_28',type,
'#skF_28': ( $i * $i ) > $i ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff(v1_xcmplx_0,type,
v1_xcmplx_0: $i > $o ).
tff(v17_waybel_0,type,
v17_waybel_0: ( $i * $i * $i ) > $o ).
tff(v6_waybel_1,type,
v6_waybel_1: ( $i * $i ) > $o ).
tff(v1_relat_1,type,
v1_relat_1: $i > $o ).
tff(k2_zfmisc_1,type,
k2_zfmisc_1: ( $i * $i ) > $i ).
tff(v19_waybel_0,type,
v19_waybel_0: ( $i * $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i ).
tff(k2_yellow_2,type,
k2_yellow_2: ( $i * $i * $i ) > $i ).
tff(k2_waybel34,type,
k2_waybel34: ( $i * $i * $i ) > $i ).
tff('#skF_24',type,
'#skF_24': $i ).
tff(v25_waybel_0,type,
v25_waybel_0: $i > $o ).
tff(v5_waybel_1,type,
v5_waybel_1: ( $i * $i * $i ) > $o ).
tff(v1_rat_1,type,
v1_rat_1: $i > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff(v2_lattice3,type,
v2_lattice3: $i > $o ).
tff(u1_orders_2,type,
u1_orders_2: $i > $i ).
tff(v23_waybel_0,type,
v23_waybel_0: ( $i * $i * $i ) > $o ).
tff(v4_membered,type,
v4_membered: $i > $o ).
tff(k3_waybel_1,type,
k3_waybel_1: ( $i * $i * $i ) > $i ).
tff(u1_struct_0,type,
u1_struct_0: $i > $i ).
tff(v24_waybel_0,type,
v24_waybel_0: $i > $o ).
tff(v1_xboole_0,type,
v1_xboole_0: $i > $o ).
tff(k1_waybel34,type,
k1_waybel34: ( $i * $i * $i ) > $i ).
tff(v1_finset_1,type,
v1_finset_1: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff(v1_waybel34,type,
v1_waybel34: ( $i * $i * $i ) > $o ).
tff('#skF_30',type,
'#skF_30': $i > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff(v1_yellow_0,type,
v1_yellow_0: $i > $o ).
tff(v3_struct_0,type,
v3_struct_0: $i > $o ).
tff(m1_subset_1,type,
m1_subset_1: ( $i * $i ) > $o ).
tff(v4_waybel_1,type,
v4_waybel_1: ( $i * $i * $i ) > $o ).
tff(f_57,negated_conjecture,
~ ! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)
=> v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_waybel34) ).
tff(f_2445,axiom,
! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)
<=> v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_waybel34) ).
tff(f_713,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v3_lattice3(A) )
=> ( ~ v3_struct_0(A)
& v3_yellow_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_yellow_0) ).
tff(f_750,axiom,
! [A] :
( l1_orders_2(A)
=> ( v3_yellow_0(A)
=> ( v1_yellow_0(A)
& v2_yellow_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc4_yellow_0) ).
tff(f_600,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
tff(f_93,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_lattice3(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v24_waybel_0(A)
& v25_waybel_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc10_waybel_0) ).
tff(f_337,axiom,
! [A] :
( l1_orders_2(A)
=> ( v1_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
tff(f_559,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v2_yellow_0(A)
& v24_waybel_0(A)
& v25_waybel_0(A) )
=> ( ~ v3_struct_0(A)
& v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_yellow_0(A)
& v2_yellow_0(A)
& v3_yellow_0(A)
& v24_waybel_0(A)
& v25_waybel_0(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_2) ).
tff(f_2329,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
tff(f_1092,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A)
& ~ v3_struct_0(B)
& l1_orders_2(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v1_funct_1(k3_waybel_1(A,B,C))
& v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
& m2_relset_1(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
tff(f_517,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( ~ v3_struct_0(A)
& v3_lattice3(A) )
=> ( ~ v3_struct_0(A)
& v1_lattice3(A)
& v2_lattice3(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
tff(f_1493,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A)
& ~ v3_struct_0(B)
& l1_orders_2(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( ~ v3_struct_0(k2_yellow_2(A,B,C))
& v1_orders_2(k2_yellow_2(A,B,C))
& v4_yellow_0(k2_yellow_2(A,B,C),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_yellow_2) ).
tff(f_1070,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A)
& ~ v3_struct_0(B)
& l1_orders_2(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v1_orders_2(k2_yellow_2(A,B,C))
& v4_yellow_0(k2_yellow_2(A,B,C),B)
& m1_yellow_0(k2_yellow_2(A,B,C),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
tff(f_1115,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_yellow_0(B,A)
=> l1_orders_2(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
tff(f_372,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
=> ( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v6_waybel_1(B,A) )
=> ( v1_funct_1(B)
& ~ v1_xboole_0(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_partfun1(B,u1_struct_0(A),u1_struct_0(A))
& v11_quantal1(B)
& v5_orders_3(B,A,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_waybel10) ).
tff(f_701,axiom,
! [A] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
=> ( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A) )
=> ( v1_funct_1(B)
& ~ v1_xboole_0(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_partfun1(B,u1_struct_0(A),u1_struct_0(A))
& v6_waybel_1(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_waybel_1) ).
tff(f_1230,axiom,
! [A,B] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A)
& v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v6_waybel_1(B,A)
& m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
=> ( ~ v3_struct_0(k2_yellow_2(A,A,B))
& v1_orders_2(k2_yellow_2(A,A,B))
& v2_orders_2(k2_yellow_2(A,A,B))
& v3_orders_2(k2_yellow_2(A,A,B))
& v4_orders_2(k2_yellow_2(A,A,B))
& v1_yellow_0(k2_yellow_2(A,A,B))
& v2_yellow_0(k2_yellow_2(A,A,B))
& v3_yellow_0(k2_yellow_2(A,A,B))
& v4_yellow_0(k2_yellow_2(A,A,B),A)
& v24_waybel_0(k2_yellow_2(A,A,B))
& v25_waybel_0(k2_yellow_2(A,A,B))
& v1_lattice3(k2_yellow_2(A,A,B))
& v2_lattice3(k2_yellow_2(A,A,B))
& v3_lattice3(k2_yellow_2(A,A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel34) ).
tff(f_798,axiom,
! [A] :
( ( v2_orders_2(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_yellow_0(B,A)
=> ( v4_yellow_0(B,A)
=> ( v2_orders_2(B)
& v4_yellow_0(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_yellow_0) ).
tff(f_838,axiom,
! [A] :
( ( v3_orders_2(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_yellow_0(B,A)
=> ( v4_yellow_0(B,A)
=> ( v3_orders_2(B)
& v4_yellow_0(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc7_yellow_0) ).
tff(f_878,axiom,
! [A] :
( ( v4_orders_2(A)
& l1_orders_2(A) )
=> ! [B] :
( m1_yellow_0(B,A)
=> ( v4_yellow_0(B,A)
=> ( v4_orders_2(B)
& v4_yellow_0(B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc8_yellow_0) ).
tff(f_1740,axiom,
! [A,B,C] :
( ( ~ v3_struct_0(A)
& l1_orders_2(A)
& ~ v3_struct_0(B)
& l1_orders_2(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v1_relat_1(k3_waybel_1(A,B,C))
& v1_funct_1(k3_waybel_1(A,B,C))
& v2_funct_1(k3_waybel_1(A,B,C))
& ~ v1_xboole_0(k3_waybel_1(A,B,C))
& v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
& v1_partfun1(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
& v5_orders_3(k3_waybel_1(A,B,C),k2_yellow_2(A,B,C),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_waybel_1) ).
tff(f_2414,axiom,
! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( v1_funct_1(B)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
=> ( v18_waybel_0(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))
& v17_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)
& ( k2_waybel34(k2_yellow_2(A,A,B),A,k2_waybel_1(A,A,B)) = k3_waybel_1(A,A,B) )
& ( k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B)) = k2_waybel_1(A,A,B) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_waybel34) ).
tff(f_1366,axiom,
! [A,B,C] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A)
& v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& v2_lattice3(B)
& v3_lattice3(B)
& l1_orders_2(B)
& v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v17_waybel_0(C,A,B)
& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v1_relat_1(k1_waybel34(A,B,C))
& v1_funct_1(k1_waybel34(A,B,C))
& ~ v1_xboole_0(k1_waybel34(A,B,C))
& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_partfun1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v18_waybel_0(k1_waybel34(A,B,C),B,A)
& v20_waybel_0(k1_waybel34(A,B,C),B,A)
& v22_waybel_0(k1_waybel34(A,B,C),B,A)
& v5_waybel_1(k1_waybel34(A,B,C),A,B)
& v5_orders_3(k1_waybel34(A,B,C),B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_waybel34) ).
tff(f_2377,axiom,
! [A] :
( ( v2_orders_2(A)
& v3_orders_2(A)
& v4_orders_2(A)
& v1_lattice3(A)
& v2_lattice3(A)
& v3_lattice3(A)
& l1_orders_2(A) )
=> ! [B] :
( ( v2_orders_2(B)
& v3_orders_2(B)
& v4_orders_2(B)
& v1_lattice3(B)
& v2_lattice3(B)
& v3_lattice3(B)
& l1_orders_2(B) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v17_waybel_0(C,A,B)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
=> ( v22_waybel_0(C,A,B)
=> v1_waybel34(k1_waybel34(A,B,C),B,A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_waybel34) ).
tff(c_26,plain,
v2_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_24,plain,
v3_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_22,plain,
v4_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_20,plain,
v1_lattice3('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_18,plain,
v2_lattice3('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_16,plain,
v3_lattice3('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_14,plain,
l1_orders_2('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_12,plain,
v1_funct_1('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_10,plain,
v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_8,plain,
v7_waybel_1('#skF_2','#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_6,plain,
m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_4,plain,
v4_waybel_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_1146,plain,
! [A_276,B_278] :
( v22_waybel_0(k3_waybel_1(A_276,A_276,B_278),k2_yellow_2(A_276,A_276,B_278),A_276)
| ~ v4_waybel_0(k2_yellow_2(A_276,A_276,B_278),A_276)
| ~ m2_relset_1(B_278,u1_struct_0(A_276),u1_struct_0(A_276))
| ~ v7_waybel_1(B_278,A_276)
| ~ v1_funct_2(B_278,u1_struct_0(A_276),u1_struct_0(A_276))
| ~ v1_funct_1(B_278)
| ~ l1_orders_2(A_276)
| ~ v3_lattice3(A_276)
| ~ v2_lattice3(A_276)
| ~ v1_lattice3(A_276)
| ~ v4_orders_2(A_276)
| ~ v3_orders_2(A_276)
| ~ v2_orders_2(A_276) ),
inference(cnfTransformation,[status(thm)],[f_2445]) ).
tff(c_1952,plain,
! [A_457] :
( v3_yellow_0(A_457)
| ~ v3_lattice3(A_457)
| v3_struct_0(A_457)
| ~ l1_orders_2(A_457) ),
inference(cnfTransformation,[status(thm)],[f_713]) ).
tff(c_306,plain,
! [A_93] :
( v2_yellow_0(A_93)
| ~ v3_yellow_0(A_93)
| ~ l1_orders_2(A_93) ),
inference(cnfTransformation,[status(thm)],[f_750]) ).
tff(c_2784,plain,
! [A_563] :
( v2_yellow_0(A_563)
| ~ v3_lattice3(A_563)
| v3_struct_0(A_563)
| ~ l1_orders_2(A_563) ),
inference(resolution,[status(thm)],[c_1952,c_306]) ).
tff(c_258,plain,
! [A_75] :
( ~ v3_struct_0(A_75)
| ~ v2_lattice3(A_75)
| ~ l1_orders_2(A_75) ),
inference(cnfTransformation,[status(thm)],[f_600]) ).
tff(c_3351,plain,
! [A_691] :
( ~ v2_lattice3(A_691)
| v2_yellow_0(A_691)
| ~ v3_lattice3(A_691)
| ~ l1_orders_2(A_691) ),
inference(resolution,[status(thm)],[c_2784,c_258]) ).
tff(c_3366,plain,
( ~ v2_lattice3('#skF_1')
| v2_yellow_0('#skF_1')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_16,c_3351]) ).
tff(c_3381,plain,
v2_yellow_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_18,c_3366]) ).
tff(c_3538,plain,
! [A_703] :
( v24_waybel_0(A_703)
| ~ v3_lattice3(A_703)
| ~ v2_orders_2(A_703)
| v3_struct_0(A_703)
| ~ l1_orders_2(A_703) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_160,plain,
! [A_43] :
( ~ v3_struct_0(A_43)
| ~ v1_lattice3(A_43)
| ~ l1_orders_2(A_43) ),
inference(cnfTransformation,[status(thm)],[f_337]) ).
tff(c_4315,plain,
! [A_794] :
( ~ v1_lattice3(A_794)
| v24_waybel_0(A_794)
| ~ v3_lattice3(A_794)
| ~ v2_orders_2(A_794)
| ~ l1_orders_2(A_794) ),
inference(resolution,[status(thm)],[c_3538,c_160]) ).
tff(c_4330,plain,
( ~ v1_lattice3('#skF_1')
| v24_waybel_0('#skF_1')
| ~ v2_orders_2('#skF_1')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_16,c_4315]) ).
tff(c_4345,plain,
v24_waybel_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_26,c_20,c_4330]) ).
tff(c_3304,plain,
! [A_688] :
( v25_waybel_0(A_688)
| ~ v3_lattice3(A_688)
| ~ v2_orders_2(A_688)
| v3_struct_0(A_688)
| ~ l1_orders_2(A_688) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_4382,plain,
! [A_799] :
( ~ v1_lattice3(A_799)
| v25_waybel_0(A_799)
| ~ v3_lattice3(A_799)
| ~ v2_orders_2(A_799)
| ~ l1_orders_2(A_799) ),
inference(resolution,[status(thm)],[c_3304,c_160]) ).
tff(c_4397,plain,
( ~ v1_lattice3('#skF_1')
| v25_waybel_0('#skF_1')
| ~ v2_orders_2('#skF_1')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_16,c_4382]) ).
tff(c_4412,plain,
v25_waybel_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_26,c_20,c_4397]) ).
tff(c_6708,plain,
! [A_1100] :
( v3_yellow_0(A_1100)
| ~ v25_waybel_0(A_1100)
| ~ v24_waybel_0(A_1100)
| ~ v2_yellow_0(A_1100)
| ~ v4_orders_2(A_1100)
| ~ v3_orders_2(A_1100)
| ~ v2_orders_2(A_1100)
| v3_struct_0(A_1100)
| ~ l1_orders_2(A_1100) ),
inference(cnfTransformation,[status(thm)],[f_559]) ).
tff(c_6729,plain,
( v3_yellow_0('#skF_1')
| ~ v25_waybel_0('#skF_1')
| ~ v24_waybel_0('#skF_1')
| ~ v2_yellow_0('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1')
| v3_struct_0('#skF_1')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_22,c_6708]) ).
tff(c_6750,plain,
( v3_yellow_0('#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_26,c_24,c_3381,c_4345,c_4412,c_6729]) ).
tff(c_6779,plain,
v3_struct_0('#skF_1'),
inference(splitLeft,[status(thm)],[c_6750]) ).
tff(c_6782,plain,
( ~ v2_lattice3('#skF_1')
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_6779,c_258]) ).
tff(c_6789,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_18,c_6782]) ).
tff(c_6791,plain,
~ v3_struct_0('#skF_1'),
inference(splitRight,[status(thm)],[c_6750]) ).
tff(c_1990,plain,
! [C_464,A_465,B_466] :
( m1_relset_1(C_464,A_465,B_466)
| ~ m2_relset_1(C_464,A_465,B_466) ),
inference(cnfTransformation,[status(thm)],[f_2329]) ).
tff(c_2002,plain,
m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1')),
inference(resolution,[status(thm)],[c_6,c_1990]) ).
tff(c_396,plain,
! [A_148,B_149,C_150] :
( m2_relset_1(k3_waybel_1(A_148,B_149,C_150),u1_struct_0(k2_yellow_2(A_148,B_149,C_150)),u1_struct_0(B_149))
| ~ m1_relset_1(C_150,u1_struct_0(A_148),u1_struct_0(B_149))
| ~ v1_funct_2(C_150,u1_struct_0(A_148),u1_struct_0(B_149))
| ~ v1_funct_1(C_150)
| ~ l1_orders_2(B_149)
| v3_struct_0(B_149)
| ~ l1_orders_2(A_148)
| v3_struct_0(A_148) ),
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_2,plain,
~ v1_waybel34(k2_waybel_1('#skF_1','#skF_1','#skF_2'),'#skF_1',k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_212,plain,
! [A_66] :
( v1_lattice3(A_66)
| ~ v3_lattice3(A_66)
| v3_struct_0(A_66)
| ~ l1_orders_2(A_66) ),
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_8565,plain,
! [A_1253,B_1254,C_1255] :
( ~ v3_struct_0(k2_yellow_2(A_1253,B_1254,C_1255))
| ~ m1_relset_1(C_1255,u1_struct_0(A_1253),u1_struct_0(B_1254))
| ~ v1_funct_2(C_1255,u1_struct_0(A_1253),u1_struct_0(B_1254))
| ~ v1_funct_1(C_1255)
| ~ l1_orders_2(B_1254)
| v3_struct_0(B_1254)
| ~ l1_orders_2(A_1253)
| v3_struct_0(A_1253) ),
inference(cnfTransformation,[status(thm)],[f_1493]) ).
tff(c_8595,plain,
( ~ v3_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_8565]) ).
tff(c_8607,plain,
( ~ v3_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_8595]) ).
tff(c_8608,plain,
~ v3_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_6791,c_8607]) ).
tff(c_8636,plain,
( v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_212,c_8608]) ).
tff(c_8639,plain,
~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitLeft,[status(thm)],[c_8636]) ).
tff(c_9658,plain,
! [A_1349,B_1350,C_1351] :
( m1_yellow_0(k2_yellow_2(A_1349,B_1350,C_1351),B_1350)
| ~ m1_relset_1(C_1351,u1_struct_0(A_1349),u1_struct_0(B_1350))
| ~ v1_funct_2(C_1351,u1_struct_0(A_1349),u1_struct_0(B_1350))
| ~ v1_funct_1(C_1351)
| ~ l1_orders_2(B_1350)
| v3_struct_0(B_1350)
| ~ l1_orders_2(A_1349)
| v3_struct_0(A_1349) ),
inference(cnfTransformation,[status(thm)],[f_1070]) ).
tff(c_9678,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_9658]) ).
tff(c_9690,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_9678]) ).
tff(c_9691,plain,
m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_6791,c_9690]) ).
tff(c_418,plain,
! [B_157,A_155] :
( l1_orders_2(B_157)
| ~ m1_yellow_0(B_157,A_155)
| ~ l1_orders_2(A_155) ),
inference(cnfTransformation,[status(thm)],[f_1115]) ).
tff(c_9694,plain,
( l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_9691,c_418]) ).
tff(c_9697,plain,
l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_9694]) ).
tff(c_9699,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8639,c_9697]) ).
tff(c_9701,plain,
l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_8636]) ).
tff(c_9700,plain,
( ~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(splitRight,[status(thm)],[c_8636]) ).
tff(c_9702,plain,
~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitLeft,[status(thm)],[c_9700]) ).
tff(c_7615,plain,
! [B_1199,A_1200] :
( ~ v1_xboole_0(B_1199)
| ~ v6_waybel_1(B_1199,A_1200)
| ~ v1_funct_2(B_1199,u1_struct_0(A_1200),u1_struct_0(A_1200))
| ~ v1_funct_1(B_1199)
| ~ m1_relset_1(B_1199,u1_struct_0(A_1200),u1_struct_0(A_1200))
| ~ l1_orders_2(A_1200)
| v3_struct_0(A_1200) ),
inference(cnfTransformation,[status(thm)],[f_372]) ).
tff(c_7648,plain,
( ~ v1_xboole_0('#skF_2')
| ~ v6_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_7615]) ).
tff(c_7660,plain,
( ~ v1_xboole_0('#skF_2')
| ~ v6_waybel_1('#skF_2','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_2002,c_12,c_7648]) ).
tff(c_7661,plain,
( ~ v1_xboole_0('#skF_2')
| ~ v6_waybel_1('#skF_2','#skF_1') ),
inference(negUnitSimplification,[status(thm)],[c_6791,c_7660]) ).
tff(c_7662,plain,
~ v6_waybel_1('#skF_2','#skF_1'),
inference(splitLeft,[status(thm)],[c_7661]) ).
tff(c_7934,plain,
! [B_1220,A_1221] :
( v6_waybel_1(B_1220,A_1221)
| ~ v7_waybel_1(B_1220,A_1221)
| ~ v1_funct_2(B_1220,u1_struct_0(A_1221),u1_struct_0(A_1221))
| ~ v1_funct_1(B_1220)
| ~ m1_relset_1(B_1220,u1_struct_0(A_1221),u1_struct_0(A_1221))
| ~ l1_orders_2(A_1221)
| v3_struct_0(A_1221) ),
inference(cnfTransformation,[status(thm)],[f_701]) ).
tff(c_7967,plain,
( v6_waybel_1('#skF_2','#skF_1')
| ~ v7_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_7934]) ).
tff(c_7979,plain,
( v6_waybel_1('#skF_2','#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_2002,c_12,c_8,c_7967]) ).
tff(c_7981,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6791,c_7662,c_7979]) ).
tff(c_7983,plain,
v6_waybel_1('#skF_2','#skF_1'),
inference(splitRight,[status(thm)],[c_7661]) ).
tff(c_28869,plain,
! [A_2629,B_2630] :
( v3_lattice3(k2_yellow_2(A_2629,A_2629,B_2630))
| ~ m1_relset_1(B_2630,u1_struct_0(A_2629),u1_struct_0(A_2629))
| ~ v6_waybel_1(B_2630,A_2629)
| ~ v1_funct_2(B_2630,u1_struct_0(A_2629),u1_struct_0(A_2629))
| ~ v1_funct_1(B_2630)
| ~ l1_orders_2(A_2629)
| ~ v3_lattice3(A_2629)
| ~ v2_lattice3(A_2629)
| ~ v1_lattice3(A_2629)
| ~ v4_orders_2(A_2629)
| ~ v3_orders_2(A_2629)
| ~ v2_orders_2(A_2629) ),
inference(cnfTransformation,[status(thm)],[f_1230]) ).
tff(c_28909,plain,
( v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v6_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_28869]) ).
tff(c_28925,plain,
v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_7983,c_2002,c_28909]) ).
tff(c_28927,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9702,c_28925]) ).
tff(c_28928,plain,
v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_9700]) ).
tff(c_28929,plain,
v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_9700]) ).
tff(c_3335,plain,
! [A_688] :
( ~ v1_lattice3(A_688)
| v25_waybel_0(A_688)
| ~ v3_lattice3(A_688)
| ~ v2_orders_2(A_688)
| ~ l1_orders_2(A_688) ),
inference(resolution,[status(thm)],[c_3304,c_160]) ).
tff(c_28938,plain,
( ~ v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| v25_waybel_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_28929,c_3335]) ).
tff(c_28968,plain,
( v25_waybel_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_9701,c_28928,c_28938]) ).
tff(c_28995,plain,
~ v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitLeft,[status(thm)],[c_28968]) ).
tff(c_30030,plain,
! [A_2722,B_2723,C_2724] :
( m1_yellow_0(k2_yellow_2(A_2722,B_2723,C_2724),B_2723)
| ~ m1_relset_1(C_2724,u1_struct_0(A_2722),u1_struct_0(B_2723))
| ~ v1_funct_2(C_2724,u1_struct_0(A_2722),u1_struct_0(B_2723))
| ~ v1_funct_1(C_2724)
| ~ l1_orders_2(B_2723)
| v3_struct_0(B_2723)
| ~ l1_orders_2(A_2722)
| v3_struct_0(A_2722) ),
inference(cnfTransformation,[status(thm)],[f_1070]) ).
tff(c_30050,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_30030]) ).
tff(c_30062,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_30050]) ).
tff(c_30063,plain,
m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_6791,c_30062]) ).
tff(c_30072,plain,
! [A_2729,B_2730,C_2731] :
( v4_yellow_0(k2_yellow_2(A_2729,B_2730,C_2731),B_2730)
| ~ m1_relset_1(C_2731,u1_struct_0(A_2729),u1_struct_0(B_2730))
| ~ v1_funct_2(C_2731,u1_struct_0(A_2729),u1_struct_0(B_2730))
| ~ v1_funct_1(C_2731)
| ~ l1_orders_2(B_2730)
| v3_struct_0(B_2730)
| ~ l1_orders_2(A_2729)
| v3_struct_0(A_2729) ),
inference(cnfTransformation,[status(thm)],[f_1493]) ).
tff(c_30092,plain,
( v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_30072]) ).
tff(c_30104,plain,
( v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_30092]) ).
tff(c_30105,plain,
v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_6791,c_30104]) ).
tff(c_322,plain,
! [B_101,A_99] :
( v2_orders_2(B_101)
| ~ v4_yellow_0(B_101,A_99)
| ~ m1_yellow_0(B_101,A_99)
| ~ l1_orders_2(A_99)
| ~ v2_orders_2(A_99) ),
inference(cnfTransformation,[status(thm)],[f_798]) ).
tff(c_30111,plain,
( v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ l1_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_30105,c_322]) ).
tff(c_30120,plain,
v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_14,c_30063,c_30111]) ).
tff(c_30122,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28995,c_30120]) ).
tff(c_30124,plain,
v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_28968]) ).
tff(c_31129,plain,
! [A_2822,B_2823,C_2824] :
( v4_yellow_0(k2_yellow_2(A_2822,B_2823,C_2824),B_2823)
| ~ m1_relset_1(C_2824,u1_struct_0(A_2822),u1_struct_0(B_2823))
| ~ v1_funct_2(C_2824,u1_struct_0(A_2822),u1_struct_0(B_2823))
| ~ v1_funct_1(C_2824)
| ~ l1_orders_2(B_2823)
| v3_struct_0(B_2823)
| ~ l1_orders_2(A_2822)
| v3_struct_0(A_2822) ),
inference(cnfTransformation,[status(thm)],[f_1493]) ).
tff(c_31149,plain,
( v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_31129]) ).
tff(c_31161,plain,
( v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_31149]) ).
tff(c_31162,plain,
v4_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(negUnitSimplification,[status(thm)],[c_6791,c_31161]) ).
tff(c_334,plain,
! [B_108,A_106] :
( v3_orders_2(B_108)
| ~ v4_yellow_0(B_108,A_106)
| ~ m1_yellow_0(B_108,A_106)
| ~ l1_orders_2(A_106)
| ~ v3_orders_2(A_106) ),
inference(cnfTransformation,[status(thm)],[f_838]) ).
tff(c_31165,plain,
( v3_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ l1_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_31162,c_334]) ).
tff(c_31174,plain,
( v3_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_14,c_31165]) ).
tff(c_31181,plain,
~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(splitLeft,[status(thm)],[c_31174]) ).
tff(c_31182,plain,
! [A_2825,B_2826,C_2827] :
( m1_yellow_0(k2_yellow_2(A_2825,B_2826,C_2827),B_2826)
| ~ m1_relset_1(C_2827,u1_struct_0(A_2825),u1_struct_0(B_2826))
| ~ v1_funct_2(C_2827,u1_struct_0(A_2825),u1_struct_0(B_2826))
| ~ v1_funct_1(C_2827)
| ~ l1_orders_2(B_2826)
| v3_struct_0(B_2826)
| ~ l1_orders_2(A_2825)
| v3_struct_0(A_2825) ),
inference(cnfTransformation,[status(thm)],[f_1070]) ).
tff(c_31202,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_31182]) ).
tff(c_31214,plain,
( m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_31202]) ).
tff(c_31216,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6791,c_31181,c_31214]) ).
tff(c_31217,plain,
v3_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(splitRight,[status(thm)],[c_31174]) ).
tff(c_31218,plain,
m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(splitRight,[status(thm)],[c_31174]) ).
tff(c_346,plain,
! [B_115,A_113] :
( v4_orders_2(B_115)
| ~ v4_yellow_0(B_115,A_113)
| ~ m1_yellow_0(B_115,A_113)
| ~ l1_orders_2(A_113)
| ~ v4_orders_2(A_113) ),
inference(cnfTransformation,[status(thm)],[f_878]) ).
tff(c_31171,plain,
( v4_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ l1_orders_2('#skF_1')
| ~ v4_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_31162,c_346]) ).
tff(c_31180,plain,
( v4_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ m1_yellow_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_22,c_14,c_31171]) ).
tff(c_31226,plain,
v4_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_31218,c_31180]) ).
tff(c_210,plain,
! [A_66] :
( v2_lattice3(A_66)
| ~ v3_lattice3(A_66)
| v3_struct_0(A_66)
| ~ l1_orders_2(A_66) ),
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_8635,plain,
( v2_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_210,c_8608]) ).
tff(c_28991,plain,
v2_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_9701,c_28929,c_8635]) ).
tff(c_30632,plain,
! [A_2797,B_2798,C_2799] :
( v1_funct_1(k3_waybel_1(A_2797,B_2798,C_2799))
| ~ m1_relset_1(C_2799,u1_struct_0(A_2797),u1_struct_0(B_2798))
| ~ v1_funct_2(C_2799,u1_struct_0(A_2797),u1_struct_0(B_2798))
| ~ v1_funct_1(C_2799)
| ~ l1_orders_2(B_2798)
| v3_struct_0(B_2798)
| ~ l1_orders_2(A_2797)
| v3_struct_0(A_2797) ),
inference(cnfTransformation,[status(thm)],[f_1740]) ).
tff(c_30662,plain,
( v1_funct_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'))
| ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_30632]) ).
tff(c_30674,plain,
( v1_funct_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'))
| v3_struct_0('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_2002,c_30662]) ).
tff(c_30675,plain,
v1_funct_1(k3_waybel_1('#skF_1','#skF_1','#skF_2')),
inference(negUnitSimplification,[status(thm)],[c_6791,c_30674]) ).
tff(c_45441,plain,
! [A_3349,B_3350] :
( v17_waybel_0(k3_waybel_1(A_3349,A_3349,B_3350),k2_yellow_2(A_3349,A_3349,B_3350),A_3349)
| ~ m2_relset_1(B_3350,u1_struct_0(A_3349),u1_struct_0(A_3349))
| ~ v7_waybel_1(B_3350,A_3349)
| ~ v1_funct_2(B_3350,u1_struct_0(A_3349),u1_struct_0(A_3349))
| ~ v1_funct_1(B_3350)
| ~ l1_orders_2(A_3349)
| ~ v3_lattice3(A_3349)
| ~ v2_lattice3(A_3349)
| ~ v1_lattice3(A_3349)
| ~ v4_orders_2(A_3349)
| ~ v3_orders_2(A_3349)
| ~ v2_orders_2(A_3349) ),
inference(cnfTransformation,[status(thm)],[f_2414]) ).
tff(c_45489,plain,
( v17_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v7_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_45441]) ).
tff(c_45522,plain,
v17_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_8,c_6,c_45489]) ).
tff(c_50604,plain,
! [A_3449,B_3450] :
( ( k1_waybel34(k2_yellow_2(A_3449,A_3449,B_3450),A_3449,k3_waybel_1(A_3449,A_3449,B_3450)) = k2_waybel_1(A_3449,A_3449,B_3450) )
| ~ m2_relset_1(B_3450,u1_struct_0(A_3449),u1_struct_0(A_3449))
| ~ v7_waybel_1(B_3450,A_3449)
| ~ v1_funct_2(B_3450,u1_struct_0(A_3449),u1_struct_0(A_3449))
| ~ v1_funct_1(B_3450)
| ~ l1_orders_2(A_3449)
| ~ v3_lattice3(A_3449)
| ~ v2_lattice3(A_3449)
| ~ v1_lattice3(A_3449)
| ~ v4_orders_2(A_3449)
| ~ v3_orders_2(A_3449)
| ~ v2_orders_2(A_3449) ),
inference(cnfTransformation,[status(thm)],[f_2414]) ).
tff(c_50664,plain,
( ( k1_waybel34(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1',k3_waybel_1('#skF_1','#skF_1','#skF_2')) = k2_waybel_1('#skF_1','#skF_1','#skF_2') )
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v7_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_10,c_50604]) ).
tff(c_50706,plain,
k1_waybel34(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1',k3_waybel_1('#skF_1','#skF_1','#skF_2')) = k2_waybel_1('#skF_1','#skF_1','#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_8,c_6,c_50664]) ).
tff(c_736,plain,
! [A_208,B_209,C_210] :
( v1_funct_2(k3_waybel_1(A_208,B_209,C_210),u1_struct_0(k2_yellow_2(A_208,B_209,C_210)),u1_struct_0(B_209))
| ~ m1_relset_1(C_210,u1_struct_0(A_208),u1_struct_0(B_209))
| ~ v1_funct_2(C_210,u1_struct_0(A_208),u1_struct_0(B_209))
| ~ v1_funct_1(C_210)
| ~ l1_orders_2(B_209)
| v3_struct_0(B_209)
| ~ l1_orders_2(A_208)
| v3_struct_0(A_208) ),
inference(cnfTransformation,[status(thm)],[f_1740]) ).
tff(c_65894,plain,
! [A_3963,B_3964,C_3965] :
( v1_partfun1(k1_waybel34(A_3963,B_3964,C_3965),u1_struct_0(B_3964),u1_struct_0(A_3963))
| ~ m1_relset_1(C_3965,u1_struct_0(A_3963),u1_struct_0(B_3964))
| ~ v17_waybel_0(C_3965,A_3963,B_3964)
| ~ v1_funct_2(C_3965,u1_struct_0(A_3963),u1_struct_0(B_3964))
| ~ v1_funct_1(C_3965)
| ~ l1_orders_2(B_3964)
| ~ v3_lattice3(B_3964)
| ~ v2_lattice3(B_3964)
| ~ v1_lattice3(B_3964)
| ~ v4_orders_2(B_3964)
| ~ v3_orders_2(B_3964)
| ~ v2_orders_2(B_3964)
| ~ l1_orders_2(A_3963)
| ~ v3_lattice3(A_3963)
| ~ v2_lattice3(A_3963)
| ~ v1_lattice3(A_3963)
| ~ v4_orders_2(A_3963)
| ~ v3_orders_2(A_3963)
| ~ v2_orders_2(A_3963) ),
inference(cnfTransformation,[status(thm)],[f_1366]) ).
tff(c_65903,plain,
( v1_partfun1(k2_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')))
| ~ m1_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1'))
| ~ v17_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ v1_funct_2(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1'))
| ~ v1_funct_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1')
| ~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v4_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(superposition,[status(thm),theory(equality)],[c_50706,c_65894]) ).
tff(c_65933,plain,
( v1_partfun1(k2_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0('#skF_1'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')))
| ~ m1_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1'))
| ~ v1_funct_2(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_30124,c_31217,c_31226,c_28928,c_28991,c_28929,c_9701,c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_30675,c_45522,c_65903]) ).
tff(c_140296,plain,
~ v1_funct_2(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')),
inference(splitLeft,[status(thm)],[c_65933]) ).
tff(c_140299,plain,
( ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_736,c_140296]) ).
tff(c_140302,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_10,c_2002,c_140299]) ).
tff(c_140304,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6791,c_140302]) ).
tff(c_140306,plain,
v1_funct_2(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')),
inference(splitRight,[status(thm)],[c_65933]) ).
tff(c_1128,plain,
! [A_262,B_266,C_268] :
( v1_waybel34(k1_waybel34(A_262,B_266,C_268),B_266,A_262)
| ~ v22_waybel_0(C_268,A_262,B_266)
| ~ m2_relset_1(C_268,u1_struct_0(A_262),u1_struct_0(B_266))
| ~ v17_waybel_0(C_268,A_262,B_266)
| ~ v1_funct_2(C_268,u1_struct_0(A_262),u1_struct_0(B_266))
| ~ v1_funct_1(C_268)
| ~ l1_orders_2(B_266)
| ~ v3_lattice3(B_266)
| ~ v2_lattice3(B_266)
| ~ v1_lattice3(B_266)
| ~ v4_orders_2(B_266)
| ~ v3_orders_2(B_266)
| ~ v2_orders_2(B_266)
| ~ l1_orders_2(A_262)
| ~ v3_lattice3(A_262)
| ~ v2_lattice3(A_262)
| ~ v1_lattice3(A_262)
| ~ v4_orders_2(A_262)
| ~ v3_orders_2(A_262)
| ~ v2_orders_2(A_262) ),
inference(cnfTransformation,[status(thm)],[f_2377]) ).
tff(c_140308,plain,
( v1_waybel34(k1_waybel34(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1',k3_waybel_1('#skF_1','#skF_1','#skF_2')),'#skF_1',k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v22_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m2_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1'))
| ~ v17_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ v1_funct_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'))
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1')
| ~ l1_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v1_lattice3(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v4_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v3_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v2_orders_2(k2_yellow_2('#skF_1','#skF_1','#skF_2')) ),
inference(resolution,[status(thm)],[c_140306,c_1128]) ).
tff(c_140477,plain,
( v1_waybel34(k2_waybel_1('#skF_1','#skF_1','#skF_2'),'#skF_1',k2_yellow_2('#skF_1','#skF_1','#skF_2'))
| ~ v22_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m2_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_30124,c_31217,c_31226,c_28928,c_28991,c_28929,c_9701,c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_30675,c_45522,c_50706,c_140308]) ).
tff(c_140478,plain,
( ~ v22_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m2_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')) ),
inference(negUnitSimplification,[status(thm)],[c_2,c_140477]) ).
tff(c_141766,plain,
~ m2_relset_1(k3_waybel_1('#skF_1','#skF_1','#skF_2'),u1_struct_0(k2_yellow_2('#skF_1','#skF_1','#skF_2')),u1_struct_0('#skF_1')),
inference(splitLeft,[status(thm)],[c_140478]) ).
tff(c_141769,plain,
( ~ m1_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| v3_struct_0('#skF_1') ),
inference(resolution,[status(thm)],[c_396,c_141766]) ).
tff(c_141775,plain,
v3_struct_0('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_12,c_10,c_2002,c_141769]) ).
tff(c_141777,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6791,c_141775]) ).
tff(c_141778,plain,
~ v22_waybel_0(k3_waybel_1('#skF_1','#skF_1','#skF_2'),k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1'),
inference(splitRight,[status(thm)],[c_140478]) ).
tff(c_141782,plain,
( ~ v4_waybel_0(k2_yellow_2('#skF_1','#skF_1','#skF_2'),'#skF_1')
| ~ m2_relset_1('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v7_waybel_1('#skF_2','#skF_1')
| ~ v1_funct_2('#skF_2',u1_struct_0('#skF_1'),u1_struct_0('#skF_1'))
| ~ v1_funct_1('#skF_2')
| ~ l1_orders_2('#skF_1')
| ~ v3_lattice3('#skF_1')
| ~ v2_lattice3('#skF_1')
| ~ v1_lattice3('#skF_1')
| ~ v4_orders_2('#skF_1')
| ~ v3_orders_2('#skF_1')
| ~ v2_orders_2('#skF_1') ),
inference(resolution,[status(thm)],[c_1146,c_141778]) ).
tff(c_141786,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_24,c_22,c_20,c_18,c_16,c_14,c_12,c_10,c_8,c_6,c_4,c_141782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : LAT369+1 : TPTP v9.0.0. Released v3.4.0.
% 0.06/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.33 % Computer : n029.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:51:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 121.28/97.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 121.39/97.45
% 121.39/97.45 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------