%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC285+1 : TPTP v9.0.0. Released v2.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 : 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 : Wed Apr 9 09:19:53 PM UTC 2025
% Result : Theorem 84.49s 66.75s
% Output : CNFRefutation 85.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 31
% Syntax : Number of formulae : 620 ( 288 unt; 0 typ; 0 def)
% Number of atoms : 1273 ( 508 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 1238 ( 585 ~; 569 |; 12 &)
% ( 7 <=>; 65 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 60 ( 60 usr; 11 con; 0-2 aty)
% Number of variables : 223 ( 216 !; 7 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ segmentP > rearsegP > neq > memberP > lt > leq > gt > geq > frontsegP > totalorderedP > totalorderP > strictorderedP > strictorderP > ssList > ssItem > singletonP > equalelemsP > duplicatefreeP > cyclefreeP > cons > app > #nlpp > tl > hd > nil > #skF_36 > #skF_25 > #skF_5 > #skF_52 > #skF_44 > #skF_21 > #skF_16 > #skF_6 > #skF_49 > #skF_18 > #skF_24 > #skF_35 > #skF_19 > #skF_31 > #skF_55 > #skF_22 > #skF_37 > #skF_54 > #skF_40 > #skF_48 > #skF_3 > #skF_34 > #skF_29 > #skF_15 > #skF_32 > #skF_53 > #skF_51 > #skF_28 > #skF_10 > #skF_41 > #skF_2 > #skF_38 > #skF_43 > #skF_1 > #skF_8 > #skF_39 > #skF_23 > #skF_33 > #skF_26 > #skF_50 > #skF_13 > #skF_17 > #skF_11 > #skF_14 > #skF_27 > #skF_12 > #skF_7 > #skF_46 > #skF_42 > #skF_45 > #skF_9 > #skF_30 > #skF_4 > #skF_20 > #skF_47
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_36',type,
'#skF_36': $i > $i ).
tff(segmentP,type,
segmentP: ( $i * $i ) > $o ).
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff(totalorderedP,type,
totalorderedP: $i > $o ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(equalelemsP,type,
equalelemsP: $i > $o ).
tff('#skF_52',type,
'#skF_52': $i ).
tff('#skF_44',type,
'#skF_44': $i > $i ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff('#skF_49',type,
'#skF_49': $i ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff('#skF_35',type,
'#skF_35': $i > $i ).
tff(singletonP,type,
singletonP: $i > $o ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff('#skF_31',type,
'#skF_31': $i > $i ).
tff('#skF_55',type,
'#skF_55': $i ).
tff('#skF_22',type,
'#skF_22': $i > $i ).
tff(frontsegP,type,
frontsegP: ( $i * $i ) > $o ).
tff('#skF_37',type,
'#skF_37': $i > $i ).
tff(totalorderP,type,
totalorderP: $i > $o ).
tff(ssItem,type,
ssItem: $i > $o ).
tff('#skF_54',type,
'#skF_54': $i ).
tff('#skF_40',type,
'#skF_40': $i > $i ).
tff('#skF_48',type,
'#skF_48': $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff('#skF_34',type,
'#skF_34': $i > $i ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff('#skF_15',type,
'#skF_15': $i > $i ).
tff('#skF_32',type,
'#skF_32': $i > $i ).
tff('#skF_53',type,
'#skF_53': $i ).
tff('#skF_51',type,
'#skF_51': $i ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff('#skF_41',type,
'#skF_41': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_38',type,
'#skF_38': $i > $i ).
tff('#skF_43',type,
'#skF_43': $i > $i ).
tff(hd,type,
hd: $i > $i ).
tff(app,type,
app: ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(duplicatefreeP,type,
duplicatefreeP: $i > $o ).
tff(gt,type,
gt: ( $i * $i ) > $o ).
tff('#skF_39',type,
'#skF_39': $i > $i ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff(rearsegP,type,
rearsegP: ( $i * $i ) > $o ).
tff('#skF_33',type,
'#skF_33': $i > $i ).
tff(memberP,type,
memberP: ( $i * $i ) > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff('#skF_50',type,
'#skF_50': $i ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(ssList,type,
ssList: $i > $o ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(strictorderP,type,
strictorderP: $i > $o ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff(geq,type,
geq: ( $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(leq,type,
leq: ( $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(lt,type,
lt: ( $i * $i ) > $o ).
tff(tl,type,
tl: $i > $i ).
tff(neq,type,
neq: ( $i * $i ) > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff('#skF_46',type,
'#skF_46': $i > $i ).
tff(nil,type,
nil: $i ).
tff('#skF_42',type,
'#skF_42': $i > $i ).
tff('#skF_45',type,
'#skF_45': $i > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff(strictorderedP,type,
strictorderedP: $i > $o ).
tff('#skF_30',type,
'#skF_30': $i > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff(cyclefreeP,type,
cyclefreeP: $i > $o ).
tff('#skF_47',type,
'#skF_47': $i > $i ).
tff(f_319,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax17) ).
tff(f_1027,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( V != X )
| ( U != W )
| ~ segmentP(X,W)
| ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssList(Z)
=> ! [X1] :
( ssList(X1)
=> ( ( app(app(Z,cons(Y,nil)),X1) != U )
| ! [X2] :
( ssItem(X2)
=> ( ( ~ memberP(Z,X2)
| leq(X2,Y) )
& ( ~ memberP(X1,X2)
| leq(Y,X2) ) ) ) ) ) ) )
| ( ~ singletonP(W)
& neq(X,nil) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
tff(f_318,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax16) ).
tff(f_859,axiom,
! [U] :
( ssList(U)
=> ( app(U,nil) = U ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax84) ).
tff(f_108,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( frontsegP(U,V)
<=> ? [W] :
( ssList(W)
& ( app(V,W) = U ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax5) ).
tff(f_834,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( cons(V,U) = app(cons(V,nil),U) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax81) ).
tff(f_135,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ssList(W)
& ? [X] :
( ssList(X)
& ( app(app(W,V),X) = U ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax7) ).
tff(f_844,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( app(app(U,V),W) = app(U,app(V,W)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax82) ).
tff(f_827,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( app(V,W) = app(V,U) )
=> ( W = U ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax80) ).
tff(f_399,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ssList(app(U,V)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax26) ).
tff(f_769,axiom,
! [U] :
( ssList(U)
=> ( ( nil != U )
=> ? [V] :
( ssItem(V)
& ( hd(U) = V ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax75) ).
tff(f_779,axiom,
! [U] :
( ssList(U)
=> ( ( nil != U )
=> ? [V] :
( ssList(V)
& ( tl(U) = V ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax76) ).
tff(f_517,axiom,
! [U] :
( ssItem(U)
=> ~ memberP(nil,U) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax38) ).
tff(f_855,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( nil = app(U,V) )
<=> ( ( nil = V )
& ( nil = U ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax83) ).
tff(f_692,axiom,
! [U] :
( ssList(U)
=> ( segmentP(nil,U)
<=> ( nil = U ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax58) ).
tff(f_311,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> ( U != V ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax15) ).
tff(f_519,axiom,
~ singletonP(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax39) ).
tff(f_385,axiom,
! [U] :
( ssList(U)
=> ( ( nil != U )
=> ssList(tl(U)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax24) ).
tff(f_803,axiom,
! [U] :
( ssList(U)
=> ( ( nil != U )
=> ( cons(hd(U),tl(U)) = U ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax78) ).
tff(f_413,axiom,
! [U] :
( ssList(U)
=> ( app(nil,U) = U ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax28) ).
tff(f_392,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( tl(cons(V,U)) = U ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax25) ).
tff(f_96,axiom,
! [U] :
( ssList(U)
=> ( singletonP(U)
<=> ? [V] :
( ssItem(V)
& ( cons(V,nil) = U ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax4) ).
tff(f_869,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( nil != U )
=> ( hd(app(U,V)) = hd(U) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax85) ).
tff(f_544,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( frontsegP(U,V)
& frontsegP(V,U) )
=> ( U = V ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax41) ).
tff(f_364,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ( nil != cons(V,U) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax21) ).
tff(f_120,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( rearsegP(U,V)
<=> ? [W] :
( ssList(W)
& ( app(W,V) = U ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax6) ).
tff(f_371,axiom,
! [U] :
( ssList(U)
=> ( ( nil != U )
=> ssItem(hd(U)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax22) ).
tff(f_758,axiom,
! [U] :
( ssItem(U)
=> equalelemsP(cons(U,nil)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax73) ).
tff(f_612,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( rearsegP(U,V)
& rearsegP(V,U) )
=> ( U = V ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax48) ).
tff(f_815,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( app(W,V) = app(U,V) )
=> ( W = U ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax79) ).
tff(f_696,axiom,
! [U] :
( ssItem(U)
=> cyclefreeP(cons(U,nil)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax59) ).
tff(c_168,plain,
ssList(nil),
inference(cnfTransformation,[status(thm)],[f_319]) ).
tff(c_394,plain,
ssItem('#skF_52'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_166,plain,
! [V_861,U_859] :
( ssList(cons(V_861,U_859))
| ~ ssItem(V_861)
| ~ ssList(U_859) ),
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_386,plain,
ssItem('#skF_55'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_390,plain,
ssList('#skF_54'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_404,plain,
ssList('#skF_50'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_18490,plain,
! [U_2107] :
( ( app(U_2107,nil) = U_2107 )
| ~ ssList(U_2107) ),
inference(cnfTransformation,[status(thm)],[f_859]) ).
tff(c_18509,plain,
app('#skF_50',nil) = '#skF_50',
inference(resolution,[status(thm)],[c_404,c_18490]) ).
tff(c_222146,plain,
! [V_5168,W_5169] :
( frontsegP(app(V_5168,W_5169),V_5168)
| ~ ssList(W_5169)
| ~ ssList(V_5168)
| ~ ssList(app(V_5168,W_5169)) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_222292,plain,
( frontsegP('#skF_50','#skF_50')
| ~ ssList(nil)
| ~ ssList('#skF_50')
| ~ ssList(app('#skF_50',nil)) ),
inference(superposition,[status(thm),theory(equality)],[c_18509,c_222146]) ).
tff(c_222396,plain,
frontsegP('#skF_50','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_18509,c_404,c_168,c_222292]) ).
tff(c_346,plain,
! [V_1069,U_1067] :
( ( app(cons(V_1069,nil),U_1067) = cons(V_1069,U_1067) )
| ~ ssItem(V_1069)
| ~ ssList(U_1067) ),
inference(cnfTransformation,[status(thm)],[f_834]) ).
tff(c_398,plain,
'#skF_48' = '#skF_50',
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_388,plain,
app(app('#skF_53',cons('#skF_52',nil)),'#skF_54') = '#skF_48',
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_421,plain,
app(app('#skF_53',cons('#skF_52',nil)),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_398,c_388]) ).
tff(c_392,plain,
ssList('#skF_53'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_236741,plain,
! [W_5379,V_5380,X_5381] :
( segmentP(app(app(W_5379,V_5380),X_5381),V_5380)
| ~ ssList(X_5381)
| ~ ssList(W_5379)
| ~ ssList(V_5380)
| ~ ssList(app(app(W_5379,V_5380),X_5381)) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_237008,plain,
( segmentP('#skF_50',cons('#skF_52',nil))
| ~ ssList('#skF_54')
| ~ ssList('#skF_53')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList(app(app('#skF_53',cons('#skF_52',nil)),'#skF_54')) ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_236741]) ).
tff(c_237170,plain,
( segmentP('#skF_50',cons('#skF_52',nil))
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_421,c_392,c_390,c_237008]) ).
tff(c_238034,plain,
~ ssList(cons('#skF_52',nil)),
inference(splitLeft,[status(thm)],[c_237170]) ).
tff(c_238037,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_238034]) ).
tff(c_238041,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_238037]) ).
tff(c_238043,plain,
ssList(cons('#skF_52',nil)),
inference(splitRight,[status(thm)],[c_237170]) ).
tff(c_231026,plain,
! [U_5306,V_5307,W_5308] :
( ( app(app(U_5306,V_5307),W_5308) = app(U_5306,app(V_5307,W_5308)) )
| ~ ssList(W_5308)
| ~ ssList(V_5307)
| ~ ssList(U_5306) ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_231093,plain,
( ( app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_231026,c_421]) ).
tff(c_231290,plain,
( ( app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_390,c_231093]) ).
tff(c_242243,plain,
app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_238043,c_231290]) ).
tff(c_242323,plain,
( ( app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_346,c_242243]) ).
tff(c_242372,plain,
app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_242323]) ).
tff(c_26,plain,
! [V_40,W_43] :
( frontsegP(app(V_40,W_43),V_40)
| ~ ssList(W_43)
| ~ ssList(V_40)
| ~ ssList(app(V_40,W_43)) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_242514,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54'))
| ~ ssList('#skF_53')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_54'))) ),
inference(superposition,[status(thm),theory(equality)],[c_242372,c_26]) ).
tff(c_242590,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_242372,c_392,c_242514]) ).
tff(c_242903,plain,
~ ssList(cons('#skF_52','#skF_54')),
inference(splitLeft,[status(thm)],[c_242590]) ).
tff(c_242906,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(resolution,[status(thm)],[c_166,c_242903]) ).
tff(c_242910,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_242906]) ).
tff(c_242912,plain,
ssList(cons('#skF_52','#skF_54')),
inference(splitRight,[status(thm)],[c_242590]) ).
tff(c_18506,plain,
app('#skF_53',nil) = '#skF_53',
inference(resolution,[status(thm)],[c_392,c_18490]) ).
tff(c_226101,plain,
! [W_5209,U_5210,V_5211] :
( ( W_5209 = U_5210 )
| ( app(V_5211,W_5209) != app(V_5211,U_5210) )
| ~ ssList(W_5209)
| ~ ssList(V_5211)
| ~ ssList(U_5210) ),
inference(cnfTransformation,[status(thm)],[f_827]) ).
tff(c_226311,plain,
! [U_5210] :
( ( nil = U_5210 )
| ( app('#skF_53',U_5210) != '#skF_53' )
| ~ ssList(nil)
| ~ ssList('#skF_53')
| ~ ssList(U_5210) ),
inference(superposition,[status(thm),theory(equality)],[c_18506,c_226101]) ).
tff(c_226511,plain,
! [U_5210] :
( ( nil = U_5210 )
| ( app('#skF_53',U_5210) != '#skF_53' )
| ~ ssList(U_5210) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_168,c_226311]) ).
tff(c_242955,plain,
( ( cons('#skF_52','#skF_54') = nil )
| ( app('#skF_53',cons('#skF_52','#skF_54')) != '#skF_53' ) ),
inference(resolution,[status(thm)],[c_242912,c_226511]) ).
tff(c_243036,plain,
( ( cons('#skF_52','#skF_54') = nil )
| ( '#skF_53' != '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_242372,c_242955]) ).
tff(c_243294,plain,
'#skF_53' != '#skF_50',
inference(splitLeft,[status(thm)],[c_243036]) ).
tff(c_192,plain,
! [U_896,V_898] :
( ssList(app(U_896,V_898))
| ~ ssList(V_898)
| ~ ssList(U_896) ),
inference(cnfTransformation,[status(thm)],[f_399]) ).
tff(c_402,plain,
ssList('#skF_51'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_8644,plain,
! [U_1759] :
( ( hd(U_1759) = '#skF_46'(U_1759) )
| ( nil = U_1759 )
| ~ ssList(U_1759) ),
inference(cnfTransformation,[status(thm)],[f_769]) ).
tff(c_8761,plain,
( ( hd('#skF_51') = '#skF_46'('#skF_51') )
| ( nil = '#skF_51' ) ),
inference(resolution,[status(thm)],[c_402,c_8644]) ).
tff(c_10242,plain,
nil = '#skF_51',
inference(splitLeft,[status(thm)],[c_8761]) ).
tff(c_10114,plain,
! [U_1782] :
( ( tl(U_1782) = '#skF_47'(U_1782) )
| ( nil = U_1782 )
| ~ ssList(U_1782) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_10230,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_10114]) ).
tff(c_10447,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( '#skF_51' = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10242,c_10230]) ).
tff(c_10448,plain,
'#skF_51' = '#skF_50',
inference(splitLeft,[status(thm)],[c_10447]) ).
tff(c_872,plain,
! [U_1438] :
( ( tl(U_1438) = '#skF_47'(U_1438) )
| ( nil = U_1438 )
| ~ ssList(U_1438) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_989,plain,
( ( tl('#skF_51') = '#skF_47'('#skF_51') )
| ( nil = '#skF_51' ) ),
inference(resolution,[status(thm)],[c_402,c_872]) ).
tff(c_4928,plain,
nil = '#skF_51',
inference(splitLeft,[status(thm)],[c_989]) ).
tff(c_988,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_872]) ).
tff(c_4980,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( '#skF_51' = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4928,c_988]) ).
tff(c_4981,plain,
'#skF_51' = '#skF_50',
inference(splitLeft,[status(thm)],[c_4980]) ).
tff(c_416,plain,
( memberP('#skF_53','#skF_55')
| memberP('#skF_54','#skF_55') ),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_446,plain,
memberP('#skF_54','#skF_55'),
inference(splitLeft,[status(thm)],[c_416]) ).
tff(c_985,plain,
( ( tl('#skF_54') = '#skF_47'('#skF_54') )
| ( nil = '#skF_54' ) ),
inference(resolution,[status(thm)],[c_390,c_872]) ).
tff(c_4079,plain,
nil = '#skF_54',
inference(splitLeft,[status(thm)],[c_985]) ).
tff(c_228,plain,
! [U_948] :
( ~ memberP(nil,U_948)
| ~ ssItem(U_948) ),
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_4770,plain,
! [U_1575] :
( ~ memberP('#skF_54',U_1575)
| ~ ssItem(U_1575) ),
inference(demodulation,[status(thm),theory(equality)],[c_4079,c_228]) ).
tff(c_4773,plain,
~ ssItem('#skF_55'),
inference(resolution,[status(thm)],[c_446,c_4770]) ).
tff(c_4777,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_4773]) ).
tff(c_4779,plain,
nil != '#skF_54',
inference(splitRight,[status(thm)],[c_985]) ).
tff(c_4929,plain,
'#skF_54' != '#skF_51',
inference(demodulation,[status(thm),theory(equality)],[c_4928,c_4779]) ).
tff(c_5113,plain,
'#skF_54' != '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_4981,c_4929]) ).
tff(c_4942,plain,
app(app('#skF_53',cons('#skF_52','#skF_51')),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_4928,c_421]) ).
tff(c_5474,plain,
app(app('#skF_53',cons('#skF_52','#skF_50')),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_4981,c_4942]) ).
tff(c_5098,plain,
nil = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_4981,c_4928]) ).
tff(c_354,plain,
! [V_1079,U_1077] :
( ( nil = V_1079 )
| ( app(U_1077,V_1079) != nil )
| ~ ssList(V_1079)
| ~ ssList(U_1077) ),
inference(cnfTransformation,[status(thm)],[f_855]) ).
tff(c_6582,plain,
! [V_1642,U_1643] :
( ( V_1642 = '#skF_50' )
| ( app(U_1643,V_1642) != '#skF_50' )
| ~ ssList(V_1642)
| ~ ssList(U_1643) ),
inference(demodulation,[status(thm),theory(equality)],[c_5098,c_5098,c_354]) ).
tff(c_6584,plain,
( ( '#skF_54' = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(superposition,[status(thm),theory(equality)],[c_5474,c_6582]) ).
tff(c_6597,plain,
( ( '#skF_54' = '#skF_50' )
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_6584]) ).
tff(c_6598,plain,
~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))),
inference(negUnitSimplification,[status(thm)],[c_5113,c_6597]) ).
tff(c_6615,plain,
( ~ ssList(cons('#skF_52','#skF_50'))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_6598]) ).
tff(c_6618,plain,
~ ssList(cons('#skF_52','#skF_50')),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_6615]) ).
tff(c_6621,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_166,c_6618]) ).
tff(c_6625,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_404,c_394,c_6621]) ).
tff(c_6627,plain,
'#skF_51' != '#skF_50',
inference(splitRight,[status(thm)],[c_4980]) ).
tff(c_396,plain,
segmentP('#skF_51','#skF_50'),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_278,plain,
! [U_1031] :
( ( nil = U_1031 )
| ~ segmentP(nil,U_1031)
| ~ ssList(U_1031) ),
inference(cnfTransformation,[status(thm)],[f_692]) ).
tff(c_7293,plain,
! [U_1665] :
( ( U_1665 = '#skF_51' )
| ~ segmentP('#skF_51',U_1665)
| ~ ssList(U_1665) ),
inference(demodulation,[status(thm),theory(equality)],[c_4928,c_4928,c_278]) ).
tff(c_7304,plain,
( ( '#skF_51' = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_396,c_7293]) ).
tff(c_7315,plain,
'#skF_51' = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_404,c_7304]) ).
tff(c_7317,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6627,c_7315]) ).
tff(c_7319,plain,
nil != '#skF_51',
inference(splitRight,[status(thm)],[c_989]) ).
tff(c_8197,plain,
! [U_1700,V_1701] :
( neq(U_1700,V_1701)
| ( V_1701 = U_1700 )
| ~ ssList(V_1701)
| ~ ssList(U_1700) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_384,plain,
( ~ neq('#skF_51',nil)
| singletonP('#skF_50') ),
inference(cnfTransformation,[status(thm)],[f_1027]) ).
tff(c_438,plain,
~ neq('#skF_51',nil),
inference(splitLeft,[status(thm)],[c_384]) ).
tff(c_8204,plain,
( ( nil = '#skF_51' )
| ~ ssList(nil)
| ~ ssList('#skF_51') ),
inference(resolution,[status(thm)],[c_8197,c_438]) ).
tff(c_8213,plain,
nil = '#skF_51',
inference(demodulation,[status(thm),theory(equality)],[c_402,c_168,c_8204]) ).
tff(c_8215,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7319,c_8213]) ).
tff(c_8216,plain,
memberP('#skF_53','#skF_55'),
inference(splitRight,[status(thm)],[c_416]) ).
tff(c_8756,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_53') )
| ( nil = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_392,c_8644]) ).
tff(c_8762,plain,
nil = '#skF_53',
inference(splitLeft,[status(thm)],[c_8756]) ).
tff(c_10104,plain,
! [U_1781] :
( ~ memberP('#skF_53',U_1781)
| ~ ssItem(U_1781) ),
inference(demodulation,[status(thm),theory(equality)],[c_8762,c_228]) ).
tff(c_10107,plain,
~ ssItem('#skF_55'),
inference(resolution,[status(thm)],[c_8216,c_10104]) ).
tff(c_10111,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_10107]) ).
tff(c_10113,plain,
nil != '#skF_53',
inference(splitRight,[status(thm)],[c_8756]) ).
tff(c_10243,plain,
'#skF_53' != '#skF_51',
inference(demodulation,[status(thm),theory(equality)],[c_10242,c_10113]) ).
tff(c_10455,plain,
'#skF_53' != '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_10448,c_10243]) ).
tff(c_10464,plain,
nil = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_10448,c_10242]) ).
tff(c_8757,plain,
( ( hd('#skF_54') = '#skF_46'('#skF_54') )
| ( nil = '#skF_54' ) ),
inference(resolution,[status(thm)],[c_390,c_8644]) ).
tff(c_10657,plain,
( ( hd('#skF_54') = '#skF_46'('#skF_54') )
| ( '#skF_54' = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10464,c_8757]) ).
tff(c_10658,plain,
'#skF_54' = '#skF_50',
inference(splitLeft,[status(thm)],[c_10657]) ).
tff(c_10270,plain,
app(app('#skF_53',cons('#skF_52','#skF_51')),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_10242,c_421]) ).
tff(c_10693,plain,
app(app('#skF_53',cons('#skF_52','#skF_50')),'#skF_50') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_10658,c_10448,c_10270]) ).
tff(c_352,plain,
! [U_1077,V_1079] :
( ( nil = U_1077 )
| ( app(U_1077,V_1079) != nil )
| ~ ssList(V_1079)
| ~ ssList(U_1077) ),
inference(cnfTransformation,[status(thm)],[f_855]) ).
tff(c_12303,plain,
! [U_1868,V_1869] :
( ( U_1868 = '#skF_50' )
| ( app(U_1868,V_1869) != '#skF_50' )
| ~ ssList(V_1869)
| ~ ssList(U_1868) ),
inference(demodulation,[status(thm),theory(equality)],[c_10464,c_10464,c_352]) ).
tff(c_12313,plain,
( ( app('#skF_53',cons('#skF_52','#skF_50')) = '#skF_50' )
| ~ ssList('#skF_50')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(superposition,[status(thm),theory(equality)],[c_10693,c_12303]) ).
tff(c_12332,plain,
( ( app('#skF_53',cons('#skF_52','#skF_50')) = '#skF_50' )
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_12313]) ).
tff(c_12551,plain,
~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))),
inference(splitLeft,[status(thm)],[c_12332]) ).
tff(c_12554,plain,
( ~ ssList(cons('#skF_52','#skF_50'))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_12551]) ).
tff(c_12557,plain,
~ ssList(cons('#skF_52','#skF_50')),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_12554]) ).
tff(c_12560,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_166,c_12557]) ).
tff(c_12564,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_404,c_394,c_12560]) ).
tff(c_12565,plain,
app('#skF_53',cons('#skF_52','#skF_50')) = '#skF_50',
inference(splitRight,[status(thm)],[c_12332]) ).
tff(c_12302,plain,
! [U_1077,V_1079] :
( ( U_1077 = '#skF_50' )
| ( app(U_1077,V_1079) != '#skF_50' )
| ~ ssList(V_1079)
| ~ ssList(U_1077) ),
inference(demodulation,[status(thm),theory(equality)],[c_10464,c_10464,c_352]) ).
tff(c_12616,plain,
( ( '#skF_53' = '#skF_50' )
| ~ ssList(cons('#skF_52','#skF_50'))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_12565,c_12302]) ).
tff(c_12627,plain,
( ( '#skF_53' = '#skF_50' )
| ~ ssList(cons('#skF_52','#skF_50')) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_12616]) ).
tff(c_12628,plain,
~ ssList(cons('#skF_52','#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_10455,c_12627]) ).
tff(c_12634,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_166,c_12628]) ).
tff(c_12638,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_404,c_394,c_12634]) ).
tff(c_12640,plain,
'#skF_54' != '#skF_50',
inference(splitRight,[status(thm)],[c_10657]) ).
tff(c_12791,plain,
app(app('#skF_53',cons('#skF_52','#skF_50')),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_10448,c_10270]) ).
tff(c_14532,plain,
! [V_1955,U_1956] :
( ( V_1955 = '#skF_50' )
| ( app(U_1956,V_1955) != '#skF_50' )
| ~ ssList(V_1955)
| ~ ssList(U_1956) ),
inference(demodulation,[status(thm),theory(equality)],[c_10464,c_10464,c_354]) ).
tff(c_14538,plain,
( ( '#skF_54' = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(superposition,[status(thm),theory(equality)],[c_12791,c_14532]) ).
tff(c_14556,plain,
( ( '#skF_54' = '#skF_50' )
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_14538]) ).
tff(c_14557,plain,
~ ssList(app('#skF_53',cons('#skF_52','#skF_50'))),
inference(negUnitSimplification,[status(thm)],[c_12640,c_14556]) ).
tff(c_14574,plain,
( ~ ssList(cons('#skF_52','#skF_50'))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_14557]) ).
tff(c_14577,plain,
~ ssList(cons('#skF_52','#skF_50')),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_14574]) ).
tff(c_14580,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_166,c_14577]) ).
tff(c_14584,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_404,c_394,c_14580]) ).
tff(c_14586,plain,
'#skF_51' != '#skF_50',
inference(splitRight,[status(thm)],[c_10447]) ).
tff(c_15025,plain,
! [U_1980] :
( ( U_1980 = '#skF_51' )
| ~ segmentP('#skF_51',U_1980)
| ~ ssList(U_1980) ),
inference(demodulation,[status(thm),theory(equality)],[c_10242,c_10242,c_278]) ).
tff(c_15036,plain,
( ( '#skF_51' = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_396,c_15025]) ).
tff(c_15047,plain,
'#skF_51' = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_404,c_15036]) ).
tff(c_15049,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14586,c_15047]) ).
tff(c_15051,plain,
nil != '#skF_51',
inference(splitRight,[status(thm)],[c_8761]) ).
tff(c_18458,plain,
! [U_2097,V_2098] :
( neq(U_2097,V_2098)
| ( V_2098 = U_2097 )
| ~ ssList(V_2098)
| ~ ssList(U_2097) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_18465,plain,
( ( nil = '#skF_51' )
| ~ ssList(nil)
| ~ ssList('#skF_51') ),
inference(resolution,[status(thm)],[c_18458,c_438]) ).
tff(c_18474,plain,
nil = '#skF_51',
inference(demodulation,[status(thm),theory(equality)],[c_402,c_168,c_18465]) ).
tff(c_18476,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15051,c_18474]) ).
tff(c_18477,plain,
singletonP('#skF_50'),
inference(splitRight,[status(thm)],[c_384]) ).
tff(c_103604,plain,
! [U_3378] :
( ( tl(U_3378) = '#skF_47'(U_3378) )
| ( nil = U_3378 )
| ~ ssList(U_3378) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_103724,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_103604]) ).
tff(c_103890,plain,
nil = '#skF_50',
inference(splitLeft,[status(thm)],[c_103724]) ).
tff(c_230,plain,
~ singletonP(nil),
inference(cnfTransformation,[status(thm)],[f_519]) ).
tff(c_103933,plain,
~ singletonP('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_103890,c_230]) ).
tff(c_103940,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_103933]) ).
tff(c_103942,plain,
nil != '#skF_50',
inference(splitRight,[status(thm)],[c_103724]) ).
tff(c_103941,plain,
tl('#skF_50') = '#skF_47'('#skF_50'),
inference(splitRight,[status(thm)],[c_103724]) ).
tff(c_188,plain,
! [U_892] :
( ssList(tl(U_892))
| ( nil = U_892 )
| ~ ssList(U_892) ),
inference(cnfTransformation,[status(thm)],[f_385]) ).
tff(c_103947,plain,
( ssList('#skF_47'('#skF_50'))
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_103941,c_188]) ).
tff(c_103951,plain,
( ssList('#skF_47'('#skF_50'))
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_103947]) ).
tff(c_103952,plain,
ssList('#skF_47'('#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_103942,c_103951]) ).
tff(c_330,plain,
! [U_1045] :
( ( hd(U_1045) = '#skF_46'(U_1045) )
| ( nil = U_1045 )
| ~ ssList(U_1045) ),
inference(cnfTransformation,[status(thm)],[f_769]) ).
tff(c_103971,plain,
( ( hd('#skF_47'('#skF_50')) = '#skF_46'('#skF_47'('#skF_50')) )
| ( '#skF_47'('#skF_50') = nil ) ),
inference(resolution,[status(thm)],[c_103952,c_330]) ).
tff(c_157767,plain,
'#skF_47'('#skF_50') = nil,
inference(splitLeft,[status(thm)],[c_103971]) ).
tff(c_18861,plain,
! [U_2158] :
( ( hd(U_2158) = '#skF_46'(U_2158) )
| ( nil = U_2158 )
| ~ ssList(U_2158) ),
inference(cnfTransformation,[status(thm)],[f_769]) ).
tff(c_18977,plain,
( ( hd('#skF_50') = '#skF_46'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_18861]) ).
tff(c_103976,plain,
hd('#skF_50') = '#skF_46'('#skF_50'),
inference(negUnitSimplification,[status(thm)],[c_103942,c_18977]) ).
tff(c_104473,plain,
! [U_3407] :
( ( cons(hd(U_3407),tl(U_3407)) = U_3407 )
| ( nil = U_3407 )
| ~ ssList(U_3407) ),
inference(cnfTransformation,[status(thm)],[f_803]) ).
tff(c_104504,plain,
( ( cons('#skF_46'('#skF_50'),tl('#skF_50')) = '#skF_50' )
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_103976,c_104473]) ).
tff(c_104531,plain,
( ( cons('#skF_46'('#skF_50'),'#skF_47'('#skF_50')) = '#skF_50' )
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_103941,c_104504]) ).
tff(c_104532,plain,
cons('#skF_46'('#skF_50'),'#skF_47'('#skF_50')) = '#skF_50',
inference(negUnitSimplification,[status(thm)],[c_103942,c_104531]) ).
tff(c_157770,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_157767,c_104532]) ).
tff(c_18973,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_53') )
| ( nil = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_392,c_18861]) ).
tff(c_18979,plain,
nil = '#skF_53',
inference(splitLeft,[status(thm)],[c_18973]) ).
tff(c_18974,plain,
( ( hd('#skF_54') = '#skF_46'('#skF_54') )
| ( nil = '#skF_54' ) ),
inference(resolution,[status(thm)],[c_390,c_18861]) ).
tff(c_19185,plain,
( ( hd('#skF_54') = '#skF_46'('#skF_54') )
| ( '#skF_54' = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_18974]) ).
tff(c_19186,plain,
'#skF_54' = '#skF_53',
inference(splitLeft,[status(thm)],[c_19185]) ).
tff(c_18484,plain,
memberP('#skF_54','#skF_55'),
inference(splitLeft,[status(thm)],[c_416]) ).
tff(c_19187,plain,
memberP('#skF_53','#skF_55'),
inference(demodulation,[status(thm),theory(equality)],[c_19186,c_18484]) ).
tff(c_19447,plain,
! [U_2168] :
( ~ memberP('#skF_53',U_2168)
| ~ ssItem(U_2168) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_228]) ).
tff(c_19450,plain,
~ ssItem('#skF_55'),
inference(resolution,[status(thm)],[c_19187,c_19447]) ).
tff(c_19454,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_19450]) ).
tff(c_19456,plain,
'#skF_54' != '#skF_53',
inference(splitRight,[status(thm)],[c_19185]) ).
tff(c_19457,plain,
( ( hd('#skF_50') = '#skF_46'('#skF_50') )
| ( '#skF_53' = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_18977]) ).
tff(c_19458,plain,
'#skF_53' = '#skF_50',
inference(splitLeft,[status(thm)],[c_19457]) ).
tff(c_19018,plain,
~ singletonP('#skF_53'),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_230]) ).
tff(c_19460,plain,
~ singletonP('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_19458,c_19018]) ).
tff(c_19473,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_19460]) ).
tff(c_19475,plain,
'#skF_53' != '#skF_50',
inference(splitRight,[status(thm)],[c_19457]) ).
tff(c_334,plain,
! [U_1047] :
( ( tl(U_1047) = '#skF_47'(U_1047) )
| ( nil = U_1047 )
| ~ ssList(U_1047) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_19029,plain,
! [U_2159] :
( ( tl(U_2159) = '#skF_47'(U_2159) )
| ( U_2159 = '#skF_53' )
| ~ ssList(U_2159) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_334]) ).
tff(c_19129,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( '#skF_53' = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_19029]) ).
tff(c_19534,plain,
tl('#skF_50') = '#skF_47'('#skF_50'),
inference(negUnitSimplification,[status(thm)],[c_19475,c_19129]) ).
tff(c_20129,plain,
! [U_2197] :
( ssList(tl(U_2197))
| ( U_2197 = '#skF_53' )
| ~ ssList(U_2197) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_188]) ).
tff(c_20150,plain,
( ssList('#skF_47'('#skF_50'))
| ( '#skF_53' = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_19534,c_20129]) ).
tff(c_20163,plain,
( ssList('#skF_47'('#skF_50'))
| ( '#skF_53' = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_20150]) ).
tff(c_20164,plain,
ssList('#skF_47'('#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_19475,c_20163]) ).
tff(c_19028,plain,
! [U_1047] :
( ( tl(U_1047) = '#skF_47'(U_1047) )
| ( U_1047 = '#skF_53' )
| ~ ssList(U_1047) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_334]) ).
tff(c_20208,plain,
( ( tl('#skF_47'('#skF_50')) = '#skF_47'('#skF_47'('#skF_50')) )
| ( '#skF_47'('#skF_50') = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_20164,c_19028]) ).
tff(c_22140,plain,
'#skF_47'('#skF_50') = '#skF_53',
inference(splitLeft,[status(thm)],[c_20208]) ).
tff(c_22145,plain,
tl('#skF_50') = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_22140,c_19534]) ).
tff(c_18989,plain,
app(app('#skF_53',cons('#skF_52','#skF_53')),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_421]) ).
tff(c_94630,plain,
! [W_3205,V_3206,X_3207] :
( segmentP(app(app(W_3205,V_3206),X_3207),V_3206)
| ~ ssList(X_3207)
| ~ ssList(W_3205)
| ~ ssList(V_3206)
| ~ ssList(app(app(W_3205,V_3206),X_3207)) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_94945,plain,
( segmentP('#skF_50',cons('#skF_52','#skF_53'))
| ~ ssList('#skF_54')
| ~ ssList('#skF_53')
| ~ ssList(cons('#skF_52','#skF_53'))
| ~ ssList(app(app('#skF_53',cons('#skF_52','#skF_53')),'#skF_54')) ),
inference(superposition,[status(thm),theory(equality)],[c_18989,c_94630]) ).
tff(c_95129,plain,
( segmentP('#skF_50',cons('#skF_52','#skF_53'))
| ~ ssList(cons('#skF_52','#skF_53')) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_18989,c_392,c_390,c_94945]) ).
tff(c_95194,plain,
~ ssList(cons('#skF_52','#skF_53')),
inference(splitLeft,[status(thm)],[c_95129]) ).
tff(c_95300,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_166,c_95194]) ).
tff(c_95304,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_392,c_394,c_95300]) ).
tff(c_95306,plain,
ssList(cons('#skF_52','#skF_53')),
inference(splitRight,[status(thm)],[c_95129]) ).
tff(c_196,plain,
! [U_906] :
( ( app(nil,U_906) = U_906 )
| ~ ssList(U_906) ),
inference(cnfTransformation,[status(thm)],[f_413]) ).
tff(c_18997,plain,
! [U_906] :
( ( app('#skF_53',U_906) = U_906 )
| ~ ssList(U_906) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_196]) ).
tff(c_95413,plain,
app('#skF_53',cons('#skF_52','#skF_53')) = cons('#skF_52','#skF_53'),
inference(resolution,[status(thm)],[c_95306,c_18997]) ).
tff(c_95430,plain,
app(cons('#skF_52','#skF_53'),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_95413,c_18989]) ).
tff(c_61643,plain,
! [V_1069,U_1067] :
( ( app(cons(V_1069,'#skF_53'),U_1067) = cons(V_1069,U_1067) )
| ~ ssItem(V_1069)
| ~ ssList(U_1067) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_346]) ).
tff(c_95726,plain,
( ( cons('#skF_52','#skF_54') = '#skF_50' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_95430,c_61643]) ).
tff(c_95772,plain,
cons('#skF_52','#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_95726]) ).
tff(c_190,plain,
! [V_895,U_893] :
( ( tl(cons(V_895,U_893)) = U_893 )
| ~ ssItem(V_895)
| ~ ssList(U_893) ),
inference(cnfTransformation,[status(thm)],[f_392]) ).
tff(c_95833,plain,
( ( tl('#skF_50') = '#skF_54' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_95772,c_190]) ).
tff(c_95886,plain,
'#skF_54' = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_22145,c_95833]) ).
tff(c_95888,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19456,c_95886]) ).
tff(c_95890,plain,
'#skF_47'('#skF_50') != '#skF_53',
inference(splitRight,[status(thm)],[c_20208]) ).
tff(c_24,plain,
! [U_30] :
( ssItem('#skF_5'(U_30))
| ~ singletonP(U_30)
| ~ ssList(U_30) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_22,plain,
! [U_30] :
( ( cons('#skF_5'(U_30),nil) = U_30 )
| ~ singletonP(U_30)
| ~ ssList(U_30) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_20484,plain,
! [U_2216] :
( ( cons('#skF_5'(U_2216),'#skF_53') = U_2216 )
| ~ singletonP(U_2216)
| ~ ssList(U_2216) ),
inference(demodulation,[status(thm),theory(equality)],[c_18979,c_22]) ).
tff(c_20490,plain,
! [U_2216] :
( ( tl(U_2216) = '#skF_53' )
| ~ ssItem('#skF_5'(U_2216))
| ~ ssList('#skF_53')
| ~ singletonP(U_2216)
| ~ ssList(U_2216) ),
inference(superposition,[status(thm),theory(equality)],[c_20484,c_190]) ).
tff(c_102193,plain,
! [U_3359] :
( ( tl(U_3359) = '#skF_53' )
| ~ ssItem('#skF_5'(U_3359))
| ~ singletonP(U_3359)
| ~ ssList(U_3359) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_20490]) ).
tff(c_102554,plain,
! [U_3363] :
( ( tl(U_3363) = '#skF_53' )
| ~ singletonP(U_3363)
| ~ ssList(U_3363) ),
inference(resolution,[status(thm)],[c_24,c_102193]) ).
tff(c_102680,plain,
( ( tl('#skF_50') = '#skF_53' )
| ~ singletonP('#skF_50') ),
inference(resolution,[status(thm)],[c_404,c_102554]) ).
tff(c_102735,plain,
'#skF_47'('#skF_50') = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_19534,c_102680]) ).
tff(c_102737,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_95890,c_102735]) ).
tff(c_102739,plain,
nil != '#skF_53',
inference(splitRight,[status(thm)],[c_18973]) ).
tff(c_102738,plain,
hd('#skF_53') = '#skF_46'('#skF_53'),
inference(splitRight,[status(thm)],[c_18973]) ).
tff(c_358,plain,
! [U_1081,V_1083] :
( ( hd(app(U_1081,V_1083)) = hd(U_1081) )
| ( nil = U_1081 )
| ~ ssList(V_1083)
| ~ ssList(U_1081) ),
inference(cnfTransformation,[status(thm)],[f_869]) ).
tff(c_242517,plain,
( ( hd('#skF_53') = hd('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52','#skF_54'))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_242372,c_358]) ).
tff(c_242592,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_102738,c_103976,c_242517]) ).
tff(c_242593,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(negUnitSimplification,[status(thm)],[c_102739,c_242592]) ).
tff(c_243508,plain,
'#skF_46'('#skF_53') = '#skF_46'('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_242912,c_242593]) ).
tff(c_103679,plain,
( ( tl('#skF_53') = '#skF_47'('#skF_53') )
| ( nil = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_392,c_103604]) ).
tff(c_103718,plain,
tl('#skF_53') = '#skF_47'('#skF_53'),
inference(negUnitSimplification,[status(thm)],[c_102739,c_103679]) ).
tff(c_103762,plain,
( ssList('#skF_47'('#skF_53'))
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_103718,c_188]) ).
tff(c_103766,plain,
( ssList('#skF_47'('#skF_53'))
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_103762]) ).
tff(c_103767,plain,
ssList('#skF_47'('#skF_53')),
inference(negUnitSimplification,[status(thm)],[c_102739,c_103766]) ).
tff(c_103784,plain,
( ( tl('#skF_47'('#skF_53')) = '#skF_47'('#skF_47'('#skF_53')) )
| ( '#skF_47'('#skF_53') = nil ) ),
inference(resolution,[status(thm)],[c_103767,c_334]) ).
tff(c_157970,plain,
'#skF_47'('#skF_53') = nil,
inference(splitLeft,[status(thm)],[c_103784]) ).
tff(c_104513,plain,
( ( cons(hd('#skF_53'),'#skF_47'('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_103718,c_104473]) ).
tff(c_104540,plain,
( ( cons('#skF_46'('#skF_53'),'#skF_47'('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_102738,c_104513]) ).
tff(c_104541,plain,
cons('#skF_46'('#skF_53'),'#skF_47'('#skF_53')) = '#skF_53',
inference(negUnitSimplification,[status(thm)],[c_102739,c_104540]) ).
tff(c_157972,plain,
cons('#skF_46'('#skF_53'),nil) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_157970,c_104541]) ).
tff(c_243521,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_243508,c_157972]) ).
tff(c_243527,plain,
'#skF_53' = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_157770,c_243521]) ).
tff(c_243529,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_243294,c_243527]) ).
tff(c_243531,plain,
'#skF_53' = '#skF_50',
inference(splitRight,[status(thm)],[c_243036]) ).
tff(c_242911,plain,
frontsegP('#skF_50','#skF_53'),
inference(splitRight,[status(thm)],[c_242590]) ).
tff(c_234,plain,
! [V_958,U_956] :
( ( V_958 = U_956 )
| ~ frontsegP(V_958,U_956)
| ~ frontsegP(U_956,V_958)
| ~ ssList(V_958)
| ~ ssList(U_956) ),
inference(cnfTransformation,[status(thm)],[f_544]) ).
tff(c_242916,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_53','#skF_50')
| ~ ssList('#skF_50')
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_242911,c_234]) ).
tff(c_242922,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_53','#skF_50') ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_404,c_242916]) ).
tff(c_243292,plain,
~ frontsegP('#skF_53','#skF_50'),
inference(splitLeft,[status(thm)],[c_242922]) ).
tff(c_243532,plain,
~ frontsegP('#skF_50','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_243531,c_243292]) ).
tff(c_243753,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_222396,c_243532]) ).
tff(c_243754,plain,
'#skF_53' = '#skF_50',
inference(splitRight,[status(thm)],[c_242922]) ).
tff(c_244076,plain,
cons('#skF_52','#skF_54') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_243754,c_243036]) ).
tff(c_182,plain,
! [V_887,U_885] :
( ( cons(V_887,U_885) != nil )
| ~ ssItem(V_887)
| ~ ssList(U_885) ),
inference(cnfTransformation,[status(thm)],[f_364]) ).
tff(c_244176,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_244076,c_182]) ).
tff(c_244253,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_244176]) ).
tff(c_244255,plain,
'#skF_47'('#skF_53') != nil,
inference(splitRight,[status(thm)],[c_103784]) ).
tff(c_18532,plain,
! [U_2109] :
( ( app(nil,U_2109) = U_2109 )
| ~ ssList(U_2109) ),
inference(cnfTransformation,[status(thm)],[f_413]) ).
tff(c_18548,plain,
app(nil,'#skF_53') = '#skF_53',
inference(resolution,[status(thm)],[c_392,c_18532]) ).
tff(c_150604,plain,
! [V_4150,W_4151] :
( frontsegP(app(V_4150,W_4151),V_4150)
| ~ ssList(W_4151)
| ~ ssList(V_4150)
| ~ ssList(app(V_4150,W_4151)) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_150795,plain,
( frontsegP('#skF_53',nil)
| ~ ssList('#skF_53')
| ~ ssList(nil)
| ~ ssList(app(nil,'#skF_53')) ),
inference(superposition,[status(thm),theory(equality)],[c_18548,c_150604]) ).
tff(c_150928,plain,
frontsegP('#skF_53',nil),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_18548,c_168,c_392,c_150795]) ).
tff(c_150950,plain,
( ( nil = '#skF_53' )
| ~ frontsegP(nil,'#skF_53')
| ~ ssList('#skF_53')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_150928,c_234]) ).
tff(c_150953,plain,
( ( nil = '#skF_53' )
| ~ frontsegP(nil,'#skF_53') ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_392,c_150950]) ).
tff(c_150954,plain,
~ frontsegP(nil,'#skF_53'),
inference(negUnitSimplification,[status(thm)],[c_102739,c_150953]) ).
tff(c_18552,plain,
app(nil,'#skF_50') = '#skF_50',
inference(resolution,[status(thm)],[c_404,c_18532]) ).
tff(c_139735,plain,
! [W_4040,V_4041] :
( rearsegP(app(W_4040,V_4041),V_4041)
| ~ ssList(W_4040)
| ~ ssList(V_4041)
| ~ ssList(app(W_4040,V_4041)) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_139917,plain,
( rearsegP('#skF_50','#skF_50')
| ~ ssList(nil)
| ~ ssList('#skF_50')
| ~ ssList(app(nil,'#skF_50')) ),
inference(superposition,[status(thm),theory(equality)],[c_18552,c_139735]) ).
tff(c_140060,plain,
rearsegP('#skF_50','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_18552,c_404,c_168,c_139917]) ).
tff(c_18508,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[c_168,c_18490]) ).
tff(c_140251,plain,
! [V_4046,W_4047] :
( frontsegP(app(V_4046,W_4047),V_4046)
| ~ ssList(W_4047)
| ~ ssList(V_4046)
| ~ ssList(app(V_4046,W_4047)) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_140457,plain,
( frontsegP(nil,nil)
| ~ ssList(nil)
| ~ ssList(nil)
| ~ ssList(app(nil,nil)) ),
inference(superposition,[status(thm),theory(equality)],[c_18508,c_140251]) ).
tff(c_140594,plain,
frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_18508,c_168,c_168,c_140457]) ).
tff(c_135271,plain,
'#skF_47'('#skF_50') = nil,
inference(splitLeft,[status(thm)],[c_103971]) ).
tff(c_139207,plain,
! [U_4037,V_4038] :
( ( hd(app(U_4037,V_4038)) = hd(U_4037) )
| ( nil = U_4037 )
| ~ ssList(V_4038)
| ~ ssList(U_4037) ),
inference(cnfTransformation,[status(thm)],[f_869]) ).
tff(c_139396,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = hd('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList('#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_139207]) ).
tff(c_139598,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_103976,c_139396]) ).
tff(c_139633,plain,
~ ssList(app('#skF_53',cons('#skF_52',nil))),
inference(splitLeft,[status(thm)],[c_139598]) ).
tff(c_139636,plain,
( ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_139633]) ).
tff(c_139639,plain,
~ ssList(cons('#skF_52',nil)),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_139636]) ).
tff(c_139642,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_139639]) ).
tff(c_139646,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_139642]) ).
tff(c_139647,plain,
( ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') ) ),
inference(splitRight,[status(thm)],[c_139598]) ).
tff(c_140232,plain,
hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50'),
inference(splitLeft,[status(thm)],[c_139647]) ).
tff(c_141243,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_358,c_140232]) ).
tff(c_141256,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_102738,c_141243]) ).
tff(c_141257,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ~ ssList(cons('#skF_52',nil)) ),
inference(negUnitSimplification,[status(thm)],[c_102739,c_141256]) ).
tff(c_141687,plain,
~ ssList(cons('#skF_52',nil)),
inference(splitLeft,[status(thm)],[c_141257]) ).
tff(c_141690,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_141687]) ).
tff(c_141694,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_141690]) ).
tff(c_141695,plain,
'#skF_46'('#skF_53') = '#skF_46'('#skF_50'),
inference(splitRight,[status(thm)],[c_141257]) ).
tff(c_141810,plain,
hd('#skF_53') = '#skF_46'('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_141695,c_102738]) ).
tff(c_340,plain,
! [U_1052] :
( ( cons(hd(U_1052),tl(U_1052)) = U_1052 )
| ( nil = U_1052 )
| ~ ssList(U_1052) ),
inference(cnfTransformation,[status(thm)],[f_803]) ).
tff(c_142173,plain,
( ( cons('#skF_46'('#skF_50'),tl('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_141810,c_340]) ).
tff(c_142183,plain,
( ( cons('#skF_46'('#skF_50'),'#skF_47'('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_103718,c_142173]) ).
tff(c_142184,plain,
cons('#skF_46'('#skF_50'),'#skF_47'('#skF_53')) = '#skF_53',
inference(negUnitSimplification,[status(thm)],[c_102739,c_142183]) ).
tff(c_184,plain,
! [U_888] :
( ssItem(hd(U_888))
| ( nil = U_888 )
| ~ ssList(U_888) ),
inference(cnfTransformation,[status(thm)],[f_371]) ).
tff(c_103980,plain,
( ssItem('#skF_46'('#skF_50'))
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_103976,c_184]) ).
tff(c_103984,plain,
( ssItem('#skF_46'('#skF_50'))
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_103980]) ).
tff(c_103985,plain,
ssItem('#skF_46'('#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_103942,c_103984]) ).
tff(c_135274,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_135271,c_104532]) ).
tff(c_138543,plain,
! [V_4026,U_4027] :
( ( app(cons(V_4026,nil),U_4027) = cons(V_4026,U_4027) )
| ~ ssItem(V_4026)
| ~ ssList(U_4027) ),
inference(cnfTransformation,[status(thm)],[f_834]) ).
tff(c_138562,plain,
! [U_4027] :
( ( cons('#skF_46'('#skF_50'),U_4027) = app('#skF_50',U_4027) )
| ~ ssItem('#skF_46'('#skF_50'))
| ~ ssList(U_4027) ),
inference(superposition,[status(thm),theory(equality)],[c_135274,c_138543]) ).
tff(c_138571,plain,
! [U_4027] :
( ( cons('#skF_46'('#skF_50'),U_4027) = app('#skF_50',U_4027) )
| ~ ssList(U_4027) ),
inference(demodulation,[status(thm),theory(equality)],[c_103985,c_138562]) ).
tff(c_142199,plain,
( ( app('#skF_50','#skF_47'('#skF_53')) = '#skF_53' )
| ~ ssList('#skF_47'('#skF_53')) ),
inference(superposition,[status(thm),theory(equality)],[c_142184,c_138571]) ).
tff(c_142230,plain,
app('#skF_50','#skF_47'('#skF_53')) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_103767,c_142199]) ).
tff(c_142263,plain,
( frontsegP('#skF_53','#skF_50')
| ~ ssList('#skF_47'('#skF_53'))
| ~ ssList('#skF_50')
| ~ ssList(app('#skF_50','#skF_47'('#skF_53'))) ),
inference(superposition,[status(thm),theory(equality)],[c_142230,c_26]) ).
tff(c_142295,plain,
frontsegP('#skF_53','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_142230,c_404,c_103767,c_142263]) ).
tff(c_142317,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_50','#skF_53')
| ~ ssList('#skF_53')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_142295,c_234]) ).
tff(c_142320,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_50','#skF_53') ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_392,c_142317]) ).
tff(c_142435,plain,
~ frontsegP('#skF_50','#skF_53'),
inference(splitLeft,[status(thm)],[c_142320]) ).
tff(c_141696,plain,
ssList(cons('#skF_52',nil)),
inference(splitRight,[status(thm)],[c_141257]) ).
tff(c_148770,plain,
! [U_4136,V_4137,W_4138] :
( ( app(app(U_4136,V_4137),W_4138) = app(U_4136,app(V_4137,W_4138)) )
| ~ ssList(W_4138)
| ~ ssList(V_4137)
| ~ ssList(U_4136) ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_148822,plain,
( ( app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_148770,c_421]) ).
tff(c_149060,plain,
app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_392,c_141696,c_390,c_148822]) ).
tff(c_149250,plain,
( ( app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_346,c_149060]) ).
tff(c_149289,plain,
app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_149250]) ).
tff(c_149319,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54'))
| ~ ssList('#skF_53')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_54'))) ),
inference(superposition,[status(thm),theory(equality)],[c_149289,c_26]) ).
tff(c_149356,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_149289,c_392,c_149319]) ).
tff(c_149357,plain,
~ ssList(cons('#skF_52','#skF_54')),
inference(negUnitSimplification,[status(thm)],[c_142435,c_149356]) ).
tff(c_149373,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(resolution,[status(thm)],[c_166,c_149357]) ).
tff(c_149377,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_149373]) ).
tff(c_149378,plain,
'#skF_53' = '#skF_50',
inference(splitRight,[status(thm)],[c_142320]) ).
tff(c_104218,plain,
! [U_3390] :
( ( cons('#skF_5'(U_3390),nil) = U_3390 )
| ~ singletonP(U_3390)
| ~ ssList(U_3390) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_326,plain,
! [U_1044] :
( equalelemsP(cons(U_1044,nil))
| ~ ssItem(U_1044) ),
inference(cnfTransformation,[status(thm)],[f_758]) ).
tff(c_104952,plain,
! [U_3422] :
( equalelemsP(U_3422)
| ~ ssItem('#skF_5'(U_3422))
| ~ singletonP(U_3422)
| ~ ssList(U_3422) ),
inference(superposition,[status(thm),theory(equality)],[c_104218,c_326]) ).
tff(c_104957,plain,
! [U_3423] :
( equalelemsP(U_3423)
| ~ singletonP(U_3423)
| ~ ssList(U_3423) ),
inference(resolution,[status(thm)],[c_24,c_104952]) ).
tff(c_105089,plain,
( equalelemsP('#skF_53')
| ~ singletonP('#skF_53') ),
inference(resolution,[status(thm)],[c_392,c_104957]) ).
tff(c_105097,plain,
~ singletonP('#skF_53'),
inference(splitLeft,[status(thm)],[c_105089]) ).
tff(c_102743,plain,
( ssItem('#skF_46'('#skF_53'))
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_102738,c_184]) ).
tff(c_102747,plain,
( ssItem('#skF_46'('#skF_53'))
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_102743]) ).
tff(c_102748,plain,
ssItem('#skF_46'('#skF_53')),
inference(negUnitSimplification,[status(thm)],[c_102739,c_102747]) ).
tff(c_103786,plain,
( ( hd('#skF_47'('#skF_53')) = '#skF_46'('#skF_47'('#skF_53')) )
| ( '#skF_47'('#skF_53') = nil ) ),
inference(resolution,[status(thm)],[c_103767,c_330]) ).
tff(c_135714,plain,
'#skF_47'('#skF_53') = nil,
inference(splitLeft,[status(thm)],[c_103786]) ).
tff(c_135717,plain,
cons('#skF_46'('#skF_53'),nil) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_135714,c_104541]) ).
tff(c_20,plain,
! [V_33] :
( singletonP(cons(V_33,nil))
| ~ ssItem(V_33)
| ~ ssList(cons(V_33,nil)) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_135776,plain,
( singletonP(cons('#skF_46'('#skF_53'),nil))
| ~ ssItem('#skF_46'('#skF_53'))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_135717,c_20]) ).
tff(c_135817,plain,
singletonP('#skF_53'),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_102748,c_135717,c_135776]) ).
tff(c_135819,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_105097,c_135817]) ).
tff(c_135821,plain,
'#skF_47'('#skF_53') != nil,
inference(splitRight,[status(thm)],[c_103786]) ).
tff(c_103787,plain,
app(nil,'#skF_47'('#skF_53')) = '#skF_47'('#skF_53'),
inference(resolution,[status(thm)],[c_103767,c_196]) ).
tff(c_140427,plain,
( frontsegP('#skF_47'('#skF_53'),nil)
| ~ ssList('#skF_47'('#skF_53'))
| ~ ssList(nil)
| ~ ssList(app(nil,'#skF_47'('#skF_53'))) ),
inference(superposition,[status(thm),theory(equality)],[c_103787,c_140251]) ).
tff(c_140574,plain,
frontsegP('#skF_47'('#skF_53'),nil),
inference(demodulation,[status(thm),theory(equality)],[c_103767,c_103787,c_168,c_103767,c_140427]) ).
tff(c_140714,plain,
( ( '#skF_47'('#skF_53') = nil )
| ~ frontsegP(nil,'#skF_47'('#skF_53'))
| ~ ssList('#skF_47'('#skF_53'))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_140574,c_234]) ).
tff(c_140717,plain,
( ( '#skF_47'('#skF_53') = nil )
| ~ frontsegP(nil,'#skF_47'('#skF_53')) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_103767,c_140714]) ).
tff(c_140718,plain,
~ frontsegP(nil,'#skF_47'('#skF_53')),
inference(negUnitSimplification,[status(thm)],[c_135821,c_140717]) ).
tff(c_149410,plain,
~ frontsegP(nil,'#skF_47'('#skF_50')),
inference(demodulation,[status(thm),theory(equality)],[c_149378,c_140718]) ).
tff(c_149482,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_140594,c_135271,c_149410]) ).
tff(c_149483,plain,
app('#skF_53',cons('#skF_52',nil)) = nil,
inference(splitRight,[status(thm)],[c_139647]) ).
tff(c_150067,plain,
app(nil,'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_149483,c_421]) ).
tff(c_18549,plain,
app(nil,'#skF_54') = '#skF_54',
inference(resolution,[status(thm)],[c_390,c_18532]) ).
tff(c_150107,plain,
'#skF_54' = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_150067,c_18549]) ).
tff(c_139648,plain,
ssList(app('#skF_53',cons('#skF_52',nil))),
inference(splitRight,[status(thm)],[c_139598]) ).
tff(c_139914,plain,
( rearsegP('#skF_50','#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52',nil)))
| ~ ssList('#skF_54')
| ~ ssList(app(app('#skF_53',cons('#skF_52',nil)),'#skF_54')) ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_139735]) ).
tff(c_140058,plain,
rearsegP('#skF_50','#skF_54'),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_421,c_390,c_139648,c_139914]) ).
tff(c_254,plain,
! [V_993,U_991] :
( ( V_993 = U_991 )
| ~ rearsegP(V_993,U_991)
| ~ rearsegP(U_991,V_993)
| ~ ssList(V_993)
| ~ ssList(U_991) ),
inference(cnfTransformation,[status(thm)],[f_612]) ).
tff(c_140078,plain,
( ( '#skF_54' = '#skF_50' )
| ~ rearsegP('#skF_54','#skF_50')
| ~ ssList('#skF_50')
| ~ ssList('#skF_54') ),
inference(resolution,[status(thm)],[c_140058,c_254]) ).
tff(c_140081,plain,
( ( '#skF_54' = '#skF_50' )
| ~ rearsegP('#skF_54','#skF_50') ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_404,c_140078]) ).
tff(c_140225,plain,
~ rearsegP('#skF_54','#skF_50'),
inference(splitLeft,[status(thm)],[c_140081]) ).
tff(c_150494,plain,
~ rearsegP('#skF_50','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_150107,c_140225]) ).
tff(c_150525,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_140060,c_150494]) ).
tff(c_150526,plain,
'#skF_54' = '#skF_50',
inference(splitRight,[status(thm)],[c_140081]) ).
tff(c_150550,plain,
app(app('#skF_53',cons('#skF_52',nil)),'#skF_50') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_150526,c_421]) ).
tff(c_152382,plain,
! [W_4163,U_4164,V_4165] :
( ( W_4163 = U_4164 )
| ( app(W_4163,V_4165) != app(U_4164,V_4165) )
| ~ ssList(W_4163)
| ~ ssList(V_4165)
| ~ ssList(U_4164) ),
inference(cnfTransformation,[status(thm)],[f_815]) ).
tff(c_152630,plain,
! [W_4163] :
( ( nil = W_4163 )
| ( app(W_4163,'#skF_50') != '#skF_50' )
| ~ ssList(W_4163)
| ~ ssList('#skF_50')
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_18552,c_152382]) ).
tff(c_155051,plain,
! [W_4185] :
( ( nil = W_4185 )
| ( app(W_4185,'#skF_50') != '#skF_50' )
| ~ ssList(W_4185) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_404,c_152630]) ).
tff(c_155054,plain,
( ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ( app(app('#skF_53',cons('#skF_52',nil)),'#skF_50') != '#skF_50' ) ),
inference(resolution,[status(thm)],[c_139648,c_155051]) ).
tff(c_155183,plain,
app('#skF_53',cons('#skF_52',nil)) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_150550,c_155054]) ).
tff(c_155377,plain,
( frontsegP(nil,'#skF_53')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53')
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_155183,c_26]) ).
tff(c_155408,plain,
( frontsegP(nil,'#skF_53')
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_155183,c_392,c_155377]) ).
tff(c_155409,plain,
~ ssList(cons('#skF_52',nil)),
inference(negUnitSimplification,[status(thm)],[c_150954,c_155408]) ).
tff(c_155427,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_155409]) ).
tff(c_155431,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_155427]) ).
tff(c_155433,plain,
'#skF_47'('#skF_50') != nil,
inference(splitRight,[status(thm)],[c_103971]) ).
tff(c_104301,plain,
! [V_3399,U_3400] :
( ( tl(cons(V_3399,U_3400)) = U_3400 )
| ~ ssItem(V_3399)
| ~ ssList(U_3400) ),
inference(cnfTransformation,[status(thm)],[f_392]) ).
tff(c_104313,plain,
! [U_30] :
( ( tl(U_30) = nil )
| ~ ssItem('#skF_5'(U_30))
| ~ ssList(nil)
| ~ singletonP(U_30)
| ~ ssList(U_30) ),
inference(superposition,[status(thm),theory(equality)],[c_22,c_104301]) ).
tff(c_157050,plain,
! [U_4233] :
( ( tl(U_4233) = nil )
| ~ ssItem('#skF_5'(U_4233))
| ~ singletonP(U_4233)
| ~ ssList(U_4233) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_104313]) ).
tff(c_157055,plain,
! [U_4234] :
( ( tl(U_4234) = nil )
| ~ singletonP(U_4234)
| ~ ssList(U_4234) ),
inference(resolution,[status(thm)],[c_24,c_157050]) ).
tff(c_157178,plain,
( ( tl('#skF_50') = nil )
| ~ singletonP('#skF_50') ),
inference(resolution,[status(thm)],[c_404,c_157055]) ).
tff(c_157233,plain,
'#skF_47'('#skF_50') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_103941,c_157178]) ).
tff(c_157235,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_155433,c_157233]) ).
tff(c_157237,plain,
singletonP('#skF_53'),
inference(splitRight,[status(thm)],[c_105089]) ).
tff(c_245237,plain,
! [U_5471] :
( ( tl(U_5471) = nil )
| ~ ssItem('#skF_5'(U_5471))
| ~ singletonP(U_5471)
| ~ ssList(U_5471) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_104313]) ).
tff(c_245242,plain,
! [U_5472] :
( ( tl(U_5472) = nil )
| ~ singletonP(U_5472)
| ~ ssList(U_5472) ),
inference(resolution,[status(thm)],[c_24,c_245237]) ).
tff(c_245344,plain,
( ( tl('#skF_53') = nil )
| ~ singletonP('#skF_53') ),
inference(resolution,[status(thm)],[c_392,c_245242]) ).
tff(c_245395,plain,
'#skF_47'('#skF_53') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_157237,c_103718,c_245344]) ).
tff(c_245397,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_244255,c_245395]) ).
tff(c_245399,plain,
'#skF_47'('#skF_50') != nil,
inference(splitRight,[status(thm)],[c_103971]) ).
tff(c_246258,plain,
! [U_5493] :
( ( tl(U_5493) = nil )
| ~ ssItem('#skF_5'(U_5493))
| ~ singletonP(U_5493)
| ~ ssList(U_5493) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_104313]) ).
tff(c_246263,plain,
! [U_5494] :
( ( tl(U_5494) = nil )
| ~ singletonP(U_5494)
| ~ ssList(U_5494) ),
inference(resolution,[status(thm)],[c_24,c_246258]) ).
tff(c_246371,plain,
( ( tl('#skF_50') = nil )
| ~ singletonP('#skF_50') ),
inference(resolution,[status(thm)],[c_404,c_246263]) ).
tff(c_246419,plain,
'#skF_47'('#skF_50') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_103941,c_246371]) ).
tff(c_246421,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_245399,c_246419]) ).
tff(c_246422,plain,
memberP('#skF_53','#skF_55'),
inference(splitRight,[status(thm)],[c_416]) ).
tff(c_246920,plain,
! [U_5551] :
( ( hd(U_5551) = '#skF_46'(U_5551) )
| ( nil = U_5551 )
| ~ ssList(U_5551) ),
inference(cnfTransformation,[status(thm)],[f_769]) ).
tff(c_247032,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_53') )
| ( nil = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_392,c_246920]) ).
tff(c_247297,plain,
nil = '#skF_53',
inference(splitLeft,[status(thm)],[c_247032]) ).
tff(c_247534,plain,
! [U_5564] :
( ~ memberP('#skF_53',U_5564)
| ~ ssItem(U_5564) ),
inference(demodulation,[status(thm),theory(equality)],[c_247297,c_228]) ).
tff(c_247537,plain,
~ ssItem('#skF_55'),
inference(resolution,[status(thm)],[c_246422,c_247534]) ).
tff(c_247541,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_247537]) ).
tff(c_247543,plain,
nil != '#skF_53',
inference(splitRight,[status(thm)],[c_247032]) ).
tff(c_247036,plain,
( ( hd('#skF_50') = '#skF_46'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_246920]) ).
tff(c_247247,plain,
nil = '#skF_50',
inference(splitLeft,[status(thm)],[c_247036]) ).
tff(c_247287,plain,
~ singletonP('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_247247,c_230]) ).
tff(c_247294,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_247287]) ).
tff(c_247296,plain,
nil != '#skF_50',
inference(splitRight,[status(thm)],[c_247036]) ).
tff(c_336737,plain,
! [U_7360] :
( ( tl(U_7360) = '#skF_47'(U_7360) )
| ( nil = U_7360 )
| ~ ssList(U_7360) ),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_336821,plain,
( ( tl('#skF_50') = '#skF_47'('#skF_50') )
| ( nil = '#skF_50' ) ),
inference(resolution,[status(thm)],[c_404,c_336737]) ).
tff(c_336859,plain,
tl('#skF_50') = '#skF_47'('#skF_50'),
inference(negUnitSimplification,[status(thm)],[c_247296,c_336821]) ).
tff(c_337043,plain,
( ssList('#skF_47'('#skF_50'))
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_336859,c_188]) ).
tff(c_337047,plain,
( ssList('#skF_47'('#skF_50'))
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_337043]) ).
tff(c_337048,plain,
ssList('#skF_47'('#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_247296,c_337047]) ).
tff(c_337068,plain,
( ( tl('#skF_47'('#skF_50')) = '#skF_47'('#skF_47'('#skF_50')) )
| ( '#skF_47'('#skF_50') = nil ) ),
inference(resolution,[status(thm)],[c_337048,c_334]) ).
tff(c_363272,plain,
'#skF_47'('#skF_50') = nil,
inference(splitLeft,[status(thm)],[c_337068]) ).
tff(c_363286,plain,
tl('#skF_50') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_363272,c_336859]) ).
tff(c_247542,plain,
hd('#skF_53') = '#skF_46'('#skF_53'),
inference(splitRight,[status(thm)],[c_247032]) ).
tff(c_247295,plain,
hd('#skF_50') = '#skF_46'('#skF_50'),
inference(splitRight,[status(thm)],[c_247036]) ).
tff(c_365407,plain,
! [U_7929,V_7930] :
( ( hd(app(U_7929,V_7930)) = hd(U_7929) )
| ( nil = U_7929 )
| ~ ssList(V_7930)
| ~ ssList(U_7929) ),
inference(cnfTransformation,[status(thm)],[f_869]) ).
tff(c_365533,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = hd('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList('#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_365407]) ).
tff(c_365675,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_247295,c_365533]) ).
tff(c_365836,plain,
~ ssList(app('#skF_53',cons('#skF_52',nil))),
inference(splitLeft,[status(thm)],[c_365675]) ).
tff(c_365839,plain,
( ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_365836]) ).
tff(c_365842,plain,
~ ssList(cons('#skF_52',nil)),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_365839]) ).
tff(c_365845,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_365842]) ).
tff(c_365849,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_365845]) ).
tff(c_365850,plain,
( ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') ) ),
inference(splitRight,[status(thm)],[c_365675]) ).
tff(c_366585,plain,
hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50'),
inference(splitLeft,[status(thm)],[c_365850]) ).
tff(c_366595,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_366585,c_358]) ).
tff(c_366608,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_247542,c_366595]) ).
tff(c_366609,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ~ ssList(cons('#skF_52',nil)) ),
inference(negUnitSimplification,[status(thm)],[c_247543,c_366608]) ).
tff(c_366618,plain,
~ ssList(cons('#skF_52',nil)),
inference(splitLeft,[status(thm)],[c_366609]) ).
tff(c_366621,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_366618]) ).
tff(c_366625,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_366621]) ).
tff(c_366627,plain,
ssList(cons('#skF_52',nil)),
inference(splitRight,[status(thm)],[c_366609]) ).
tff(c_363304,plain,
( ( cons(hd('#skF_50'),nil) = '#skF_50' )
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_363286,c_340]) ).
tff(c_363311,plain,
( ( cons('#skF_46'('#skF_50'),nil) = '#skF_50' )
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_247295,c_363304]) ).
tff(c_363312,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_50',
inference(negUnitSimplification,[status(thm)],[c_247296,c_363311]) ).
tff(c_366626,plain,
'#skF_46'('#skF_53') = '#skF_46'('#skF_50'),
inference(splitRight,[status(thm)],[c_366609]) ).
tff(c_336812,plain,
( ( tl('#skF_53') = '#skF_47'('#skF_53') )
| ( nil = '#skF_53' ) ),
inference(resolution,[status(thm)],[c_392,c_336737]) ).
tff(c_336851,plain,
tl('#skF_53') = '#skF_47'('#skF_53'),
inference(negUnitSimplification,[status(thm)],[c_247543,c_336812]) ).
tff(c_336866,plain,
( ssList('#skF_47'('#skF_53'))
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_336851,c_188]) ).
tff(c_336870,plain,
( ssList('#skF_47'('#skF_53'))
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_336866]) ).
tff(c_336871,plain,
ssList('#skF_47'('#skF_53')),
inference(negUnitSimplification,[status(thm)],[c_247543,c_336870]) ).
tff(c_336966,plain,
( ( tl('#skF_47'('#skF_53')) = '#skF_47'('#skF_47'('#skF_53')) )
| ( '#skF_47'('#skF_53') = nil ) ),
inference(resolution,[status(thm)],[c_336871,c_334]) ).
tff(c_363395,plain,
'#skF_47'('#skF_53') = nil,
inference(splitLeft,[status(thm)],[c_336966]) ).
tff(c_363402,plain,
tl('#skF_53') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_363395,c_336851]) ).
tff(c_363419,plain,
( ( cons(hd('#skF_53'),nil) = '#skF_53' )
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_363402,c_340]) ).
tff(c_363426,plain,
( ( cons('#skF_46'('#skF_53'),nil) = '#skF_53' )
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_247542,c_363419]) ).
tff(c_363427,plain,
cons('#skF_46'('#skF_53'),nil) = '#skF_53',
inference(negUnitSimplification,[status(thm)],[c_247543,c_363426]) ).
tff(c_366685,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_366626,c_363427]) ).
tff(c_366689,plain,
'#skF_53' = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_363312,c_366685]) ).
tff(c_366718,plain,
app(app('#skF_50',cons('#skF_52',nil)),'#skF_54') = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_366689,c_421]) ).
tff(c_375095,plain,
! [U_8076,V_8077,W_8078] :
( ( app(app(U_8076,V_8077),W_8078) = app(U_8076,app(V_8077,W_8078)) )
| ~ ssList(W_8078)
| ~ ssList(V_8077)
| ~ ssList(U_8076) ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_375212,plain,
( ( app('#skF_50',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_366718,c_375095]) ).
tff(c_375398,plain,
app('#skF_50',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_404,c_366627,c_390,c_375212]) ).
tff(c_375584,plain,
( ( app('#skF_50',cons('#skF_52','#skF_54')) = '#skF_50' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_346,c_375398]) ).
tff(c_375625,plain,
app('#skF_50',cons('#skF_52','#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_375584]) ).
tff(c_247547,plain,
( ssItem('#skF_46'('#skF_50'))
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_247295,c_184]) ).
tff(c_247551,plain,
( ssItem('#skF_46'('#skF_50'))
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_247547]) ).
tff(c_247552,plain,
ssItem('#skF_46'('#skF_50')),
inference(negUnitSimplification,[status(thm)],[c_247296,c_247551]) ).
tff(c_365954,plain,
! [V_7936,U_7937] :
( ( app(cons(V_7936,nil),U_7937) = cons(V_7936,U_7937) )
| ~ ssItem(V_7936)
| ~ ssList(U_7937) ),
inference(cnfTransformation,[status(thm)],[f_834]) ).
tff(c_365976,plain,
! [U_7937] :
( ( cons('#skF_46'('#skF_50'),U_7937) = app('#skF_50',U_7937) )
| ~ ssItem('#skF_46'('#skF_50'))
| ~ ssList(U_7937) ),
inference(superposition,[status(thm),theory(equality)],[c_363312,c_365954]) ).
tff(c_367143,plain,
! [U_7958] :
( ( cons('#skF_46'('#skF_50'),U_7958) = app('#skF_50',U_7958) )
| ~ ssList(U_7958) ),
inference(demodulation,[status(thm),theory(equality)],[c_247552,c_365976]) ).
tff(c_367166,plain,
! [U_7958] :
( ( tl(app('#skF_50',U_7958)) = U_7958 )
| ~ ssItem('#skF_46'('#skF_50'))
| ~ ssList(U_7958)
| ~ ssList(U_7958) ),
inference(superposition,[status(thm),theory(equality)],[c_367143,c_190]) ).
tff(c_367223,plain,
! [U_7958] :
( ( tl(app('#skF_50',U_7958)) = U_7958 )
| ~ ssList(U_7958) ),
inference(demodulation,[status(thm),theory(equality)],[c_247552,c_367166]) ).
tff(c_375673,plain,
( ( cons('#skF_52','#skF_54') = tl('#skF_50') )
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(superposition,[status(thm),theory(equality)],[c_375625,c_367223]) ).
tff(c_375714,plain,
( ( cons('#skF_52','#skF_54') = nil )
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(demodulation,[status(thm),theory(equality)],[c_363286,c_375673]) ).
tff(c_376039,plain,
~ ssList(cons('#skF_52','#skF_54')),
inference(splitLeft,[status(thm)],[c_375714]) ).
tff(c_376059,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(resolution,[status(thm)],[c_166,c_376039]) ).
tff(c_376063,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_376059]) ).
tff(c_376064,plain,
cons('#skF_52','#skF_54') = nil,
inference(splitRight,[status(thm)],[c_375714]) ).
tff(c_376224,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_376064,c_182]) ).
tff(c_376255,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_376224]) ).
tff(c_376256,plain,
app('#skF_53',cons('#skF_52',nil)) = nil,
inference(splitRight,[status(thm)],[c_365850]) ).
tff(c_376274,plain,
( ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_376256,c_352]) ).
tff(c_376288,plain,
( ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_376274]) ).
tff(c_376289,plain,
~ ssList(cons('#skF_52',nil)),
inference(negUnitSimplification,[status(thm)],[c_247543,c_376288]) ).
tff(c_376382,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_376289]) ).
tff(c_376386,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_376382]) ).
tff(c_376388,plain,
'#skF_47'('#skF_53') != nil,
inference(splitRight,[status(thm)],[c_336966]) ).
tff(c_246424,plain,
! [U_5495] :
( ( app(U_5495,nil) = U_5495 )
| ~ ssList(U_5495) ),
inference(cnfTransformation,[status(thm)],[f_859]) ).
tff(c_246441,plain,
app('#skF_54',nil) = '#skF_54',
inference(resolution,[status(thm)],[c_390,c_246424]) ).
tff(c_340369,plain,
'#skF_47'('#skF_50') = nil,
inference(splitLeft,[status(thm)],[c_337068]) ).
tff(c_337587,plain,
! [U_7388] :
( ( cons(hd(U_7388),tl(U_7388)) = U_7388 )
| ( nil = U_7388 )
| ~ ssList(U_7388) ),
inference(cnfTransformation,[status(thm)],[f_803]) ).
tff(c_337636,plain,
( ( cons('#skF_46'('#skF_50'),tl('#skF_50')) = '#skF_50' )
| ( nil = '#skF_50' )
| ~ ssList('#skF_50') ),
inference(superposition,[status(thm),theory(equality)],[c_247295,c_337587]) ).
tff(c_337663,plain,
( ( cons('#skF_46'('#skF_50'),'#skF_47'('#skF_50')) = '#skF_50' )
| ( nil = '#skF_50' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_336859,c_337636]) ).
tff(c_337664,plain,
cons('#skF_46'('#skF_50'),'#skF_47'('#skF_50')) = '#skF_50',
inference(negUnitSimplification,[status(thm)],[c_247296,c_337663]) ).
tff(c_340371,plain,
cons('#skF_46'('#skF_50'),nil) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_340369,c_337664]) ).
tff(c_344436,plain,
! [V_7570,U_7571] :
( ( app(cons(V_7570,nil),U_7571) = cons(V_7570,U_7571) )
| ~ ssItem(V_7570)
| ~ ssList(U_7571) ),
inference(cnfTransformation,[status(thm)],[f_834]) ).
tff(c_344464,plain,
! [U_7571] :
( ( cons('#skF_46'('#skF_50'),U_7571) = app('#skF_50',U_7571) )
| ~ ssItem('#skF_46'('#skF_50'))
| ~ ssList(U_7571) ),
inference(superposition,[status(thm),theory(equality)],[c_340371,c_344436]) ).
tff(c_344483,plain,
! [U_7572] :
( ( cons('#skF_46'('#skF_50'),U_7572) = app('#skF_50',U_7572) )
| ~ ssList(U_7572) ),
inference(demodulation,[status(thm),theory(equality)],[c_247552,c_344464]) ).
tff(c_343338,plain,
! [U_7553,V_7554] :
( ( hd(app(U_7553,V_7554)) = hd(U_7553) )
| ( nil = U_7553 )
| ~ ssList(V_7554)
| ~ ssList(U_7553) ),
inference(cnfTransformation,[status(thm)],[f_869]) ).
tff(c_343518,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = hd('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList('#skF_54')
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_343338]) ).
tff(c_343714,plain,
( ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') )
| ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ~ ssList(app('#skF_53',cons('#skF_52',nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_247295,c_343518]) ).
tff(c_343745,plain,
~ ssList(app('#skF_53',cons('#skF_52',nil))),
inference(splitLeft,[status(thm)],[c_343714]) ).
tff(c_343748,plain,
( ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(resolution,[status(thm)],[c_192,c_343745]) ).
tff(c_343751,plain,
~ ssList(cons('#skF_52',nil)),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_343748]) ).
tff(c_343754,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_343751]) ).
tff(c_343758,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_343754]) ).
tff(c_343759,plain,
( ( app('#skF_53',cons('#skF_52',nil)) = nil )
| ( hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50') ) ),
inference(splitRight,[status(thm)],[c_343714]) ).
tff(c_343887,plain,
hd(app('#skF_53',cons('#skF_52',nil))) = '#skF_46'('#skF_50'),
inference(splitLeft,[status(thm)],[c_343759]) ).
tff(c_343921,plain,
( ( hd('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_343887,c_358]) ).
tff(c_343934,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_247542,c_343921]) ).
tff(c_343935,plain,
( ( '#skF_46'('#skF_53') = '#skF_46'('#skF_50') )
| ~ ssList(cons('#skF_52',nil)) ),
inference(negUnitSimplification,[status(thm)],[c_247543,c_343934]) ).
tff(c_343944,plain,
~ ssList(cons('#skF_52',nil)),
inference(splitLeft,[status(thm)],[c_343935]) ).
tff(c_343947,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_343944]) ).
tff(c_343951,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_343947]) ).
tff(c_343952,plain,
'#skF_46'('#skF_53') = '#skF_46'('#skF_50'),
inference(splitRight,[status(thm)],[c_343935]) ).
tff(c_344126,plain,
hd('#skF_53') = '#skF_46'('#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_343952,c_247542]) ).
tff(c_344142,plain,
( ( cons('#skF_46'('#skF_50'),tl('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_344126,c_340]) ).
tff(c_344149,plain,
( ( cons('#skF_46'('#skF_50'),'#skF_47'('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_336851,c_344142]) ).
tff(c_344150,plain,
cons('#skF_46'('#skF_50'),'#skF_47'('#skF_53')) = '#skF_53',
inference(negUnitSimplification,[status(thm)],[c_247543,c_344149]) ).
tff(c_344493,plain,
( ( app('#skF_50','#skF_47'('#skF_53')) = '#skF_53' )
| ~ ssList('#skF_47'('#skF_53')) ),
inference(superposition,[status(thm),theory(equality)],[c_344483,c_344150]) ).
tff(c_344564,plain,
app('#skF_50','#skF_47'('#skF_53')) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_336871,c_344493]) ).
tff(c_345650,plain,
! [V_7584,W_7585] :
( frontsegP(app(V_7584,W_7585),V_7584)
| ~ ssList(W_7585)
| ~ ssList(V_7584)
| ~ ssList(app(V_7584,W_7585)) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_345661,plain,
( frontsegP('#skF_53','#skF_50')
| ~ ssList('#skF_47'('#skF_53'))
| ~ ssList('#skF_50')
| ~ ssList(app('#skF_50','#skF_47'('#skF_53'))) ),
inference(superposition,[status(thm),theory(equality)],[c_344564,c_345650]) ).
tff(c_345868,plain,
frontsegP('#skF_53','#skF_50'),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_344564,c_404,c_336871,c_345661]) ).
tff(c_346901,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_50','#skF_53')
| ~ ssList('#skF_53')
| ~ ssList('#skF_50') ),
inference(resolution,[status(thm)],[c_345868,c_234]) ).
tff(c_346904,plain,
( ( '#skF_53' = '#skF_50' )
| ~ frontsegP('#skF_50','#skF_53') ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_392,c_346901]) ).
tff(c_348977,plain,
~ frontsegP('#skF_50','#skF_53'),
inference(splitLeft,[status(thm)],[c_346904]) ).
tff(c_343953,plain,
ssList(cons('#skF_52',nil)),
inference(splitRight,[status(thm)],[c_343935]) ).
tff(c_356137,plain,
! [U_7719,V_7720,W_7721] :
( ( app(app(U_7719,V_7720),W_7721) = app(U_7719,app(V_7720,W_7721)) )
| ~ ssList(W_7721)
| ~ ssList(V_7720)
| ~ ssList(U_7719) ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_356406,plain,
( ( app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50' )
| ~ ssList('#skF_54')
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_421,c_356137]) ).
tff(c_356565,plain,
app('#skF_53',app(cons('#skF_52',nil),'#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_392,c_343953,c_390,c_356406]) ).
tff(c_358525,plain,
( ( app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50' )
| ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(superposition,[status(thm),theory(equality)],[c_346,c_356565]) ).
tff(c_358568,plain,
app('#skF_53',cons('#skF_52','#skF_54')) = '#skF_50',
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_358525]) ).
tff(c_358618,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54'))
| ~ ssList('#skF_53')
| ~ ssList(app('#skF_53',cons('#skF_52','#skF_54'))) ),
inference(superposition,[status(thm),theory(equality)],[c_358568,c_26]) ).
tff(c_358658,plain,
( frontsegP('#skF_50','#skF_53')
| ~ ssList(cons('#skF_52','#skF_54')) ),
inference(demodulation,[status(thm),theory(equality)],[c_404,c_358568,c_392,c_358618]) ).
tff(c_358659,plain,
~ ssList(cons('#skF_52','#skF_54')),
inference(negUnitSimplification,[status(thm)],[c_348977,c_358658]) ).
tff(c_358673,plain,
( ~ ssItem('#skF_52')
| ~ ssList('#skF_54') ),
inference(resolution,[status(thm)],[c_166,c_358659]) ).
tff(c_358677,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_390,c_394,c_358673]) ).
tff(c_358678,plain,
'#skF_53' = '#skF_50',
inference(splitRight,[status(thm)],[c_346904]) ).
tff(c_337187,plain,
! [U_7373] :
( ( cons('#skF_5'(U_7373),nil) = U_7373 )
| ~ singletonP(U_7373)
| ~ ssList(U_7373) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_280,plain,
! [U_1032] :
( cyclefreeP(cons(U_1032,nil))
| ~ ssItem(U_1032) ),
inference(cnfTransformation,[status(thm)],[f_696]) ).
tff(c_337415,plain,
! [U_7386] :
( cyclefreeP(U_7386)
| ~ ssItem('#skF_5'(U_7386))
| ~ singletonP(U_7386)
| ~ ssList(U_7386) ),
inference(superposition,[status(thm),theory(equality)],[c_337187,c_280]) ).
tff(c_337449,plain,
! [U_7387] :
( cyclefreeP(U_7387)
| ~ singletonP(U_7387)
| ~ ssList(U_7387) ),
inference(resolution,[status(thm)],[c_24,c_337415]) ).
tff(c_337577,plain,
( cyclefreeP('#skF_53')
| ~ singletonP('#skF_53') ),
inference(resolution,[status(thm)],[c_392,c_337449]) ).
tff(c_337585,plain,
~ singletonP('#skF_53'),
inference(splitLeft,[status(thm)],[c_337577]) ).
tff(c_247675,plain,
( ssItem('#skF_46'('#skF_53'))
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_247542,c_184]) ).
tff(c_247679,plain,
( ssItem('#skF_46'('#skF_53'))
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_247675]) ).
tff(c_247680,plain,
ssItem('#skF_46'('#skF_53')),
inference(negUnitSimplification,[status(thm)],[c_247543,c_247679]) ).
tff(c_340481,plain,
'#skF_47'('#skF_53') = nil,
inference(splitLeft,[status(thm)],[c_336966]) ).
tff(c_337633,plain,
( ( cons('#skF_46'('#skF_53'),tl('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' )
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_247542,c_337587]) ).
tff(c_337660,plain,
( ( cons('#skF_46'('#skF_53'),'#skF_47'('#skF_53')) = '#skF_53' )
| ( nil = '#skF_53' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_336851,c_337633]) ).
tff(c_337661,plain,
cons('#skF_46'('#skF_53'),'#skF_47'('#skF_53')) = '#skF_53',
inference(negUnitSimplification,[status(thm)],[c_247543,c_337660]) ).
tff(c_340486,plain,
cons('#skF_46'('#skF_53'),nil) = '#skF_53',
inference(demodulation,[status(thm),theory(equality)],[c_340481,c_337661]) ).
tff(c_340649,plain,
! [V_7464] :
( singletonP(cons(V_7464,nil))
| ~ ssItem(V_7464)
| ~ ssList(cons(V_7464,nil)) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_340652,plain,
( singletonP(cons('#skF_46'('#skF_53'),nil))
| ~ ssItem('#skF_46'('#skF_53'))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_340486,c_340649]) ).
tff(c_340667,plain,
singletonP('#skF_53'),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_247680,c_340486,c_340652]) ).
tff(c_340669,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_337585,c_340667]) ).
tff(c_340671,plain,
'#skF_47'('#skF_53') != nil,
inference(splitRight,[status(thm)],[c_336966]) ).
tff(c_347020,plain,
! [W_7597,U_7598,V_7599] :
( ( W_7597 = U_7598 )
| ( app(V_7599,W_7597) != app(V_7599,U_7598) )
| ~ ssList(W_7597)
| ~ ssList(V_7599)
| ~ ssList(U_7598) ),
inference(cnfTransformation,[status(thm)],[f_827]) ).
tff(c_347298,plain,
! [U_7598] :
( ( nil = U_7598 )
| ( app('#skF_54',U_7598) != '#skF_54' )
| ~ ssList(nil)
| ~ ssList('#skF_54')
| ~ ssList(U_7598) ),
inference(superposition,[status(thm),theory(equality)],[c_246441,c_347020]) ).
tff(c_348374,plain,
! [U_7604] :
( ( nil = U_7604 )
| ( app('#skF_54',U_7604) != '#skF_54' )
| ~ ssList(U_7604) ),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_168,c_347298]) ).
tff(c_348422,plain,
( ( '#skF_47'('#skF_53') = nil )
| ( app('#skF_54','#skF_47'('#skF_53')) != '#skF_54' ) ),
inference(resolution,[status(thm)],[c_336871,c_348374]) ).
tff(c_348538,plain,
app('#skF_54','#skF_47'('#skF_53')) != '#skF_54',
inference(negUnitSimplification,[status(thm)],[c_340671,c_348422]) ).
tff(c_358682,plain,
app('#skF_54','#skF_47'('#skF_50')) != '#skF_54',
inference(demodulation,[status(thm),theory(equality)],[c_358678,c_348538]) ).
tff(c_358758,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_246441,c_340369,c_358682]) ).
tff(c_358759,plain,
app('#skF_53',cons('#skF_52',nil)) = nil,
inference(splitRight,[status(thm)],[c_343759]) ).
tff(c_358775,plain,
( ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil))
| ~ ssList('#skF_53') ),
inference(superposition,[status(thm),theory(equality)],[c_358759,c_352]) ).
tff(c_358788,plain,
( ( nil = '#skF_53' )
| ~ ssList(cons('#skF_52',nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_358775]) ).
tff(c_358789,plain,
~ ssList(cons('#skF_52',nil)),
inference(negUnitSimplification,[status(thm)],[c_247543,c_358788]) ).
tff(c_358874,plain,
( ~ ssItem('#skF_52')
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_166,c_358789]) ).
tff(c_358878,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_168,c_394,c_358874]) ).
tff(c_358880,plain,
'#skF_47'('#skF_50') != nil,
inference(splitRight,[status(thm)],[c_337068]) ).
tff(c_337193,plain,
! [U_7373] :
( ( tl(U_7373) = nil )
| ~ ssItem('#skF_5'(U_7373))
| ~ ssList(nil)
| ~ singletonP(U_7373)
| ~ ssList(U_7373) ),
inference(superposition,[status(thm),theory(equality)],[c_337187,c_190]) ).
tff(c_360910,plain,
! [U_7801] :
( ( tl(U_7801) = nil )
| ~ ssItem('#skF_5'(U_7801))
| ~ singletonP(U_7801)
| ~ ssList(U_7801) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_337193]) ).
tff(c_360915,plain,
! [U_7802] :
( ( tl(U_7802) = nil )
| ~ singletonP(U_7802)
| ~ ssList(U_7802) ),
inference(resolution,[status(thm)],[c_24,c_360910]) ).
tff(c_361041,plain,
( ( tl('#skF_50') = nil )
| ~ singletonP('#skF_50') ),
inference(resolution,[status(thm)],[c_404,c_360915]) ).
tff(c_361098,plain,
'#skF_47'('#skF_50') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_336859,c_361041]) ).
tff(c_361100,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358880,c_361098]) ).
tff(c_361102,plain,
singletonP('#skF_53'),
inference(splitRight,[status(thm)],[c_337577]) ).
tff(c_379021,plain,
! [U_8154] :
( ( tl(U_8154) = nil )
| ~ ssItem('#skF_5'(U_8154))
| ~ singletonP(U_8154)
| ~ ssList(U_8154) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_337193]) ).
tff(c_379026,plain,
! [U_8155] :
( ( tl(U_8155) = nil )
| ~ singletonP(U_8155)
| ~ ssList(U_8155) ),
inference(resolution,[status(thm)],[c_24,c_379021]) ).
tff(c_379143,plain,
( ( tl('#skF_53') = nil )
| ~ singletonP('#skF_53') ),
inference(resolution,[status(thm)],[c_392,c_379026]) ).
tff(c_379202,plain,
'#skF_47'('#skF_53') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_361102,c_336851,c_379143]) ).
tff(c_379204,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_376388,c_379202]) ).
tff(c_379206,plain,
'#skF_47'('#skF_50') != nil,
inference(splitRight,[status(thm)],[c_337068]) ).
tff(c_380771,plain,
! [U_8199] :
( ( tl(U_8199) = nil )
| ~ ssItem('#skF_5'(U_8199))
| ~ singletonP(U_8199)
| ~ ssList(U_8199) ),
inference(demodulation,[status(thm),theory(equality)],[c_168,c_337193]) ).
tff(c_380776,plain,
! [U_8200] :
( ( tl(U_8200) = nil )
| ~ singletonP(U_8200)
| ~ ssList(U_8200) ),
inference(resolution,[status(thm)],[c_24,c_380771]) ).
tff(c_380890,plain,
( ( tl('#skF_50') = nil )
| ~ singletonP('#skF_50') ),
inference(resolution,[status(thm)],[c_404,c_380776]) ).
tff(c_380941,plain,
'#skF_47'('#skF_50') = nil,
inference(demodulation,[status(thm),theory(equality)],[c_18477,c_336859,c_380890]) ).
tff(c_380943,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_379206,c_380941]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC285+1 : TPTP v9.0.0. Released v2.4.0.
% 0.14/0.13 % 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.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 02:06:35 EDT 2025
% 0.14/0.34 % CPUTime :
% 84.49/66.75 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.59/66.82
% 84.59/66.82 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------