%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC284-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 : n004.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 : Unsatisfiable 249.48s 226.39s
% Output : CNFRefutation 249.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 53
% Syntax : Number of formulae : 688 ( 312 unt; 0 typ; 0 def)
% Number of atoms : 1540 ( 391 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1761 ( 909 ~; 852 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 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 : 58 ( 58 usr; 12 con; 0-2 aty)
% Number of variables : 327 ( 327 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ segmentP > rearsegP > neq > memberP > lt > leq > gt > geq > frontsegP > totalorderedP > totalorderP > strictorderedP > strictorderP > ssList > ssItem > singletonP > equalelemsP > duplicatefreeP > cyclefreeP > skaf48 > skaf47 > skaf46 > skaf45 > skaf43 > skaf42 > cons > app > #nlpp > tl > skaf83 > skaf82 > skaf81 > skaf80 > skaf79 > skaf78 > skaf77 > skaf76 > skaf75 > skaf74 > skaf73 > skaf72 > skaf71 > skaf70 > skaf69 > skaf68 > skaf67 > skaf66 > skaf65 > skaf64 > skaf63 > skaf62 > skaf61 > skaf60 > skaf59 > skaf58 > skaf57 > skaf56 > skaf55 > skaf54 > skaf53 > skaf52 > skaf51 > skaf50 > skaf49 > skaf44 > hd > skac3 > skac2 > sk9 > sk8 > sk7 > sk6 > sk5 > sk4 > sk3 > sk2 > sk1 > nil
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(skaf56,type,
skaf56: $i > $i ).
tff(segmentP,type,
segmentP: ( $i * $i ) > $o ).
tff(totalorderedP,type,
totalorderedP: $i > $o ).
tff(equalelemsP,type,
equalelemsP: $i > $o ).
tff(skaf74,type,
skaf74: $i > $i ).
tff(skaf61,type,
skaf61: $i > $i ).
tff(skaf51,type,
skaf51: $i > $i ).
tff(skaf83,type,
skaf83: $i > $i ).
tff(skac2,type,
skac2: $i ).
tff(skaf63,type,
skaf63: $i > $i ).
tff(skaf62,type,
skaf62: $i > $i ).
tff(sk9,type,
sk9: $i ).
tff(sk2,type,
sk2: $i ).
tff(skaf52,type,
skaf52: $i > $i ).
tff(skaf50,type,
skaf50: $i > $i ).
tff(skaf42,type,
skaf42: ( $i * $i ) > $i ).
tff(skaf44,type,
skaf44: $i > $i ).
tff(singletonP,type,
singletonP: $i > $o ).
tff(skaf67,type,
skaf67: $i > $i ).
tff(skaf75,type,
skaf75: $i > $i ).
tff(sk1,type,
sk1: $i ).
tff(skaf58,type,
skaf58: $i > $i ).
tff(skaf46,type,
skaf46: ( $i * $i ) > $i ).
tff(frontsegP,type,
frontsegP: ( $i * $i ) > $o ).
tff(skaf70,type,
skaf70: $i > $i ).
tff(totalorderP,type,
totalorderP: $i > $o ).
tff(ssItem,type,
ssItem: $i > $o ).
tff(sk6,type,
sk6: $i ).
tff(skaf82,type,
skaf82: $i > $i ).
tff(skaf47,type,
skaf47: ( $i * $i ) > $i ).
tff(skaf76,type,
skaf76: $i > $i ).
tff(skac3,type,
skac3: $i ).
tff(skaf80,type,
skaf80: $i > $i ).
tff(skaf59,type,
skaf59: $i > $i ).
tff(skaf53,type,
skaf53: $i > $i ).
tff(skaf45,type,
skaf45: ( $i * $i ) > $i ).
tff(hd,type,
hd: $i > $i ).
tff(app,type,
app: ( $i * $i ) > $i ).
tff(skaf72,type,
skaf72: $i > $i ).
tff(duplicatefreeP,type,
duplicatefreeP: $i > $o ).
tff(skaf64,type,
skaf64: $i > $i ).
tff(sk4,type,
sk4: $i ).
tff(sk8,type,
sk8: $i ).
tff(gt,type,
gt: ( $i * $i ) > $o ).
tff(skaf71,type,
skaf71: $i > $i ).
tff(skaf78,type,
skaf78: $i > $i ).
tff(sk5,type,
sk5: $i ).
tff(skaf79,type,
skaf79: $i > $i ).
tff(rearsegP,type,
rearsegP: ( $i * $i ) > $o ).
tff(memberP,type,
memberP: ( $i * $i ) > $o ).
tff(skaf73,type,
skaf73: $i > $i ).
tff(ssList,type,
ssList: $i > $o ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(skaf54,type,
skaf54: $i > $i ).
tff(skaf77,type,
skaf77: $i > $i ).
tff(sk3,type,
sk3: $i ).
tff(skaf66,type,
skaf66: $i > $i ).
tff(strictorderP,type,
strictorderP: $i > $o ).
tff(skaf81,type,
skaf81: $i > $i ).
tff(geq,type,
geq: ( $i * $i ) > $o ).
tff(skaf60,type,
skaf60: $i > $i ).
tff(leq,type,
leq: ( $i * $i ) > $o ).
tff(lt,type,
lt: ( $i * $i ) > $o ).
tff(skaf69,type,
skaf69: $i > $i ).
tff(tl,type,
tl: $i > $i ).
tff(neq,type,
neq: ( $i * $i ) > $o ).
tff(skaf43,type,
skaf43: ( $i * $i ) > $i ).
tff(skaf48,type,
skaf48: ( $i * $i ) > $i ).
tff(skaf65,type,
skaf65: $i > $i ).
tff(skaf57,type,
skaf57: $i > $i ).
tff(sk7,type,
sk7: $i ).
tff(nil,type,
nil: $i ).
tff(skaf49,type,
skaf49: $i > $i ).
tff(skaf55,type,
skaf55: $i > $i ).
tff(skaf68,type,
skaf68: $i > $i ).
tff(strictorderedP,type,
strictorderedP: $i > $o ).
tff(cyclefreeP,type,
cyclefreeP: $i > $o ).
tff(f_1655,axiom,
ssItem(sk8),
file(unknown,unknown) ).
tff(f_1651,axiom,
ssItem(sk5),
file(unknown,unknown) ).
tff(f_56,axiom,
ssList(nil),
file(unknown,unknown) ).
tff(f_342,axiom,
! [U,V] :
( ~ ssItem(U)
| ~ ssList(V)
| ssList(cons(U,V)) ),
file(unknown,unknown) ).
tff(f_1652,axiom,
ssList(sk6),
file(unknown,unknown) ).
tff(f_334,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ssList(app(V,U)) ),
file(unknown,unknown) ).
tff(f_1653,axiom,
ssList(sk7),
file(unknown,unknown) ).
tff(f_245,axiom,
! [U] :
( ~ ssList(U)
| ( app(U,nil) = U ) ),
file(unknown,unknown) ).
tff(f_961,axiom,
! [U,V,W] :
( ( app(U,V) != W )
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| rearsegP(W,V) ),
file(unknown,unknown) ).
tff(f_770,axiom,
! [U,V] :
( ~ rearsegP(U,V)
| ~ rearsegP(V,U)
| ~ ssList(U)
| ~ ssList(V)
| ( V = U ) ),
file(unknown,unknown) ).
tff(f_1650,axiom,
sk1 = sk3,
file(unknown,unknown) ).
tff(f_1647,axiom,
ssList(sk3),
file(unknown,unknown) ).
tff(f_1649,axiom,
sk2 = sk4,
file(unknown,unknown) ).
tff(f_1675,axiom,
( ( nil = sk3 )
| ( nil != sk4 ) ),
file(unknown,unknown) ).
tff(f_1648,axiom,
ssList(sk4),
file(unknown,unknown) ).
tff(f_456,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| neq(V,U)
| ( V = U ) ),
file(unknown,unknown) ).
tff(f_1679,axiom,
( ssItem(sk9)
| ~ neq(sk4,nil) ),
file(unknown,unknown) ).
tff(f_1683,axiom,
( ( cons(sk9,nil) = sk3 )
| ~ neq(sk4,nil) ),
file(unknown,unknown) ).
tff(f_666,axiom,
! [U,V] :
( ~ ssItem(U)
| ~ ssList(V)
| ( app(cons(U,nil),V) = cons(U,V) ) ),
file(unknown,unknown) ).
tff(f_446,axiom,
! [U,V] :
( ( cons(U,V) != V )
| ~ ssItem(U)
| ~ ssList(V) ),
file(unknown,unknown) ).
tff(f_250,axiom,
! [U] :
( ~ ssList(U)
| ( app(nil,U) = U ) ),
file(unknown,unknown) ).
tff(f_975,axiom,
! [U,V,W] :
( ( app(U,V) != W )
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| frontsegP(W,U) ),
file(unknown,unknown) ).
tff(f_1460,axiom,
! [U,V,W,X] :
( ~ frontsegP(U,V)
| ( W != X )
| ~ ssList(V)
| ~ ssList(U)
| ~ ssItem(X)
| ~ ssItem(W)
| frontsegP(cons(W,U),cons(X,V)) ),
file(unknown,unknown) ).
tff(f_784,axiom,
! [U,V] :
( ~ frontsegP(U,V)
| ~ frontsegP(V,U)
| ~ ssList(U)
| ~ ssList(V)
| ( V = U ) ),
file(unknown,unknown) ).
tff(f_1654,axiom,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
file(unknown,unknown) ).
tff(f_1371,axiom,
! [U,V,W,X] :
( ( app(app(U,V),W) != X )
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| segmentP(X,V) ),
file(unknown,unknown) ).
tff(f_1051,axiom,
! [U,V,W] :
( ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ( app(app(W,V),U) = app(W,app(V,U)) ) ),
file(unknown,unknown) ).
tff(f_186,axiom,
! [U] :
( ~ ssItem(U)
| leq(U,U) ),
file(unknown,unknown) ).
tff(f_64,axiom,
! [U] : ssList(skaf82(U)),
file(unknown,unknown) ).
tff(f_420,axiom,
! [U,V] :
( ~ ssItem(U)
| ~ ssList(V)
| ( tl(cons(U,V)) = V ) ),
file(unknown,unknown) ).
tff(f_437,axiom,
! [U,V] :
( ( cons(U,V) != nil )
| ~ ssItem(U)
| ~ ssList(V) ),
file(unknown,unknown) ).
tff(f_428,axiom,
! [U,V] :
( ~ ssItem(U)
| ~ ssList(V)
| ( hd(cons(U,V)) = U ) ),
file(unknown,unknown) ).
tff(f_62,axiom,
! [U] : ssItem(skaf83(U)),
file(unknown,unknown) ).
tff(f_543,axiom,
! [U] :
( ~ ssList(U)
| ( cons(skaf83(U),skaf82(U)) = U )
| ( nil = U ) ),
file(unknown,unknown) ).
tff(f_1422,axiom,
! [U,V,W,X] :
( ~ frontsegP(cons(U,V),cons(W,X))
| ~ ssList(X)
| ~ ssList(V)
| ~ ssItem(W)
| ~ ssItem(U)
| ( U = W ) ),
file(unknown,unknown) ).
tff(f_132,axiom,
! [U] : ssItem(skaf44(U)),
file(unknown,unknown) ).
tff(f_464,axiom,
! [U] :
( ~ singletonP(U)
| ~ ssList(U)
| ( cons(skaf44(U),nil) = U ) ),
file(unknown,unknown) ).
tff(f_197,axiom,
! [U] :
( ~ ssItem(U)
| equalelemsP(cons(U,nil)) ),
file(unknown,unknown) ).
tff(f_207,axiom,
! [U] :
( ~ ssItem(U)
| strictorderedP(cons(U,nil)) ),
file(unknown,unknown) ).
tff(f_715,axiom,
! [U,V] :
( ~ strictorderedP(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U)
| strictorderedP(V)
| ( nil = V ) ),
file(unknown,unknown) ).
tff(f_624,axiom,
! [U,V] :
( ( cons(U,nil) != V )
| ~ ssItem(U)
| ~ ssList(V)
| singletonP(V) ),
file(unknown,unknown) ).
tff(f_1405,axiom,
! [U,V,W,X] :
( ( app(U,cons(V,W)) != X )
| ~ ssList(W)
| ~ ssList(U)
| ~ ssItem(V)
| ~ ssList(X)
| memberP(X,V) ),
file(unknown,unknown) ).
tff(f_1239,axiom,
! [U,V,W] :
( ~ memberP(cons(U,V),W)
| ~ ssList(V)
| ~ ssItem(U)
| ~ ssItem(W)
| memberP(V,W)
| ( W = U ) ),
file(unknown,unknown) ).
tff(f_233,axiom,
! [U] :
( ~ memberP(nil,U)
| ~ ssItem(U) ),
file(unknown,unknown) ).
tff(f_647,axiom,
! [U,V] :
( ( app(U,V) != nil )
| ~ ssList(V)
| ~ ssList(U)
| ( nil = U ) ),
file(unknown,unknown) ).
tff(f_278,axiom,
! [U] :
( ~ ssList(U)
| ssItem(hd(U))
| ( nil = U ) ),
file(unknown,unknown) ).
tff(f_492,axiom,
! [U] :
( ~ ssList(U)
| ( cons(hd(U),tl(U)) = U )
| ( nil = U ) ),
file(unknown,unknown) ).
tff(f_898,axiom,
! [U,V,W] :
( ( U != V )
| ~ ssList(W)
| ~ ssItem(V)
| ~ ssItem(U)
| memberP(cons(V,W),U) ),
file(unknown,unknown) ).
tff(f_1658,axiom,
( memberP(sk6,sk8)
| memberP(sk7,sk8) ),
file(unknown,unknown) ).
tff(f_702,axiom,
! [U,V] :
( ~ ssList(U)
| ~ ssList(V)
| ( nil = V )
| ( hd(app(V,U)) = hd(V) ) ),
file(unknown,unknown) ).
tff(f_940,axiom,
! [U,V,W] :
( ~ memberP(U,V)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssItem(V)
| memberP(app(W,U),V) ),
file(unknown,unknown) ).
tff(f_1662,axiom,
( memberP(sk6,sk8)
| ~ leq(sk5,sk8) ),
file(unknown,unknown) ).
tff(f_222,axiom,
! [U] :
( ~ ssItem(U)
| totalorderP(cons(U,nil)) ),
file(unknown,unknown) ).
tff(c_392,plain,
ssItem(sk8),
inference(cnfTransformation,[status(thm)],[f_1655]) ).
tff(c_384,plain,
ssItem(sk5),
inference(cnfTransformation,[status(thm)],[f_1651]) ).
tff(c_16,plain,
ssList(nil),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_172,plain,
! [U_82,V_83] :
( ssList(cons(U_82,V_83))
| ~ ssList(V_83)
| ~ ssItem(U_82) ),
inference(cnfTransformation,[status(thm)],[f_342]) ).
tff(c_386,plain,
ssList(sk6),
inference(cnfTransformation,[status(thm)],[f_1652]) ).
tff(c_170,plain,
! [V_81,U_80] :
( ssList(app(V_81,U_80))
| ~ ssList(V_81)
| ~ ssList(U_80) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_388,plain,
ssList(sk7),
inference(cnfTransformation,[status(thm)],[f_1653]) ).
tff(c_448294,plain,
! [U_16866] :
( ( app(U_16866,nil) = U_16866 )
| ~ ssList(U_16866) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_448414,plain,
app(sk7,nil) = sk7,
inference(resolution,[status(thm)],[c_388,c_448294]) ).
tff(c_451378,plain,
! [U_17121,V_17122] :
( rearsegP(app(U_17121,V_17122),V_17122)
| ~ ssList(app(U_17121,V_17122))
| ~ ssList(V_17122)
| ~ ssList(U_17121) ),
inference(cnfTransformation,[status(thm)],[f_961]) ).
tff(c_451521,plain,
( rearsegP(sk7,nil)
| ~ ssList(app(sk7,nil))
| ~ ssList(nil)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_448414,c_451378]) ).
tff(c_451620,plain,
rearsegP(sk7,nil),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_16,c_388,c_448414,c_451521]) ).
tff(c_256,plain,
! [V_155,U_154] :
( ( V_155 = U_154 )
| ~ ssList(V_155)
| ~ ssList(U_154)
| ~ rearsegP(V_155,U_154)
| ~ rearsegP(U_154,V_155) ),
inference(cnfTransformation,[status(thm)],[f_770]) ).
tff(c_451638,plain,
( ( sk7 = nil )
| ~ ssList(sk7)
| ~ ssList(nil)
| ~ rearsegP(nil,sk7) ),
inference(resolution,[status(thm)],[c_451620,c_256]) ).
tff(c_451641,plain,
( ( sk7 = nil )
| ~ rearsegP(nil,sk7) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_388,c_451638]) ).
tff(c_454554,plain,
~ rearsegP(nil,sk7),
inference(splitLeft,[status(thm)],[c_451641]) ).
tff(c_382,plain,
sk3 = sk1,
inference(cnfTransformation,[status(thm)],[f_1650]) ).
tff(c_376,plain,
ssList(sk3),
inference(cnfTransformation,[status(thm)],[f_1647]) ).
tff(c_416,plain,
ssList(sk1),
inference(demodulation,[status(thm),theory(equality)],[c_382,c_376]) ).
tff(c_380,plain,
sk4 = sk2,
inference(cnfTransformation,[status(thm)],[f_1649]) ).
tff(c_402,plain,
( ( sk4 != nil )
| ( sk3 = nil ) ),
inference(cnfTransformation,[status(thm)],[f_1675]) ).
tff(c_409,plain,
( ( sk4 != nil )
| ( sk1 = nil ) ),
inference(demodulation,[status(thm),theory(equality)],[c_382,c_402]) ).
tff(c_413,plain,
( ( sk2 != nil )
| ( sk1 = nil ) ),
inference(demodulation,[status(thm),theory(equality)],[c_380,c_409]) ).
tff(c_463,plain,
sk2 != nil,
inference(splitLeft,[status(thm)],[c_413]) ).
tff(c_378,plain,
ssList(sk4),
inference(cnfTransformation,[status(thm)],[f_1648]) ).
tff(c_415,plain,
ssList(sk2),
inference(demodulation,[status(thm),theory(equality)],[c_380,c_378]) ).
tff(c_2107,plain,
! [V_506,U_507] :
( ( V_506 = U_507 )
| neq(V_506,U_507)
| ~ ssList(V_506)
| ~ ssList(U_507) ),
inference(cnfTransformation,[status(thm)],[f_456]) ).
tff(c_404,plain,
( ~ neq(sk4,nil)
| ssItem(sk9) ),
inference(cnfTransformation,[status(thm)],[f_1679]) ).
tff(c_411,plain,
( ~ neq(sk2,nil)
| ssItem(sk9) ),
inference(demodulation,[status(thm),theory(equality)],[c_380,c_404]) ).
tff(c_477,plain,
~ neq(sk2,nil),
inference(splitLeft,[status(thm)],[c_411]) ).
tff(c_2118,plain,
( ( sk2 = nil )
| ~ ssList(sk2)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_2107,c_477]) ).
tff(c_2125,plain,
sk2 = nil,
inference(demodulation,[status(thm),theory(equality)],[c_16,c_415,c_2118]) ).
tff(c_2127,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_463,c_2125]) ).
tff(c_2128,plain,
ssItem(sk9),
inference(splitRight,[status(thm)],[c_411]) ).
tff(c_2129,plain,
neq(sk2,nil),
inference(splitRight,[status(thm)],[c_411]) ).
tff(c_406,plain,
( ~ neq(sk4,nil)
| ( cons(sk9,nil) = sk3 ) ),
inference(cnfTransformation,[status(thm)],[f_1683]) ).
tff(c_410,plain,
( ~ neq(sk4,nil)
| ( cons(sk9,nil) = sk1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_382,c_406]) ).
tff(c_414,plain,
( ~ neq(sk2,nil)
| ( cons(sk9,nil) = sk1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_380,c_410]) ).
tff(c_257395,plain,
cons(sk9,nil) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_2129,c_414]) ).
tff(c_370513,plain,
! [U_13197,V_13198] :
( ( app(cons(U_13197,nil),V_13198) = cons(U_13197,V_13198) )
| ~ ssList(V_13198)
| ~ ssItem(U_13197) ),
inference(cnfTransformation,[status(thm)],[f_666]) ).
tff(c_370528,plain,
! [V_13198] :
( ( cons(sk9,V_13198) = app(sk1,V_13198) )
| ~ ssList(V_13198)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_370513]) ).
tff(c_383626,plain,
! [V_13954] :
( ( cons(sk9,V_13954) = app(sk1,V_13954) )
| ~ ssList(V_13954) ),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_370528]) ).
tff(c_383765,plain,
cons(sk9,sk1) = app(sk1,sk1),
inference(resolution,[status(thm)],[c_416,c_383626]) ).
tff(c_257435,plain,
! [V_9490,U_9491] :
( ~ ssList(V_9490)
| ~ ssItem(U_9491)
| ( cons(U_9491,V_9490) != V_9490 ) ),
inference(cnfTransformation,[status(thm)],[f_446]) ).
tff(c_369327,plain,
! [U_13097] :
( ~ ssItem(U_13097)
| ( cons(U_13097,sk1) != sk1 ) ),
inference(resolution,[status(thm)],[c_416,c_257435]) ).
tff(c_369392,plain,
cons(sk9,sk1) != sk1,
inference(resolution,[status(thm)],[c_2128,c_369327]) ).
tff(c_384506,plain,
app(sk1,sk1) != sk1,
inference(demodulation,[status(thm),theory(equality)],[c_383765,c_369392]) ).
tff(c_384594,plain,
( ssList(app(sk1,sk1))
| ~ ssList(sk1)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_383765,c_172]) ).
tff(c_384656,plain,
ssList(app(sk1,sk1)),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_416,c_384594]) ).
tff(c_256732,plain,
! [U_9432] :
( ( app(nil,U_9432) = U_9432 )
| ~ ssList(U_9432) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_256858,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[c_416,c_256732]) ).
tff(c_371365,plain,
! [U_13223,V_13224] :
( frontsegP(app(U_13223,V_13224),U_13223)
| ~ ssList(app(U_13223,V_13224))
| ~ ssList(U_13223)
| ~ ssList(V_13224) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_371505,plain,
( frontsegP(sk1,nil)
| ~ ssList(app(nil,sk1))
| ~ ssList(nil)
| ~ ssList(sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_256858,c_371365]) ).
tff(c_371614,plain,
frontsegP(sk1,nil),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_16,c_416,c_256858,c_371505]) ).
tff(c_375114,plain,
! [X_13390,U_13391,V_13392] :
( frontsegP(cons(X_13390,U_13391),cons(X_13390,V_13392))
| ~ ssItem(X_13390)
| ~ ssList(U_13391)
| ~ ssList(V_13392)
| ~ frontsegP(U_13391,V_13392) ),
inference(cnfTransformation,[status(thm)],[f_1460]) ).
tff(c_375148,plain,
! [U_13391] :
( frontsegP(cons(sk9,U_13391),sk1)
| ~ ssItem(sk9)
| ~ ssList(U_13391)
| ~ ssList(nil)
| ~ frontsegP(U_13391,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_375114]) ).
tff(c_406268,plain,
! [U_14640] :
( frontsegP(cons(sk9,U_14640),sk1)
| ~ ssList(U_14640)
| ~ frontsegP(U_14640,nil) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_375148]) ).
tff(c_406344,plain,
( frontsegP(app(sk1,sk1),sk1)
| ~ ssList(sk1)
| ~ frontsegP(sk1,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_383765,c_406268]) ).
tff(c_406410,plain,
frontsegP(app(sk1,sk1),sk1),
inference(demodulation,[status(thm),theory(equality)],[c_371614,c_416,c_406344]) ).
tff(c_258,plain,
! [V_157,U_156] :
( ( V_157 = U_156 )
| ~ ssList(V_157)
| ~ ssList(U_156)
| ~ frontsegP(V_157,U_156)
| ~ frontsegP(U_156,V_157) ),
inference(cnfTransformation,[status(thm)],[f_784]) ).
tff(c_406441,plain,
( ( app(sk1,sk1) = sk1 )
| ~ ssList(app(sk1,sk1))
| ~ ssList(sk1)
| ~ frontsegP(sk1,app(sk1,sk1)) ),
inference(resolution,[status(thm)],[c_406410,c_258]) ).
tff(c_406450,plain,
( ( app(sk1,sk1) = sk1 )
| ~ frontsegP(sk1,app(sk1,sk1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_384656,c_406441]) ).
tff(c_406451,plain,
~ frontsegP(sk1,app(sk1,sk1)),
inference(negUnitSimplification,[status(thm)],[c_384506,c_406450]) ).
tff(c_240,plain,
! [U_138,V_139] :
( ( app(cons(U_138,nil),V_139) = cons(U_138,V_139) )
| ~ ssList(V_139)
| ~ ssItem(U_138) ),
inference(cnfTransformation,[status(thm)],[f_666]) ).
tff(c_390,plain,
app(app(sk6,cons(sk5,nil)),sk7) = sk1,
inference(cnfTransformation,[status(thm)],[f_1654]) ).
tff(c_376519,plain,
! [U_13438,V_13439,W_13440] :
( segmentP(app(app(U_13438,V_13439),W_13440),V_13439)
| ~ ssList(app(app(U_13438,V_13439),W_13440))
| ~ ssList(V_13439)
| ~ ssList(U_13438)
| ~ ssList(W_13440) ),
inference(cnfTransformation,[status(thm)],[f_1371]) ).
tff(c_376620,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_376519]) ).
tff(c_376776,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_416,c_390,c_376620]) ).
tff(c_393875,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_376776]) ).
tff(c_393878,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_393875]) ).
tff(c_393882,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_393878]) ).
tff(c_393884,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_376776]) ).
tff(c_298,plain,
! [W_208,V_207,U_206] :
( ( app(app(W_208,V_207),U_206) = app(W_208,app(V_207,U_206)) )
| ~ ssList(W_208)
| ~ ssList(V_207)
| ~ ssList(U_206) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_124,plain,
! [U_56] :
( leq(U_56,U_56)
| ~ ssItem(U_56) ),
inference(cnfTransformation,[status(thm)],[f_186]) ).
tff(c_256593,plain,
! [U_9423] :
( ( app(U_9423,nil) = U_9423 )
| ~ ssList(U_9423) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_256717,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[c_16,c_256593]) ).
tff(c_260016,plain,
! [U_9671,V_9672] :
( frontsegP(app(U_9671,V_9672),U_9671)
| ~ ssList(app(U_9671,V_9672))
| ~ ssList(U_9671)
| ~ ssList(V_9672) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_260150,plain,
( frontsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_256717,c_260016]) ).
tff(c_260237,plain,
frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_256717,c_260150]) ).
tff(c_26,plain,
! [U_2] : ssList(skaf82(U_2)),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_258463,plain,
! [U_9556,V_9557] :
( ( tl(cons(U_9556,V_9557)) = V_9557 )
| ~ ssList(V_9557)
| ~ ssItem(U_9556) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_258478,plain,
( ( tl(sk1) = nil )
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_258463]) ).
tff(c_258484,plain,
tl(sk1) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_16,c_258478]) ).
tff(c_257182,plain,
! [V_9484,U_9485] :
( ~ ssList(V_9484)
| ~ ssItem(U_9485)
| ( cons(U_9485,V_9484) != nil ) ),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_257309,plain,
! [U_9489] :
( ~ ssItem(U_9489)
| ( cons(U_9489,nil) != nil ) ),
inference(resolution,[status(thm)],[c_16,c_257182]) ).
tff(c_257374,plain,
cons(sk9,nil) != nil,
inference(resolution,[status(thm)],[c_2128,c_257309]) ).
tff(c_257559,plain,
sk1 != nil,
inference(demodulation,[status(thm),theory(equality)],[c_257395,c_257374]) ).
tff(c_258102,plain,
! [U_9539,V_9540] :
( ( hd(cons(U_9539,V_9540)) = U_9539 )
| ~ ssList(V_9540)
| ~ ssItem(U_9539) ),
inference(cnfTransformation,[status(thm)],[f_428]) ).
tff(c_258117,plain,
( ( hd(sk1) = sk9 )
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_258102]) ).
tff(c_258123,plain,
hd(sk1) = sk9,
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_16,c_258117]) ).
tff(c_24,plain,
! [U_1] : ssItem(skaf83(U_1)),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_258849,plain,
! [U_9608] :
( ( nil = U_9608 )
| ( cons(skaf83(U_9608),skaf82(U_9608)) = U_9608 )
| ~ ssList(U_9608) ),
inference(cnfTransformation,[status(thm)],[f_543]) ).
tff(c_194,plain,
! [U_95,V_96] :
( ( hd(cons(U_95,V_96)) = U_95 )
| ~ ssList(V_96)
| ~ ssItem(U_95) ),
inference(cnfTransformation,[status(thm)],[f_428]) ).
tff(c_258861,plain,
! [U_9608] :
( ( skaf83(U_9608) = hd(U_9608) )
| ~ ssList(skaf82(U_9608))
| ~ ssItem(skaf83(U_9608))
| ( nil = U_9608 )
| ~ ssList(U_9608) ),
inference(superposition,[status(thm),theory(equality)],[c_258849,c_194]) ).
tff(c_268087,plain,
! [U_10151] :
( ( skaf83(U_10151) = hd(U_10151) )
| ( nil = U_10151 )
| ~ ssList(U_10151) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_26,c_258861]) ).
tff(c_268186,plain,
( ( skaf83(sk1) = hd(sk1) )
| ( sk1 = nil ) ),
inference(resolution,[status(thm)],[c_416,c_268087]) ).
tff(c_268227,plain,
( ( skaf83(sk1) = sk9 )
| ( sk1 = nil ) ),
inference(demodulation,[status(thm),theory(equality)],[c_258123,c_268186]) ).
tff(c_268228,plain,
skaf83(sk1) = sk9,
inference(negUnitSimplification,[status(thm)],[c_257559,c_268227]) ).
tff(c_218,plain,
! [U_117] :
( ( nil = U_117 )
| ( cons(skaf83(U_117),skaf82(U_117)) = U_117 )
| ~ ssList(U_117) ),
inference(cnfTransformation,[status(thm)],[f_543]) ).
tff(c_268246,plain,
( ( sk1 = nil )
| ( cons(sk9,skaf82(sk1)) = sk1 )
| ~ ssList(sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_268228,c_218]) ).
tff(c_268260,plain,
( ( sk1 = nil )
| ( cons(sk9,skaf82(sk1)) = sk1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_268246]) ).
tff(c_268261,plain,
cons(sk9,skaf82(sk1)) = sk1,
inference(negUnitSimplification,[status(thm)],[c_257559,c_268260]) ).
tff(c_192,plain,
! [U_93,V_94] :
( ( tl(cons(U_93,V_94)) = V_94 )
| ~ ssList(V_94)
| ~ ssItem(U_93) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_268767,plain,
( ( tl(sk1) = skaf82(sk1) )
| ~ ssList(skaf82(sk1))
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_268261,c_192]) ).
tff(c_268830,plain,
skaf82(sk1) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_26,c_258484,c_268767]) ).
tff(c_259777,plain,
! [U_9669,V_9670] :
( rearsegP(app(U_9669,V_9670),V_9670)
| ~ ssList(app(U_9669,V_9670))
| ~ ssList(V_9670)
| ~ ssList(U_9669) ),
inference(cnfTransformation,[status(thm)],[f_961]) ).
tff(c_259911,plain,
( rearsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_256717,c_259777]) ).
tff(c_259998,plain,
rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_256717,c_259911]) ).
tff(c_268225,plain,
( ( skaf83(sk6) = hd(sk6) )
| ( sk6 = nil ) ),
inference(resolution,[status(thm)],[c_386,c_268087]) ).
tff(c_268331,plain,
sk6 = nil,
inference(splitLeft,[status(thm)],[c_268225]) ).
tff(c_256718,plain,
app(sk6,nil) = sk6,
inference(resolution,[status(thm)],[c_386,c_256593]) ).
tff(c_259896,plain,
( rearsegP(sk6,nil)
| ~ ssList(app(sk6,nil))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_256718,c_259777]) ).
tff(c_259988,plain,
rearsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_256718,c_259896]) ).
tff(c_260239,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ rearsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_259988,c_256]) ).
tff(c_260242,plain,
( ( sk6 = nil )
| ~ rearsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_260239]) ).
tff(c_263462,plain,
~ rearsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_260242]) ).
tff(c_268335,plain,
~ rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_268331,c_263462]) ).
tff(c_268396,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_259998,c_268335]) ).
tff(c_268397,plain,
skaf83(sk6) = hd(sk6),
inference(splitRight,[status(thm)],[c_268225]) ).
tff(c_268422,plain,
ssItem(hd(sk6)),
inference(superposition,[status(thm),theory(equality)],[c_268397,c_24]) ).
tff(c_268398,plain,
sk6 != nil,
inference(splitRight,[status(thm)],[c_268225]) ).
tff(c_268412,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),skaf82(sk6)) = sk6 )
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_268397,c_218]) ).
tff(c_268426,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),skaf82(sk6)) = sk6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_268412]) ).
tff(c_268427,plain,
cons(hd(sk6),skaf82(sk6)) = sk6,
inference(negUnitSimplification,[status(thm)],[c_268398,c_268426]) ).
tff(c_264239,plain,
! [W_9861,U_9862,V_9863,X_9864] :
( ( W_9861 = U_9862 )
| ~ ssItem(U_9862)
| ~ ssItem(W_9861)
| ~ ssList(V_9863)
| ~ ssList(X_9864)
| ~ frontsegP(cons(U_9862,V_9863),cons(W_9861,X_9864)) ),
inference(cnfTransformation,[status(thm)],[f_1422]) ).
tff(c_264269,plain,
! [W_9861,X_9864] :
( ( sk9 = W_9861 )
| ~ ssItem(sk9)
| ~ ssItem(W_9861)
| ~ ssList(nil)
| ~ ssList(X_9864)
| ~ frontsegP(sk1,cons(W_9861,X_9864)) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_264239]) ).
tff(c_316588,plain,
! [W_11514,X_11515] :
( ( sk9 = W_11514 )
| ~ ssItem(W_11514)
| ~ ssList(X_11515)
| ~ frontsegP(sk1,cons(W_11514,X_11515)) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_264269]) ).
tff(c_316672,plain,
( ( hd(sk6) = sk9 )
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6))
| ~ frontsegP(sk1,sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_268427,c_316588]) ).
tff(c_316774,plain,
( ( hd(sk6) = sk9 )
| ~ frontsegP(sk1,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_268422,c_316672]) ).
tff(c_316793,plain,
~ frontsegP(sk1,sk6),
inference(splitLeft,[status(thm)],[c_316774]) ).
tff(c_265776,plain,
! [U_9915,V_9916,W_9917] :
( segmentP(app(app(U_9915,V_9916),W_9917),V_9916)
| ~ ssList(app(app(U_9915,V_9916),W_9917))
| ~ ssList(V_9916)
| ~ ssList(U_9915)
| ~ ssList(W_9917) ),
inference(cnfTransformation,[status(thm)],[f_1371]) ).
tff(c_265889,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_265776]) ).
tff(c_266049,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_416,c_390,c_265889]) ).
tff(c_273419,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_266049]) ).
tff(c_273422,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_273419]) ).
tff(c_273426,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_273422]) ).
tff(c_273428,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_266049]) ).
tff(c_262630,plain,
! [W_9801,V_9802,U_9803] :
( ( app(app(W_9801,V_9802),U_9803) = app(W_9801,app(V_9802,U_9803)) )
| ~ ssList(W_9801)
| ~ ssList(V_9802)
| ~ ssList(U_9803) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_262667,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_262630,c_390]) ).
tff(c_262826,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_262667]) ).
tff(c_329373,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_273428,c_262826]) ).
tff(c_329432,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_329373]) ).
tff(c_329472,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_329432]) ).
tff(c_288,plain,
! [U_192,V_193] :
( frontsegP(app(U_192,V_193),U_192)
| ~ ssList(app(U_192,V_193))
| ~ ssList(U_192)
| ~ ssList(V_193) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_329539,plain,
( frontsegP(sk1,sk6)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_329472,c_288]) ).
tff(c_329592,plain,
( frontsegP(sk1,sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_416,c_329472,c_329539]) ).
tff(c_329593,plain,
~ ssList(cons(sk5,sk7)),
inference(negUnitSimplification,[status(thm)],[c_316793,c_329592]) ).
tff(c_329610,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_329593]) ).
tff(c_329614,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_329610]) ).
tff(c_329616,plain,
frontsegP(sk1,sk6),
inference(splitRight,[status(thm)],[c_316774]) ).
tff(c_256855,plain,
! [U_2] : ( app(nil,skaf82(U_2)) = skaf82(U_2) ),
inference(resolution,[status(thm)],[c_26,c_256732]) ).
tff(c_260024,plain,
! [U_2] :
( frontsegP(skaf82(U_2),nil)
| ~ ssList(app(nil,skaf82(U_2)))
| ~ ssList(nil)
| ~ ssList(skaf82(U_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_256855,c_260016]) ).
tff(c_260155,plain,
! [U_2] : frontsegP(skaf82(U_2),nil),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_16,c_26,c_256855,c_260024]) ).
tff(c_329615,plain,
hd(sk6) = sk9,
inference(splitRight,[status(thm)],[c_316774]) ).
tff(c_329678,plain,
cons(sk9,skaf82(sk6)) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_329615,c_268427]) ).
tff(c_262971,plain,
! [X_9809,U_9810,V_9811] :
( frontsegP(cons(X_9809,U_9810),cons(X_9809,V_9811))
| ~ ssItem(X_9809)
| ~ ssList(U_9810)
| ~ ssList(V_9811)
| ~ frontsegP(U_9810,V_9811) ),
inference(cnfTransformation,[status(thm)],[f_1460]) ).
tff(c_262999,plain,
! [U_9810] :
( frontsegP(cons(sk9,U_9810),sk1)
| ~ ssItem(sk9)
| ~ ssList(U_9810)
| ~ ssList(nil)
| ~ frontsegP(U_9810,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_262971]) ).
tff(c_263013,plain,
! [U_9810] :
( frontsegP(cons(sk9,U_9810),sk1)
| ~ ssList(U_9810)
| ~ frontsegP(U_9810,nil) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_262999]) ).
tff(c_329828,plain,
( frontsegP(sk6,sk1)
| ~ ssList(skaf82(sk6))
| ~ frontsegP(skaf82(sk6),nil) ),
inference(superposition,[status(thm),theory(equality)],[c_329678,c_263013]) ).
tff(c_329937,plain,
frontsegP(sk6,sk1),
inference(demodulation,[status(thm),theory(equality)],[c_260155,c_26,c_329828]) ).
tff(c_330207,plain,
( ( sk6 = sk1 )
| ~ ssList(sk6)
| ~ ssList(sk1)
| ~ frontsegP(sk1,sk6) ),
inference(resolution,[status(thm)],[c_329937,c_258]) ).
tff(c_330216,plain,
sk6 = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_329616,c_416,c_386,c_330207]) ).
tff(c_94,plain,
! [U_36] : ssItem(skaf44(U_36)),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_257915,plain,
! [U_9511] :
( ( cons(skaf44(U_9511),nil) = U_9511 )
| ~ ssList(U_9511)
| ~ singletonP(U_9511) ),
inference(cnfTransformation,[status(thm)],[f_464]) ).
tff(c_128,plain,
! [U_58] :
( equalelemsP(cons(U_58,nil))
| ~ ssItem(U_58) ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_257938,plain,
! [U_9511] :
( equalelemsP(U_9511)
| ~ ssItem(skaf44(U_9511))
| ~ ssList(U_9511)
| ~ singletonP(U_9511) ),
inference(superposition,[status(thm),theory(equality)],[c_257915,c_128]) ).
tff(c_258192,plain,
! [U_9547] :
( equalelemsP(U_9547)
| ~ ssList(U_9547)
| ~ singletonP(U_9547) ),
inference(demodulation,[status(thm),theory(equality)],[c_94,c_257938]) ).
tff(c_258330,plain,
( equalelemsP(sk6)
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_258192]) ).
tff(c_258335,plain,
~ singletonP(sk6),
inference(splitLeft,[status(thm)],[c_258330]) ).
tff(c_132,plain,
! [U_60] :
( strictorderedP(cons(U_60,nil))
| ~ ssItem(U_60) ),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_257417,plain,
( strictorderedP(sk1)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_132]) ).
tff(c_257433,plain,
strictorderedP(sk1),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_257417]) ).
tff(c_264272,plain,
! [U_9862,V_9863] :
( ( sk9 = U_9862 )
| ~ ssItem(U_9862)
| ~ ssItem(sk9)
| ~ ssList(V_9863)
| ~ ssList(nil)
| ~ frontsegP(cons(U_9862,V_9863),sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_264239]) ).
tff(c_296093,plain,
! [U_11122,V_11123] :
( ( sk9 = U_11122 )
| ~ ssItem(U_11122)
| ~ ssList(V_11123)
| ~ frontsegP(cons(U_11122,V_11123),sk1) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_264272]) ).
tff(c_296174,plain,
( ( hd(sk6) = sk9 )
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6))
| ~ frontsegP(sk6,sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_268427,c_296093]) ).
tff(c_296276,plain,
( ( hd(sk6) = sk9 )
| ~ frontsegP(sk6,sk1) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_268422,c_296174]) ).
tff(c_297879,plain,
~ frontsegP(sk6,sk1),
inference(splitLeft,[status(thm)],[c_296276]) ).
tff(c_297017,plain,
! [W_11132,X_11133] :
( ( sk9 = W_11132 )
| ~ ssItem(W_11132)
| ~ ssList(X_11133)
| ~ frontsegP(sk1,cons(W_11132,X_11133)) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_264269]) ).
tff(c_297101,plain,
( ( hd(sk6) = sk9 )
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6))
| ~ frontsegP(sk1,sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_268427,c_297017]) ).
tff(c_297203,plain,
( ( hd(sk6) = sk9 )
| ~ frontsegP(sk1,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_268422,c_297101]) ).
tff(c_297981,plain,
~ frontsegP(sk1,sk6),
inference(splitLeft,[status(thm)],[c_297203]) ).
tff(c_262719,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_262630]) ).
tff(c_262853,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_262719]) ).
tff(c_301115,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_273428,c_262853]) ).
tff(c_301165,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_301115]) ).
tff(c_301199,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_301165]) ).
tff(c_301257,plain,
( frontsegP(sk1,sk6)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_301199,c_288]) ).
tff(c_301304,plain,
( frontsegP(sk1,sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_416,c_301199,c_301257]) ).
tff(c_301305,plain,
~ ssList(cons(sk5,sk7)),
inference(negUnitSimplification,[status(thm)],[c_297981,c_301304]) ).
tff(c_301322,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_301305]) ).
tff(c_301326,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_301322]) ).
tff(c_301327,plain,
hd(sk6) = sk9,
inference(splitRight,[status(thm)],[c_297203]) ).
tff(c_301434,plain,
cons(sk9,skaf82(sk6)) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_301327,c_268427]) ).
tff(c_301581,plain,
( frontsegP(sk6,sk1)
| ~ ssList(skaf82(sk6))
| ~ frontsegP(skaf82(sk6),nil) ),
inference(superposition,[status(thm),theory(equality)],[c_301434,c_263013]) ).
tff(c_301693,plain,
frontsegP(sk6,sk1),
inference(demodulation,[status(thm),theory(equality)],[c_260155,c_26,c_301581]) ).
tff(c_301695,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_297879,c_301693]) ).
tff(c_301697,plain,
frontsegP(sk6,sk1),
inference(splitRight,[status(thm)],[c_296276]) ).
tff(c_302471,plain,
( ( sk6 = sk1 )
| ~ ssList(sk6)
| ~ ssList(sk1)
| ~ frontsegP(sk1,sk6) ),
inference(resolution,[status(thm)],[c_301697,c_258]) ).
tff(c_302480,plain,
( ( sk6 = sk1 )
| ~ frontsegP(sk1,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_386,c_302471]) ).
tff(c_302807,plain,
~ frontsegP(sk1,sk6),
inference(splitLeft,[status(thm)],[c_302480]) ).
tff(c_307263,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_273428,c_262853]) ).
tff(c_307316,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_307263]) ).
tff(c_307352,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_307316]) ).
tff(c_307413,plain,
( frontsegP(sk1,sk6)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_307352,c_288]) ).
tff(c_307462,plain,
( frontsegP(sk1,sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_416,c_307352,c_307413]) ).
tff(c_307463,plain,
~ ssList(cons(sk5,sk7)),
inference(negUnitSimplification,[status(thm)],[c_302807,c_307462]) ).
tff(c_307480,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_307463]) ).
tff(c_307484,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_307480]) ).
tff(c_307485,plain,
sk6 = sk1,
inference(splitRight,[status(thm)],[c_302480]) ).
tff(c_248,plain,
! [V_147,U_146] :
( ( nil = V_147 )
| strictorderedP(V_147)
| ~ ssItem(U_146)
| ~ ssList(V_147)
| ~ strictorderedP(cons(U_146,V_147)) ),
inference(cnfTransformation,[status(thm)],[f_715]) ).
tff(c_269615,plain,
( ( skaf82(sk6) = nil )
| strictorderedP(skaf82(sk6))
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6))
| ~ strictorderedP(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_268427,c_248]) ).
tff(c_269679,plain,
( ( skaf82(sk6) = nil )
| strictorderedP(skaf82(sk6))
| ~ strictorderedP(sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_268422,c_269615]) ).
tff(c_286362,plain,
~ strictorderedP(sk6),
inference(splitLeft,[status(thm)],[c_269679]) ).
tff(c_307590,plain,
~ strictorderedP(sk1),
inference(demodulation,[status(thm),theory(equality)],[c_307485,c_286362]) ).
tff(c_307766,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_257433,c_307590]) ).
tff(c_307767,plain,
( strictorderedP(skaf82(sk6))
| ( skaf82(sk6) = nil ) ),
inference(splitRight,[status(thm)],[c_269679]) ).
tff(c_307769,plain,
skaf82(sk6) = nil,
inference(splitLeft,[status(thm)],[c_307767]) ).
tff(c_307772,plain,
cons(hd(sk6),nil) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_307769,c_268427]) ).
tff(c_258744,plain,
! [U_9605] :
( singletonP(cons(U_9605,nil))
| ~ ssList(cons(U_9605,nil))
| ~ ssItem(U_9605) ),
inference(cnfTransformation,[status(thm)],[f_624]) ).
tff(c_258751,plain,
! [U_82] :
( singletonP(cons(U_82,nil))
| ~ ssList(nil)
| ~ ssItem(U_82) ),
inference(resolution,[status(thm)],[c_172,c_258744]) ).
tff(c_258759,plain,
! [U_82] :
( singletonP(cons(U_82,nil))
| ~ ssItem(U_82) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_258751]) ).
tff(c_308020,plain,
( singletonP(sk6)
| ~ ssItem(hd(sk6)) ),
inference(superposition,[status(thm),theory(equality)],[c_307772,c_258759]) ).
tff(c_308121,plain,
singletonP(sk6),
inference(demodulation,[status(thm),theory(equality)],[c_268422,c_308020]) ).
tff(c_308123,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_258335,c_308121]) ).
tff(c_308125,plain,
skaf82(sk6) != nil,
inference(splitRight,[status(thm)],[c_307767]) ).
tff(c_330233,plain,
skaf82(sk1) != nil,
inference(demodulation,[status(thm),theory(equality)],[c_330216,c_308125]) ).
tff(c_330411,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_268830,c_330233]) ).
tff(c_330412,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_260242]) ).
tff(c_256857,plain,
app(nil,sk6) = sk6,
inference(resolution,[status(thm)],[c_386,c_256732]) ).
tff(c_260126,plain,
( frontsegP(sk6,nil)
| ~ ssList(app(nil,sk6))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_256857,c_260016]) ).
tff(c_260221,plain,
frontsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_256857,c_260126]) ).
tff(c_260382,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ frontsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_260221,c_258]) ).
tff(c_260385,plain,
( ( sk6 = nil )
| ~ frontsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_260382]) ).
tff(c_263322,plain,
~ frontsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_260385]) ).
tff(c_330414,plain,
~ frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_330412,c_263322]) ).
tff(c_330471,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_260237,c_330414]) ).
tff(c_330472,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_260385]) ).
tff(c_368320,plain,
( ( app(nil,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_330472,c_262853]) ).
tff(c_368321,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_368320]) ).
tff(c_368324,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_368321]) ).
tff(c_368328,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_368324]) ).
tff(c_368330,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_368320]) ).
tff(c_148,plain,
! [U_69] :
( ( app(nil,U_69) = U_69 )
| ~ ssList(U_69) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_368442,plain,
app(nil,cons(sk5,nil)) = cons(sk5,nil),
inference(resolution,[status(thm)],[c_368330,c_148]) ).
tff(c_259809,plain,
( rearsegP(sk1,sk7)
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_259777]) ).
tff(c_259930,plain,
( rearsegP(sk1,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_416,c_390,c_259809]) ).
tff(c_348206,plain,
( rearsegP(sk1,sk7)
| ~ ssList(app(nil,cons(sk5,nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_330472,c_259930]) ).
tff(c_348207,plain,
~ ssList(app(nil,cons(sk5,nil))),
inference(splitLeft,[status(thm)],[c_348206]) ).
tff(c_348210,plain,
( ~ ssList(nil)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[c_170,c_348207]) ).
tff(c_348213,plain,
~ ssList(cons(sk5,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_348210]) ).
tff(c_348216,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_348213]) ).
tff(c_348220,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_348216]) ).
tff(c_348222,plain,
ssList(app(nil,cons(sk5,nil))),
inference(splitRight,[status(thm)],[c_348206]) ).
tff(c_330628,plain,
app(app(nil,cons(sk5,nil)),sk7) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_330472,c_390]) ).
tff(c_348526,plain,
( frontsegP(sk1,app(nil,cons(sk5,nil)))
| ~ ssList(app(app(nil,cons(sk5,nil)),sk7))
| ~ ssList(app(nil,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_330628,c_288]) ).
tff(c_348568,plain,
frontsegP(sk1,app(nil,cons(sk5,nil))),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_348222,c_416,c_330628,c_348526]) ).
tff(c_368660,plain,
frontsegP(sk1,cons(sk5,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_368442,c_348568]) ).
tff(c_159588,plain,
cons(sk9,nil) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_2129,c_414]) ).
tff(c_209273,plain,
! [U_7778,V_7779] :
( ( app(cons(U_7778,nil),V_7779) = cons(U_7778,V_7779) )
| ~ ssList(V_7779)
| ~ ssItem(U_7778) ),
inference(cnfTransformation,[status(thm)],[f_666]) ).
tff(c_209288,plain,
! [V_7779] :
( ( cons(sk9,V_7779) = app(sk1,V_7779) )
| ~ ssList(V_7779)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_209273]) ).
tff(c_222426,plain,
! [V_8552] :
( ( cons(sk9,V_8552) = app(sk1,V_8552) )
| ~ ssList(V_8552) ),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_209288]) ).
tff(c_222565,plain,
cons(sk9,sk1) = app(sk1,sk1),
inference(resolution,[status(thm)],[c_416,c_222426]) ).
tff(c_159910,plain,
! [V_5840,U_5841] :
( ~ ssList(V_5840)
| ~ ssItem(U_5841)
| ( cons(U_5841,V_5840) != V_5840 ) ),
inference(cnfTransformation,[status(thm)],[f_446]) ).
tff(c_209161,plain,
! [U_7766] :
( ~ ssItem(U_7766)
| ( cons(U_7766,sk1) != sk1 ) ),
inference(resolution,[status(thm)],[c_416,c_159910]) ).
tff(c_209226,plain,
cons(sk9,sk1) != sk1,
inference(resolution,[status(thm)],[c_2128,c_209161]) ).
tff(c_223693,plain,
app(sk1,sk1) != sk1,
inference(demodulation,[status(thm),theory(equality)],[c_222565,c_209226]) ).
tff(c_223782,plain,
( ssList(app(sk1,sk1))
| ~ ssList(sk1)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_222565,c_172]) ).
tff(c_223844,plain,
ssList(app(sk1,sk1)),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_416,c_223782]) ).
tff(c_159150,plain,
! [U_5774] :
( ( app(nil,U_5774) = U_5774 )
| ~ ssList(U_5774) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_159276,plain,
app(nil,sk1) = sk1,
inference(resolution,[status(thm)],[c_416,c_159150]) ).
tff(c_210245,plain,
! [U_7822,V_7823] :
( frontsegP(app(U_7822,V_7823),U_7822)
| ~ ssList(app(U_7822,V_7823))
| ~ ssList(U_7822)
| ~ ssList(V_7823) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_210397,plain,
( frontsegP(sk1,nil)
| ~ ssList(app(nil,sk1))
| ~ ssList(nil)
| ~ ssList(sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_159276,c_210245]) ).
tff(c_210502,plain,
frontsegP(sk1,nil),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_16,c_416,c_159276,c_210397]) ).
tff(c_214158,plain,
! [X_7980,U_7981,V_7982] :
( frontsegP(cons(X_7980,U_7981),cons(X_7980,V_7982))
| ~ ssItem(X_7980)
| ~ ssList(U_7981)
| ~ ssList(V_7982)
| ~ frontsegP(U_7981,V_7982) ),
inference(cnfTransformation,[status(thm)],[f_1460]) ).
tff(c_214192,plain,
! [U_7981] :
( frontsegP(cons(sk9,U_7981),sk1)
| ~ ssItem(sk9)
| ~ ssList(U_7981)
| ~ ssList(nil)
| ~ frontsegP(U_7981,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_214158]) ).
tff(c_245351,plain,
! [U_9271] :
( frontsegP(cons(sk9,U_9271),sk1)
| ~ ssList(U_9271)
| ~ frontsegP(U_9271,nil) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_214192]) ).
tff(c_245427,plain,
( frontsegP(app(sk1,sk1),sk1)
| ~ ssList(sk1)
| ~ frontsegP(sk1,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_222565,c_245351]) ).
tff(c_245493,plain,
frontsegP(app(sk1,sk1),sk1),
inference(demodulation,[status(thm),theory(equality)],[c_210502,c_416,c_245427]) ).
tff(c_245524,plain,
( ( app(sk1,sk1) = sk1 )
| ~ ssList(app(sk1,sk1))
| ~ ssList(sk1)
| ~ frontsegP(sk1,app(sk1,sk1)) ),
inference(resolution,[status(thm)],[c_245493,c_258]) ).
tff(c_245533,plain,
( ( app(sk1,sk1) = sk1 )
| ~ frontsegP(sk1,app(sk1,sk1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_223844,c_245524]) ).
tff(c_245534,plain,
~ frontsegP(sk1,app(sk1,sk1)),
inference(negUnitSimplification,[status(thm)],[c_223693,c_245533]) ).
tff(c_215422,plain,
! [U_8037,V_8038,W_8039] :
( segmentP(app(app(U_8037,V_8038),W_8039),V_8038)
| ~ ssList(app(app(U_8037,V_8038),W_8039))
| ~ ssList(V_8038)
| ~ ssList(U_8037)
| ~ ssList(W_8039) ),
inference(cnfTransformation,[status(thm)],[f_1371]) ).
tff(c_215520,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_215422]) ).
tff(c_215676,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_416,c_390,c_215520]) ).
tff(c_233076,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_215676]) ).
tff(c_233079,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_233076]) ).
tff(c_233083,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_233079]) ).
tff(c_233085,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_215676]) ).
tff(c_213684,plain,
! [W_7971,V_7972,U_7973] :
( ( app(app(W_7971,V_7972),U_7973) = app(W_7971,app(V_7972,U_7973)) )
| ~ ssList(W_7971)
| ~ ssList(V_7972)
| ~ ssList(U_7973) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_213724,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_213684,c_390]) ).
tff(c_213907,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_213724]) ).
tff(c_248642,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_233085,c_213907]) ).
tff(c_248692,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_248642]) ).
tff(c_248725,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_248692]) ).
tff(c_350,plain,
! [U_273,V_274,W_275] :
( memberP(app(U_273,cons(V_274,W_275)),V_274)
| ~ ssList(app(U_273,cons(V_274,W_275)))
| ~ ssItem(V_274)
| ~ ssList(U_273)
| ~ ssList(W_275) ),
inference(cnfTransformation,[status(thm)],[f_1405]) ).
tff(c_248753,plain,
( memberP(sk1,sk5)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssItem(sk5)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_248725,c_350]) ).
tff(c_248810,plain,
memberP(sk1,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_384,c_416,c_248725,c_248753]) ).
tff(c_214127,plain,
! [W_7977,U_7978,V_7979] :
( ( W_7977 = U_7978 )
| memberP(V_7979,W_7977)
| ~ ssItem(W_7977)
| ~ ssItem(U_7978)
| ~ ssList(V_7979)
| ~ memberP(cons(U_7978,V_7979),W_7977) ),
inference(cnfTransformation,[status(thm)],[f_1239]) ).
tff(c_214148,plain,
! [W_7977] :
( ( sk9 = W_7977 )
| memberP(nil,W_7977)
| ~ ssItem(W_7977)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk1,W_7977) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_214127]) ).
tff(c_214157,plain,
! [W_7977] :
( ( sk9 = W_7977 )
| memberP(nil,W_7977)
| ~ ssItem(W_7977)
| ~ memberP(sk1,W_7977) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_214148]) ).
tff(c_248841,plain,
( ( sk9 = sk5 )
| memberP(nil,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_248810,c_214157]) ).
tff(c_248844,plain,
( ( sk9 = sk5 )
| memberP(nil,sk5) ),
inference(demodulation,[status(thm),theory(equality)],[c_384,c_248841]) ).
tff(c_248845,plain,
memberP(nil,sk5),
inference(splitLeft,[status(thm)],[c_248844]) ).
tff(c_142,plain,
! [U_65] :
( ~ ssItem(U_65)
| ~ memberP(nil,U_65) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_248932,plain,
~ ssItem(sk5),
inference(resolution,[status(thm)],[c_248845,c_142]) ).
tff(c_248936,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_248932]) ).
tff(c_248937,plain,
sk9 = sk5,
inference(splitRight,[status(thm)],[c_248844]) ).
tff(c_249029,plain,
cons(sk5,nil) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_248937,c_159588]) ).
tff(c_2277,plain,
! [U_524] :
( ( app(U_524,nil) = U_524 )
| ~ ssList(U_524) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_2401,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[c_16,c_2277]) ).
tff(c_162285,plain,
! [U_6022,V_6023] :
( rearsegP(app(U_6022,V_6023),V_6023)
| ~ ssList(app(U_6022,V_6023))
| ~ ssList(V_6023)
| ~ ssList(U_6022) ),
inference(cnfTransformation,[status(thm)],[f_961]) ).
tff(c_162428,plain,
( rearsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_2401,c_162285]) ).
tff(c_162521,plain,
rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_2401,c_162428]) ).
tff(c_162550,plain,
! [U_6024,V_6025] :
( frontsegP(app(U_6024,V_6025),U_6024)
| ~ ssList(app(U_6024,V_6025))
| ~ ssList(U_6024)
| ~ ssList(V_6025) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_162693,plain,
( frontsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_2401,c_162550]) ).
tff(c_162786,plain,
frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_2401,c_162693]) ).
tff(c_161497,plain,
! [U_5957] :
( singletonP(cons(U_5957,nil))
| ~ ssList(cons(U_5957,nil))
| ~ ssItem(U_5957) ),
inference(cnfTransformation,[status(thm)],[f_624]) ).
tff(c_161507,plain,
( singletonP(cons(sk9,nil))
| ~ ssList(sk1)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_161497]) ).
tff(c_161514,plain,
singletonP(sk1),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_416,c_159588,c_161507]) ).
tff(c_2402,plain,
app(sk6,nil) = sk6,
inference(resolution,[status(thm)],[c_386,c_2277]) ).
tff(c_161075,plain,
! [U_5930,V_5931] :
( ( nil = U_5930 )
| ~ ssList(U_5930)
| ~ ssList(V_5931)
| ( app(U_5930,V_5931) != nil ) ),
inference(cnfTransformation,[status(thm)],[f_647]) ).
tff(c_161178,plain,
! [V_5931] :
( ( sk6 = nil )
| ~ ssList(V_5931)
| ( app(sk6,V_5931) != nil ) ),
inference(resolution,[status(thm)],[c_386,c_161075]) ).
tff(c_170377,plain,
! [V_6495] :
( ~ ssList(V_6495)
| ( app(sk6,V_6495) != nil ) ),
inference(splitLeft,[status(thm)],[c_161178]) ).
tff(c_170470,plain,
app(sk6,nil) != nil,
inference(resolution,[status(thm)],[c_16,c_170377]) ).
tff(c_170514,plain,
sk6 != nil,
inference(demodulation,[status(thm),theory(equality)],[c_2402,c_170470]) ).
tff(c_156,plain,
! [U_73] :
( ( nil = U_73 )
| ssItem(hd(U_73))
| ~ ssList(U_73) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_161464,plain,
! [U_5952] :
( ( nil = U_5952 )
| ( cons(skaf83(U_5952),skaf82(U_5952)) = U_5952 )
| ~ ssList(U_5952) ),
inference(cnfTransformation,[status(thm)],[f_543]) ).
tff(c_161476,plain,
! [U_5952] :
( ( tl(U_5952) = skaf82(U_5952) )
| ~ ssList(skaf82(U_5952))
| ~ ssItem(skaf83(U_5952))
| ( nil = U_5952 )
| ~ ssList(U_5952) ),
inference(superposition,[status(thm),theory(equality)],[c_161464,c_192]) ).
tff(c_171607,plain,
! [U_6631] :
( ( tl(U_6631) = skaf82(U_6631) )
| ( nil = U_6631 )
| ~ ssList(U_6631) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_26,c_161476]) ).
tff(c_171703,plain,
( ( tl(sk6) = skaf82(sk6) )
| ( sk6 = nil ) ),
inference(resolution,[status(thm)],[c_386,c_171607]) ).
tff(c_171747,plain,
tl(sk6) = skaf82(sk6),
inference(negUnitSimplification,[status(thm)],[c_170514,c_171703]) ).
tff(c_208,plain,
! [U_108] :
( ( nil = U_108 )
| ( cons(hd(U_108),tl(U_108)) = U_108 )
| ~ ssList(U_108) ),
inference(cnfTransformation,[status(thm)],[f_492]) ).
tff(c_171853,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),skaf82(sk6)) = sk6 )
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_171747,c_208]) ).
tff(c_171866,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),skaf82(sk6)) = sk6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_171853]) ).
tff(c_171867,plain,
cons(hd(sk6),skaf82(sk6)) = sk6,
inference(negUnitSimplification,[status(thm)],[c_170514,c_171866]) ).
tff(c_276,plain,
! [V_177,W_178] :
( memberP(cons(V_177,W_178),V_177)
| ~ ssItem(V_177)
| ~ ssList(W_178) ),
inference(cnfTransformation,[status(thm)],[f_898]) ).
tff(c_172463,plain,
( memberP(sk6,hd(sk6))
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6)) ),
inference(superposition,[status(thm),theory(equality)],[c_171867,c_276]) ).
tff(c_172524,plain,
( memberP(sk6,hd(sk6))
| ~ ssItem(hd(sk6)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_172463]) ).
tff(c_173130,plain,
~ ssItem(hd(sk6)),
inference(splitLeft,[status(thm)],[c_172524]) ).
tff(c_173133,plain,
( ( sk6 = nil )
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[c_156,c_173130]) ).
tff(c_173136,plain,
sk6 = nil,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_173133]) ).
tff(c_173138,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_170514,c_173136]) ).
tff(c_173140,plain,
ssItem(hd(sk6)),
inference(splitRight,[status(thm)],[c_172524]) ).
tff(c_166856,plain,
! [W_6201,U_6202,V_6203,X_6204] :
( ( W_6201 = U_6202 )
| ~ ssItem(U_6202)
| ~ ssItem(W_6201)
| ~ ssList(V_6203)
| ~ ssList(X_6204)
| ~ frontsegP(cons(U_6202,V_6203),cons(W_6201,X_6204)) ),
inference(cnfTransformation,[status(thm)],[f_1422]) ).
tff(c_166886,plain,
! [W_6201,X_6204] :
( ( sk9 = W_6201 )
| ~ ssItem(sk9)
| ~ ssItem(W_6201)
| ~ ssList(nil)
| ~ ssList(X_6204)
| ~ frontsegP(sk1,cons(W_6201,X_6204)) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_166856]) ).
tff(c_199932,plain,
! [W_7477,X_7478] :
( ( sk9 = W_7477 )
| ~ ssItem(W_7477)
| ~ ssList(X_7478)
| ~ frontsegP(sk1,cons(W_7477,X_7478)) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_166886]) ).
tff(c_200019,plain,
( ( hd(sk6) = sk9 )
| ~ ssItem(hd(sk6))
| ~ ssList(skaf82(sk6))
| ~ frontsegP(sk1,sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_171867,c_199932]) ).
tff(c_200120,plain,
( ( hd(sk6) = sk9 )
| ~ frontsegP(sk1,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_173140,c_200019]) ).
tff(c_200179,plain,
~ frontsegP(sk1,sk6),
inference(splitLeft,[status(thm)],[c_200120]) ).
tff(c_168456,plain,
! [U_6257,V_6258,W_6259] :
( segmentP(app(app(U_6257,V_6258),W_6259),V_6258)
| ~ ssList(app(app(U_6257,V_6258),W_6259))
| ~ ssList(V_6258)
| ~ ssList(U_6257)
| ~ ssList(W_6259) ),
inference(cnfTransformation,[status(thm)],[f_1371]) ).
tff(c_168581,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_168456]) ).
tff(c_168747,plain,
( segmentP(sk1,cons(sk5,nil))
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_416,c_390,c_168581]) ).
tff(c_184989,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_168747]) ).
tff(c_184992,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_184989]) ).
tff(c_184996,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_184992]) ).
tff(c_184998,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_168747]) ).
tff(c_165942,plain,
! [W_6181,V_6182,U_6183] :
( ( app(app(W_6181,V_6182),U_6183) = app(W_6181,app(V_6182,U_6183)) )
| ~ ssList(W_6181)
| ~ ssList(V_6182)
| ~ ssList(U_6183) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_166046,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_165942]) ).
tff(c_166188,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_166046]) ).
tff(c_207066,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_184998,c_166188]) ).
tff(c_207119,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_207066]) ).
tff(c_207155,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_207119]) ).
tff(c_207216,plain,
( frontsegP(sk1,sk6)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_207155,c_288]) ).
tff(c_207265,plain,
( frontsegP(sk1,sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_416,c_207155,c_207216]) ).
tff(c_207266,plain,
~ ssList(cons(sk5,sk7)),
inference(negUnitSimplification,[status(thm)],[c_200179,c_207265]) ).
tff(c_207283,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_207266]) ).
tff(c_207287,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_207283]) ).
tff(c_207289,plain,
frontsegP(sk1,sk6),
inference(splitRight,[status(thm)],[c_200120]) ).
tff(c_159273,plain,
! [U_2] : ( app(nil,skaf82(U_2)) = skaf82(U_2) ),
inference(resolution,[status(thm)],[c_26,c_159150]) ).
tff(c_162654,plain,
! [U_2] :
( frontsegP(skaf82(U_2),nil)
| ~ ssList(app(nil,skaf82(U_2)))
| ~ ssList(nil)
| ~ ssList(skaf82(U_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_159273,c_162550]) ).
tff(c_162760,plain,
! [U_2] : frontsegP(skaf82(U_2),nil),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_16,c_26,c_159273,c_162654]) ).
tff(c_207288,plain,
hd(sk6) = sk9,
inference(splitRight,[status(thm)],[c_200120]) ).
tff(c_207362,plain,
cons(sk9,skaf82(sk6)) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_207288,c_171867]) ).
tff(c_165549,plain,
! [X_6162,U_6163,V_6164] :
( frontsegP(cons(X_6162,U_6163),cons(X_6162,V_6164))
| ~ ssItem(X_6162)
| ~ ssList(U_6163)
| ~ ssList(V_6164)
| ~ frontsegP(U_6163,V_6164) ),
inference(cnfTransformation,[status(thm)],[f_1460]) ).
tff(c_165583,plain,
! [U_6163] :
( frontsegP(cons(sk9,U_6163),sk1)
| ~ ssItem(sk9)
| ~ ssList(U_6163)
| ~ ssList(nil)
| ~ frontsegP(U_6163,nil) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_165549]) ).
tff(c_165597,plain,
! [U_6163] :
( frontsegP(cons(sk9,U_6163),sk1)
| ~ ssList(U_6163)
| ~ frontsegP(U_6163,nil) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_165583]) ).
tff(c_207523,plain,
( frontsegP(sk6,sk1)
| ~ ssList(skaf82(sk6))
| ~ frontsegP(skaf82(sk6),nil) ),
inference(superposition,[status(thm),theory(equality)],[c_207362,c_165597]) ).
tff(c_207635,plain,
frontsegP(sk6,sk1),
inference(demodulation,[status(thm),theory(equality)],[c_162760,c_26,c_207523]) ).
tff(c_207707,plain,
( ( sk6 = sk1 )
| ~ ssList(sk6)
| ~ ssList(sk1)
| ~ frontsegP(sk1,sk6) ),
inference(resolution,[status(thm)],[c_207635,c_258]) ).
tff(c_207716,plain,
sk6 = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_207289,c_416,c_386,c_207707]) ).
tff(c_160406,plain,
! [U_5862] :
( ( cons(skaf44(U_5862),nil) = U_5862 )
| ~ ssList(U_5862)
| ~ singletonP(U_5862) ),
inference(cnfTransformation,[status(thm)],[f_464]) ).
tff(c_160430,plain,
! [U_5862] :
( equalelemsP(U_5862)
| ~ ssItem(skaf44(U_5862))
| ~ ssList(U_5862)
| ~ singletonP(U_5862) ),
inference(superposition,[status(thm),theory(equality)],[c_160406,c_128]) ).
tff(c_160462,plain,
! [U_5864] :
( equalelemsP(U_5864)
| ~ ssList(U_5864)
| ~ singletonP(U_5864) ),
inference(demodulation,[status(thm),theory(equality)],[c_94,c_160430]) ).
tff(c_160600,plain,
( equalelemsP(sk6)
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_160462]) ).
tff(c_160605,plain,
~ singletonP(sk6),
inference(splitLeft,[status(thm)],[c_160600]) ).
tff(c_207888,plain,
~ singletonP(sk1),
inference(demodulation,[status(thm),theory(equality)],[c_207716,c_160605]) ).
tff(c_207929,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_161514,c_207888]) ).
tff(c_207930,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_161178]) ).
tff(c_159275,plain,
app(nil,sk6) = sk6,
inference(resolution,[status(thm)],[c_386,c_159150]) ).
tff(c_162684,plain,
( frontsegP(sk6,nil)
| ~ ssList(app(nil,sk6))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_159275,c_162550]) ).
tff(c_162780,plain,
frontsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_159275,c_162684]) ).
tff(c_163077,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ frontsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_162780,c_258]) ).
tff(c_163080,plain,
( ( sk6 = nil )
| ~ frontsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_163077]) ).
tff(c_165742,plain,
~ frontsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_163080]) ).
tff(c_207956,plain,
~ frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_207930,c_165742]) ).
tff(c_207995,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_162786,c_207956]) ).
tff(c_207996,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_163080]) ).
tff(c_162413,plain,
( rearsegP(sk6,nil)
| ~ ssList(app(sk6,nil))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_2402,c_162285]) ).
tff(c_162511,plain,
rearsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_2402,c_162413]) ).
tff(c_162540,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ rearsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_162511,c_256]) ).
tff(c_162543,plain,
( ( sk6 = nil )
| ~ rearsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_162540]) ).
tff(c_165634,plain,
~ rearsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_162543]) ).
tff(c_207998,plain,
~ rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_207996,c_165634]) ).
tff(c_208033,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_162521,c_207998]) ).
tff(c_208034,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_162543]) ).
tff(c_394,plain,
( memberP(sk7,sk8)
| memberP(sk6,sk8) ),
inference(cnfTransformation,[status(thm)],[f_1658]) ).
tff(c_2269,plain,
memberP(sk6,sk8),
inference(splitLeft,[status(thm)],[c_394]) ).
tff(c_208065,plain,
memberP(nil,sk8),
inference(demodulation,[status(thm),theory(equality)],[c_208034,c_2269]) ).
tff(c_208084,plain,
~ ssItem(sk8),
inference(resolution,[status(thm)],[c_208065,c_142]) ).
tff(c_208088,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_392,c_208084]) ).
tff(c_208090,plain,
singletonP(sk6),
inference(splitRight,[status(thm)],[c_160600]) ).
tff(c_202,plain,
! [U_103] :
( ( cons(skaf44(U_103),nil) = U_103 )
| ~ ssList(U_103)
| ~ singletonP(U_103) ),
inference(cnfTransformation,[status(thm)],[f_464]) ).
tff(c_159664,plain,
! [V_5831,U_5832] :
( ~ ssList(V_5831)
| ~ ssItem(U_5832)
| ( cons(U_5832,V_5831) != nil ) ),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_209363,plain,
! [U_7793] :
( ~ ssItem(U_7793)
| ( cons(U_7793,nil) != nil ) ),
inference(resolution,[status(thm)],[c_16,c_159664]) ).
tff(c_209821,plain,
! [U_7805] : ( cons(skaf44(U_7805),nil) != nil ),
inference(resolution,[status(thm)],[c_94,c_209363]) ).
tff(c_217333,plain,
! [U_8192] :
( ( nil != U_8192 )
| ~ ssList(U_8192)
| ~ singletonP(U_8192) ),
inference(superposition,[status(thm),theory(equality)],[c_202,c_209821]) ).
tff(c_217429,plain,
( ( sk6 != nil )
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_217333]) ).
tff(c_217472,plain,
sk6 != nil,
inference(demodulation,[status(thm),theory(equality)],[c_208090,c_217429]) ).
tff(c_222567,plain,
cons(sk9,sk7) = app(sk1,sk7),
inference(resolution,[status(thm)],[c_388,c_222426]) ).
tff(c_222804,plain,
( ssList(app(sk1,sk7))
| ~ ssList(sk7)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_222567,c_172]) ).
tff(c_222864,plain,
ssList(app(sk1,sk7)),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_388,c_222804]) ).
tff(c_208208,plain,
! [U_7686,V_7687] :
( ( hd(cons(U_7686,V_7687)) = U_7686 )
| ~ ssList(V_7687)
| ~ ssItem(U_7686) ),
inference(cnfTransformation,[status(thm)],[f_428]) ).
tff(c_208223,plain,
( ( hd(sk1) = sk9 )
| ~ ssList(nil)
| ~ ssItem(sk9) ),
inference(superposition,[status(thm),theory(equality)],[c_159588,c_208208]) ).
tff(c_208229,plain,
hd(sk1) = sk9,
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_16,c_208223]) ).
tff(c_249028,plain,
hd(sk1) = sk5,
inference(demodulation,[status(thm),theory(equality)],[c_248937,c_208229]) ).
tff(c_249022,plain,
cons(sk5,sk7) = app(sk1,sk7),
inference(demodulation,[status(thm),theory(equality)],[c_248937,c_222567]) ).
tff(c_251830,plain,
app(sk6,app(sk1,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_249022,c_248725]) ).
tff(c_246,plain,
! [V_145,U_144] :
( ( hd(app(V_145,U_144)) = hd(V_145) )
| ( nil = V_145 )
| ~ ssList(V_145)
| ~ ssList(U_144) ),
inference(cnfTransformation,[status(thm)],[f_702]) ).
tff(c_252271,plain,
( ( hd(sk6) = hd(sk1) )
| ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(app(sk1,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_251830,c_246]) ).
tff(c_252306,plain,
( ( hd(sk6) = sk5 )
| ( sk6 = nil ) ),
inference(demodulation,[status(thm),theory(equality)],[c_222864,c_386,c_249028,c_252271]) ).
tff(c_252307,plain,
hd(sk6) = sk5,
inference(negUnitSimplification,[status(thm)],[c_217472,c_252306]) ).
tff(c_160412,plain,
! [U_5862] :
( ( tl(U_5862) = nil )
| ~ ssList(nil)
| ~ ssItem(skaf44(U_5862))
| ~ ssList(U_5862)
| ~ singletonP(U_5862) ),
inference(superposition,[status(thm),theory(equality)],[c_160406,c_192]) ).
tff(c_217501,plain,
! [U_8218] :
( ( tl(U_8218) = nil )
| ~ ssList(U_8218)
| ~ singletonP(U_8218) ),
inference(demodulation,[status(thm),theory(equality)],[c_94,c_16,c_160412]) ).
tff(c_217597,plain,
( ( tl(sk6) = nil )
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_217501]) ).
tff(c_217640,plain,
tl(sk6) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_208090,c_217597]) ).
tff(c_217652,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),nil) = sk6 )
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_217640,c_208]) ).
tff(c_217662,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),nil) = sk6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_217652]) ).
tff(c_217663,plain,
cons(hd(sk6),nil) = sk6,
inference(negUnitSimplification,[status(thm)],[c_217472,c_217662]) ).
tff(c_252431,plain,
cons(sk5,nil) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_252307,c_217663]) ).
tff(c_252439,plain,
sk6 = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_249029,c_252431]) ).
tff(c_249380,plain,
app(app(sk6,sk1),sk7) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_249029,c_390]) ).
tff(c_252522,plain,
app(app(sk1,sk1),sk7) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_252439,c_249380]) ).
tff(c_256535,plain,
( frontsegP(sk1,app(sk1,sk1))
| ~ ssList(app(app(sk1,sk1),sk7))
| ~ ssList(app(sk1,sk1))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_252522,c_288]) ).
tff(c_256583,plain,
frontsegP(sk1,app(sk1,sk1)),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_223844,c_416,c_252522,c_256535]) ).
tff(c_256585,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_245534,c_256583]) ).
tff(c_256587,plain,
~ memberP(sk6,sk8),
inference(splitRight,[status(thm)],[c_394]) ).
tff(c_330631,plain,
~ memberP(nil,sk8),
inference(demodulation,[status(thm),theory(equality)],[c_330472,c_256587]) ).
tff(c_256586,plain,
memberP(sk7,sk8),
inference(splitRight,[status(thm)],[c_394]) ).
tff(c_282,plain,
! [W_187,U_185,V_186] :
( memberP(app(W_187,U_185),V_186)
| ~ ssItem(V_186)
| ~ ssList(W_187)
| ~ ssList(U_185)
| ~ memberP(U_185,V_186) ),
inference(cnfTransformation,[status(thm)],[f_940]) ).
tff(c_348514,plain,
! [V_186] :
( memberP(sk1,V_186)
| ~ ssItem(V_186)
| ~ ssList(app(nil,cons(sk5,nil)))
| ~ ssList(sk7)
| ~ memberP(sk7,V_186) ),
inference(superposition,[status(thm),theory(equality)],[c_330628,c_282]) ).
tff(c_349938,plain,
! [V_12632] :
( memberP(sk1,V_12632)
| ~ ssItem(V_12632)
| ~ memberP(sk7,V_12632) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_348222,c_348514]) ).
tff(c_349952,plain,
( memberP(sk1,sk8)
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[c_256586,c_349938]) ).
tff(c_349965,plain,
memberP(sk1,sk8),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_349952]) ).
tff(c_331002,plain,
! [W_11715,U_11716,V_11717] :
( ( W_11715 = U_11716 )
| memberP(V_11717,W_11715)
| ~ ssItem(W_11715)
| ~ ssItem(U_11716)
| ~ ssList(V_11717)
| ~ memberP(cons(U_11716,V_11717),W_11715) ),
inference(cnfTransformation,[status(thm)],[f_1239]) ).
tff(c_331023,plain,
! [W_11715] :
( ( sk9 = W_11715 )
| memberP(nil,W_11715)
| ~ ssItem(W_11715)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk1,W_11715) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_331002]) ).
tff(c_364969,plain,
! [W_13025] :
( ( sk9 = W_13025 )
| memberP(nil,W_13025)
| ~ ssItem(W_13025)
| ~ memberP(sk1,W_13025) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_331023]) ).
tff(c_364975,plain,
( ( sk9 = sk8 )
| memberP(nil,sk8)
| ~ ssItem(sk8) ),
inference(resolution,[status(thm)],[c_349965,c_364969]) ).
tff(c_364992,plain,
( ( sk9 = sk8 )
| memberP(nil,sk8) ),
inference(demodulation,[status(thm),theory(equality)],[c_392,c_364975]) ).
tff(c_364993,plain,
sk9 = sk8,
inference(negUnitSimplification,[status(thm)],[c_330631,c_364992]) ).
tff(c_331037,plain,
! [W_11722,U_11723,V_11724,X_11725] :
( ( W_11722 = U_11723 )
| ~ ssItem(U_11723)
| ~ ssItem(W_11722)
| ~ ssList(V_11724)
| ~ ssList(X_11725)
| ~ frontsegP(cons(U_11723,V_11724),cons(W_11722,X_11725)) ),
inference(cnfTransformation,[status(thm)],[f_1422]) ).
tff(c_331067,plain,
! [W_11722,X_11725] :
( ( sk9 = W_11722 )
| ~ ssItem(sk9)
| ~ ssItem(W_11722)
| ~ ssList(nil)
| ~ ssList(X_11725)
| ~ frontsegP(sk1,cons(W_11722,X_11725)) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_331037]) ).
tff(c_331086,plain,
! [W_11722,X_11725] :
( ( sk9 = W_11722 )
| ~ ssItem(W_11722)
| ~ ssList(X_11725)
| ~ frontsegP(sk1,cons(W_11722,X_11725)) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_331067]) ).
tff(c_366235,plain,
! [W_11722,X_11725] :
( ( sk8 = W_11722 )
| ~ ssItem(W_11722)
| ~ ssList(X_11725)
| ~ frontsegP(sk1,cons(W_11722,X_11725)) ),
inference(demodulation,[status(thm),theory(equality)],[c_364993,c_331086]) ).
tff(c_368778,plain,
( ( sk8 = sk5 )
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[c_368660,c_366235]) ).
tff(c_368785,plain,
sk8 = sk5,
inference(demodulation,[status(thm),theory(equality)],[c_16,c_384,c_368778]) ).
tff(c_396,plain,
( ~ leq(sk5,sk8)
| memberP(sk6,sk8) ),
inference(cnfTransformation,[status(thm)],[f_1662]) ).
tff(c_256912,plain,
~ leq(sk5,sk8),
inference(negUnitSimplification,[status(thm)],[c_256587,c_396]) ).
tff(c_368850,plain,
~ leq(sk5,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_368785,c_256912]) ).
tff(c_369272,plain,
~ ssItem(sk5),
inference(resolution,[status(thm)],[c_124,c_368850]) ).
tff(c_369282,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_369272]) ).
tff(c_369284,plain,
singletonP(sk6),
inference(splitRight,[status(thm)],[c_258330]) ).
tff(c_257389,plain,
! [U_36] : ( cons(skaf44(U_36),nil) != nil ),
inference(resolution,[status(thm)],[c_94,c_257309]) ).
tff(c_378538,plain,
! [U_13628] :
( ( nil != U_13628 )
| ~ ssList(U_13628)
| ~ singletonP(U_13628) ),
inference(superposition,[status(thm),theory(equality)],[c_257915,c_257389]) ).
tff(c_378634,plain,
( ( sk6 != nil )
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_378538]) ).
tff(c_378677,plain,
sk6 != nil,
inference(demodulation,[status(thm),theory(equality)],[c_369284,c_378634]) ).
tff(c_369412,plain,
! [U_13098,V_13099] :
( ( tl(cons(U_13098,V_13099)) = V_13099 )
| ~ ssList(V_13099)
| ~ ssItem(U_13098) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_369424,plain,
! [U_103] :
( ( tl(U_103) = nil )
| ~ ssList(nil)
| ~ ssItem(skaf44(U_103))
| ~ ssList(U_103)
| ~ singletonP(U_103) ),
inference(superposition,[status(thm),theory(equality)],[c_202,c_369412]) ).
tff(c_378700,plain,
! [U_13647] :
( ( tl(U_13647) = nil )
| ~ ssList(U_13647)
| ~ singletonP(U_13647) ),
inference(demodulation,[status(thm),theory(equality)],[c_94,c_16,c_369424]) ).
tff(c_378796,plain,
( ( tl(sk6) = nil )
| ~ singletonP(sk6) ),
inference(resolution,[status(thm)],[c_386,c_378700]) ).
tff(c_378839,plain,
tl(sk6) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_369284,c_378796]) ).
tff(c_378851,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),nil) = sk6 )
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_378839,c_208]) ).
tff(c_378861,plain,
( ( sk6 = nil )
| ( cons(hd(sk6),nil) = sk6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_378851]) ).
tff(c_378862,plain,
cons(hd(sk6),nil) = sk6,
inference(negUnitSimplification,[status(thm)],[c_378677,c_378861]) ).
tff(c_138,plain,
! [U_63] :
( totalorderP(cons(U_63,nil))
| ~ ssItem(U_63) ),
inference(cnfTransformation,[status(thm)],[f_222]) ).
tff(c_378960,plain,
( totalorderP(sk6)
| ~ ssItem(hd(sk6)) ),
inference(superposition,[status(thm),theory(equality)],[c_378862,c_138]) ).
tff(c_379045,plain,
~ ssItem(hd(sk6)),
inference(splitLeft,[status(thm)],[c_378960]) ).
tff(c_379049,plain,
( ( sk6 = nil )
| ~ ssList(sk6) ),
inference(resolution,[status(thm)],[c_156,c_379045]) ).
tff(c_379052,plain,
sk6 = nil,
inference(demodulation,[status(thm),theory(equality)],[c_386,c_379049]) ).
tff(c_379054,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_378677,c_379052]) ).
tff(c_379056,plain,
ssItem(hd(sk6)),
inference(splitRight,[status(thm)],[c_378960]) ).
tff(c_375176,plain,
! [W_13394,U_13395,V_13396,X_13397] :
( ( W_13394 = U_13395 )
| ~ ssItem(U_13395)
| ~ ssItem(W_13394)
| ~ ssList(V_13396)
| ~ ssList(X_13397)
| ~ frontsegP(cons(U_13395,V_13396),cons(W_13394,X_13397)) ),
inference(cnfTransformation,[status(thm)],[f_1422]) ).
tff(c_375206,plain,
! [W_13394,X_13397] :
( ( sk9 = W_13394 )
| ~ ssItem(sk9)
| ~ ssItem(W_13394)
| ~ ssList(nil)
| ~ ssList(X_13397)
| ~ frontsegP(sk1,cons(W_13394,X_13397)) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_375176]) ).
tff(c_407196,plain,
! [W_14663,X_14664] :
( ( sk9 = W_14663 )
| ~ ssItem(W_14663)
| ~ ssList(X_14664)
| ~ frontsegP(sk1,cons(W_14663,X_14664)) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_375206]) ).
tff(c_407286,plain,
( ( hd(sk6) = sk9 )
| ~ ssItem(hd(sk6))
| ~ ssList(nil)
| ~ frontsegP(sk1,sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_378862,c_407196]) ).
tff(c_407386,plain,
( ( hd(sk6) = sk9 )
| ~ frontsegP(sk1,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_379056,c_407286]) ).
tff(c_407452,plain,
~ frontsegP(sk1,sk6),
inference(splitLeft,[status(thm)],[c_407386]) ).
tff(c_374735,plain,
! [W_13382,V_13383,U_13384] :
( ( app(app(W_13382,V_13383),U_13384) = app(W_13382,app(V_13383,U_13384)) )
| ~ ssList(W_13382)
| ~ ssList(V_13383)
| ~ ssList(U_13384) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_374775,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_374735,c_390]) ).
tff(c_374955,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_374775]) ).
tff(c_412268,plain,
app(sk6,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_393884,c_374955]) ).
tff(c_412318,plain,
( ( app(sk6,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_412268]) ).
tff(c_412352,plain,
app(sk6,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_412318]) ).
tff(c_412411,plain,
( frontsegP(sk1,sk6)
| ~ ssList(app(sk6,cons(sk5,sk7)))
| ~ ssList(sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(superposition,[status(thm),theory(equality)],[c_412352,c_288]) ).
tff(c_412458,plain,
( frontsegP(sk1,sk6)
| ~ ssList(cons(sk5,sk7)) ),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_416,c_412352,c_412411]) ).
tff(c_412459,plain,
~ ssList(cons(sk5,sk7)),
inference(negUnitSimplification,[status(thm)],[c_407452,c_412458]) ).
tff(c_412476,plain,
( ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_412459]) ).
tff(c_412480,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_412476]) ).
tff(c_412481,plain,
hd(sk6) = sk9,
inference(splitRight,[status(thm)],[c_407386]) ).
tff(c_412706,plain,
cons(sk9,nil) = sk6,
inference(demodulation,[status(thm),theory(equality)],[c_412481,c_378862]) ).
tff(c_412716,plain,
sk6 = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_257395,c_412706]) ).
tff(c_412933,plain,
app(app(sk1,cons(sk5,nil)),sk7) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_412716,c_390]) ).
tff(c_414239,plain,
( ( app(sk1,app(cons(sk5,nil),sk7)) = sk1 )
| ~ ssList(sk1)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_298,c_412933]) ).
tff(c_414278,plain,
app(sk1,app(cons(sk5,nil),sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_388,c_393884,c_416,c_414239]) ).
tff(c_414800,plain,
( ( app(sk1,cons(sk5,sk7)) = sk1 )
| ~ ssList(sk7)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_240,c_414278]) ).
tff(c_414833,plain,
app(sk1,cons(sk5,sk7)) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_388,c_414800]) ).
tff(c_414862,plain,
( memberP(sk1,sk5)
| ~ ssList(app(sk1,cons(sk5,sk7)))
| ~ ssItem(sk5)
| ~ ssList(sk1)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_414833,c_350]) ).
tff(c_414919,plain,
memberP(sk1,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_416,c_384,c_416,c_414833,c_414862]) ).
tff(c_374437,plain,
! [W_13358,U_13359,V_13360] :
( ( W_13358 = U_13359 )
| memberP(V_13360,W_13358)
| ~ ssItem(W_13358)
| ~ ssItem(U_13359)
| ~ ssList(V_13360)
| ~ memberP(cons(U_13359,V_13360),W_13358) ),
inference(cnfTransformation,[status(thm)],[f_1239]) ).
tff(c_374458,plain,
! [W_13358] :
( ( sk9 = W_13358 )
| memberP(nil,W_13358)
| ~ ssItem(W_13358)
| ~ ssItem(sk9)
| ~ ssList(nil)
| ~ memberP(sk1,W_13358) ),
inference(superposition,[status(thm),theory(equality)],[c_257395,c_374437]) ).
tff(c_374467,plain,
! [W_13358] :
( ( sk9 = W_13358 )
| memberP(nil,W_13358)
| ~ ssItem(W_13358)
| ~ memberP(sk1,W_13358) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2128,c_374458]) ).
tff(c_414950,plain,
( ( sk9 = sk5 )
| memberP(nil,sk5)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_414919,c_374467]) ).
tff(c_414953,plain,
( ( sk9 = sk5 )
| memberP(nil,sk5) ),
inference(demodulation,[status(thm),theory(equality)],[c_384,c_414950]) ).
tff(c_414954,plain,
memberP(nil,sk5),
inference(splitLeft,[status(thm)],[c_414953]) ).
tff(c_414957,plain,
~ ssItem(sk5),
inference(resolution,[status(thm)],[c_414954,c_142]) ).
tff(c_414961,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_414957]) ).
tff(c_414962,plain,
sk9 = sk5,
inference(splitRight,[status(thm)],[c_414953]) ).
tff(c_415051,plain,
cons(sk5,nil) = sk1,
inference(demodulation,[status(thm),theory(equality)],[c_414962,c_257395]) ).
tff(c_371019,plain,
! [U_13219,V_13220] :
( rearsegP(app(U_13219,V_13220),V_13220)
| ~ ssList(app(U_13219,V_13220))
| ~ ssList(V_13220)
| ~ ssList(U_13219) ),
inference(cnfTransformation,[status(thm)],[f_961]) ).
tff(c_371072,plain,
( rearsegP(sk1,sk7)
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_390,c_371019]) ).
tff(c_371207,plain,
( rearsegP(sk1,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_416,c_390,c_371072]) ).
tff(c_385121,plain,
~ ssList(app(sk6,cons(sk5,nil))),
inference(splitLeft,[status(thm)],[c_371207]) ).
tff(c_385211,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[c_170,c_385121]) ).
tff(c_385214,plain,
~ ssList(cons(sk5,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_385211]) ).
tff(c_385217,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_385214]) ).
tff(c_385221,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_385217]) ).
tff(c_385223,plain,
ssList(app(sk6,cons(sk5,nil))),
inference(splitRight,[status(thm)],[c_371207]) ).
tff(c_412829,plain,
ssList(app(sk1,cons(sk5,nil))),
inference(demodulation,[status(thm),theory(equality)],[c_412716,c_385223]) ).
tff(c_414226,plain,
( frontsegP(sk1,app(sk1,cons(sk5,nil)))
| ~ ssList(app(app(sk1,cons(sk5,nil)),sk7))
| ~ ssList(app(sk1,cons(sk5,nil)))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_412933,c_288]) ).
tff(c_414268,plain,
frontsegP(sk1,app(sk1,cons(sk5,nil))),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_412829,c_416,c_412933,c_414226]) ).
tff(c_415211,plain,
frontsegP(sk1,app(sk1,sk1)),
inference(demodulation,[status(thm),theory(equality)],[c_415051,c_414268]) ).
tff(c_415253,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_406451,c_415211]) ).
tff(c_415254,plain,
sk1 = nil,
inference(splitRight,[status(thm)],[c_413]) ).
tff(c_449288,plain,
app(app(sk6,cons(sk5,nil)),sk7) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_415254,c_390]) ).
tff(c_451437,plain,
( rearsegP(nil,sk7)
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_449288,c_451378]) ).
tff(c_451564,plain,
( rearsegP(nil,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_16,c_449288,c_451437]) ).
tff(c_461763,plain,
~ ssList(app(sk6,cons(sk5,nil))),
inference(negUnitSimplification,[status(thm)],[c_454554,c_451564]) ).
tff(c_461766,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[c_170,c_461763]) ).
tff(c_461769,plain,
~ ssList(cons(sk5,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_461766]) ).
tff(c_461785,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_461769]) ).
tff(c_461789,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_461785]) ).
tff(c_461790,plain,
sk7 = nil,
inference(splitRight,[status(thm)],[c_451641]) ).
tff(c_415453,plain,
! [U_14851] :
( ( app(U_14851,nil) = U_14851 )
| ~ ssList(U_14851) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_415571,plain,
app(nil,nil) = nil,
inference(resolution,[status(thm)],[c_16,c_415453]) ).
tff(c_418808,plain,
! [U_15099,V_15100] :
( rearsegP(app(U_15099,V_15100),V_15100)
| ~ ssList(app(U_15099,V_15100))
| ~ ssList(V_15100)
| ~ ssList(U_15099) ),
inference(cnfTransformation,[status(thm)],[f_961]) ).
tff(c_418957,plain,
( rearsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_415571,c_418808]) ).
tff(c_419054,plain,
rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_415571,c_418957]) ).
tff(c_418526,plain,
! [U_15097,V_15098] :
( frontsegP(app(U_15097,V_15098),U_15097)
| ~ ssList(app(U_15097,V_15098))
| ~ ssList(U_15097)
| ~ ssList(V_15098) ),
inference(cnfTransformation,[status(thm)],[f_975]) ).
tff(c_418675,plain,
( frontsegP(nil,nil)
| ~ ssList(app(nil,nil))
| ~ ssList(nil)
| ~ ssList(nil) ),
inference(superposition,[status(thm),theory(equality)],[c_415571,c_418526]) ).
tff(c_418772,plain,
frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_16,c_16,c_415571,c_418675]) ).
tff(c_415573,plain,
app(sk7,nil) = sk7,
inference(resolution,[status(thm)],[c_388,c_415453]) ).
tff(c_418951,plain,
( rearsegP(sk7,nil)
| ~ ssList(app(sk7,nil))
| ~ ssList(nil)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_415573,c_418808]) ).
tff(c_419050,plain,
rearsegP(sk7,nil),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_16,c_388,c_415573,c_418951]) ).
tff(c_419068,plain,
( ( sk7 = nil )
| ~ ssList(sk7)
| ~ ssList(nil)
| ~ rearsegP(nil,sk7) ),
inference(resolution,[status(thm)],[c_419050,c_256]) ).
tff(c_419071,plain,
( ( sk7 = nil )
| ~ rearsegP(nil,sk7) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_388,c_419068]) ).
tff(c_421987,plain,
~ rearsegP(nil,sk7),
inference(splitLeft,[status(thm)],[c_419071]) ).
tff(c_416308,plain,
app(app(sk6,cons(sk5,nil)),sk7) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_415254,c_390]) ).
tff(c_418867,plain,
( rearsegP(nil,sk7)
| ~ ssList(app(app(sk6,cons(sk5,nil)),sk7))
| ~ ssList(sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(superposition,[status(thm),theory(equality)],[c_416308,c_418808]) ).
tff(c_418994,plain,
( rearsegP(nil,sk7)
| ~ ssList(app(sk6,cons(sk5,nil))) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_16,c_416308,c_418867]) ).
tff(c_429058,plain,
~ ssList(app(sk6,cons(sk5,nil))),
inference(negUnitSimplification,[status(thm)],[c_421987,c_418994]) ).
tff(c_429061,plain,
( ~ ssList(sk6)
| ~ ssList(cons(sk5,nil)) ),
inference(resolution,[status(thm)],[c_170,c_429058]) ).
tff(c_429064,plain,
~ ssList(cons(sk5,nil)),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_429061]) ).
tff(c_429067,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_429064]) ).
tff(c_429071,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_429067]) ).
tff(c_429072,plain,
sk7 = nil,
inference(splitRight,[status(thm)],[c_419071]) ).
tff(c_415592,plain,
! [U_14859] :
( ( app(nil,U_14859) = U_14859 )
| ~ ssList(U_14859) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_415713,plain,
app(nil,sk7) = sk7,
inference(resolution,[status(thm)],[c_388,c_415592]) ).
tff(c_418663,plain,
( frontsegP(sk7,nil)
| ~ ssList(app(nil,sk7))
| ~ ssList(nil)
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_415713,c_418526]) ).
tff(c_418764,plain,
frontsegP(sk7,nil),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_16,c_388,c_415713,c_418663]) ).
tff(c_418774,plain,
( ( sk7 = nil )
| ~ ssList(sk7)
| ~ ssList(nil)
| ~ frontsegP(nil,sk7) ),
inference(resolution,[status(thm)],[c_418764,c_258]) ).
tff(c_418777,plain,
( ( sk7 = nil )
| ~ frontsegP(nil,sk7) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_388,c_418774]) ).
tff(c_421986,plain,
~ frontsegP(nil,sk7),
inference(splitLeft,[status(thm)],[c_418777]) ).
tff(c_429074,plain,
~ frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_429072,c_421986]) ).
tff(c_429128,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_418772,c_429074]) ).
tff(c_429129,plain,
sk7 = nil,
inference(splitRight,[status(thm)],[c_418777]) ).
tff(c_421509,plain,
! [W_15234,V_15235,U_15236] :
( ( app(app(W_15234,V_15235),U_15236) = app(W_15234,app(V_15235,U_15236)) )
| ~ ssList(W_15234)
| ~ ssList(V_15235)
| ~ ssList(U_15236) ),
inference(cnfTransformation,[status(thm)],[f_1051]) ).
tff(c_421625,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = nil )
| ~ ssList(sk6)
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7) ),
inference(superposition,[status(thm),theory(equality)],[c_416308,c_421509]) ).
tff(c_421765,plain,
( ( app(sk6,app(cons(sk5,nil),sk7)) = nil )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_388,c_386,c_421625]) ).
tff(c_447484,plain,
( ( app(sk6,app(cons(sk5,nil),nil)) = nil )
| ~ ssList(cons(sk5,nil)) ),
inference(demodulation,[status(thm),theory(equality)],[c_429129,c_421765]) ).
tff(c_447485,plain,
~ ssList(cons(sk5,nil)),
inference(splitLeft,[status(thm)],[c_447484]) ).
tff(c_447488,plain,
( ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(resolution,[status(thm)],[c_172,c_447485]) ).
tff(c_447492,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_447488]) ).
tff(c_447494,plain,
ssList(cons(sk5,nil)),
inference(splitRight,[status(thm)],[c_447484]) ).
tff(c_417402,plain,
! [U_15003] :
( ( nil = U_15003 )
| ( cons(skaf83(U_15003),skaf82(U_15003)) = U_15003 )
| ~ ssList(U_15003) ),
inference(cnfTransformation,[status(thm)],[f_543]) ).
tff(c_417411,plain,
! [U_15003] :
( ( skaf83(U_15003) = hd(U_15003) )
| ~ ssList(skaf82(U_15003))
| ~ ssItem(skaf83(U_15003))
| ( nil = U_15003 )
| ~ ssList(U_15003) ),
inference(superposition,[status(thm),theory(equality)],[c_417402,c_194]) ).
tff(c_432814,plain,
! [U_16045] :
( ( skaf83(U_16045) = hd(U_16045) )
| ( nil = U_16045 )
| ~ ssList(U_16045) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_26,c_417411]) ).
tff(c_432943,plain,
( ( skaf83(sk6) = hd(sk6) )
| ( sk6 = nil ) ),
inference(resolution,[status(thm)],[c_386,c_432814]) ).
tff(c_432944,plain,
sk6 = nil,
inference(splitLeft,[status(thm)],[c_432943]) ).
tff(c_415712,plain,
app(nil,sk6) = sk6,
inference(resolution,[status(thm)],[c_386,c_415592]) ).
tff(c_418666,plain,
( frontsegP(sk6,nil)
| ~ ssList(app(nil,sk6))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_415712,c_418526]) ).
tff(c_418766,plain,
frontsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_415712,c_418666]) ).
tff(c_418779,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ frontsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_418766,c_258]) ).
tff(c_418782,plain,
( ( sk6 = nil )
| ~ frontsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_418779]) ).
tff(c_429297,plain,
~ frontsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_418782]) ).
tff(c_432945,plain,
~ frontsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_432944,c_429297]) ).
tff(c_433000,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_418772,c_432945]) ).
tff(c_433002,plain,
sk6 != nil,
inference(splitRight,[status(thm)],[c_432943]) ).
tff(c_417077,plain,
! [U_14977,V_14978] :
( ( nil = U_14977 )
| ~ ssList(U_14977)
| ~ ssList(V_14978)
| ( app(U_14977,V_14978) != nil ) ),
inference(cnfTransformation,[status(thm)],[f_647]) ).
tff(c_417176,plain,
! [V_14978] :
( ( sk6 = nil )
| ~ ssList(V_14978)
| ( app(sk6,V_14978) != nil ) ),
inference(resolution,[status(thm)],[c_386,c_417077]) ).
tff(c_434439,plain,
! [V_14978] :
( ~ ssList(V_14978)
| ( app(sk6,V_14978) != nil ) ),
inference(negUnitSimplification,[status(thm)],[c_433002,c_417176]) ).
tff(c_447599,plain,
app(sk6,cons(sk5,nil)) != nil,
inference(resolution,[status(thm)],[c_447494,c_434439]) ).
tff(c_416188,plain,
! [U_14893,V_14894] :
( ssList(cons(U_14893,V_14894))
| ~ ssList(V_14894)
| ~ ssItem(U_14893) ),
inference(cnfTransformation,[status(thm)],[f_342]) ).
tff(c_146,plain,
! [U_68] :
( ( app(U_68,nil) = U_68 )
| ~ ssList(U_68) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_416202,plain,
! [U_14893,V_14894] :
( ( app(cons(U_14893,V_14894),nil) = cons(U_14893,V_14894) )
| ~ ssList(V_14894)
| ~ ssItem(U_14893) ),
inference(resolution,[status(thm)],[c_416188,c_146]) ).
tff(c_447493,plain,
app(sk6,app(cons(sk5,nil),nil)) = nil,
inference(splitRight,[status(thm)],[c_447484]) ).
tff(c_448074,plain,
( ( app(sk6,cons(sk5,nil)) = nil )
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(superposition,[status(thm),theory(equality)],[c_416202,c_447493]) ).
tff(c_448115,plain,
app(sk6,cons(sk5,nil)) = nil,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_16,c_448074]) ).
tff(c_448117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_447599,c_448115]) ).
tff(c_448118,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_418782]) ).
tff(c_415572,plain,
app(sk6,nil) = sk6,
inference(resolution,[status(thm)],[c_386,c_415453]) ).
tff(c_418954,plain,
( rearsegP(sk6,nil)
| ~ ssList(app(sk6,nil))
| ~ ssList(nil)
| ~ ssList(sk6) ),
inference(superposition,[status(thm),theory(equality)],[c_415572,c_418808]) ).
tff(c_419052,plain,
rearsegP(sk6,nil),
inference(demodulation,[status(thm),theory(equality)],[c_386,c_16,c_386,c_415572,c_418954]) ).
tff(c_419114,plain,
( ( sk6 = nil )
| ~ ssList(sk6)
| ~ ssList(nil)
| ~ rearsegP(nil,sk6) ),
inference(resolution,[status(thm)],[c_419052,c_256]) ).
tff(c_419117,plain,
( ( sk6 = nil )
| ~ rearsegP(nil,sk6) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386,c_419114]) ).
tff(c_421952,plain,
~ rearsegP(nil,sk6),
inference(splitLeft,[status(thm)],[c_419117]) ).
tff(c_448120,plain,
~ rearsegP(nil,nil),
inference(demodulation,[status(thm),theory(equality)],[c_448118,c_421952]) ).
tff(c_448174,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_419054,c_448120]) ).
tff(c_448175,plain,
sk6 = nil,
inference(splitRight,[status(thm)],[c_419117]) ).
tff(c_415438,plain,
memberP(sk6,sk8),
inference(splitLeft,[status(thm)],[c_394]) ).
tff(c_448259,plain,
memberP(nil,sk8),
inference(demodulation,[status(thm),theory(equality)],[c_448175,c_415438]) ).
tff(c_448277,plain,
~ ssItem(sk8),
inference(resolution,[status(thm)],[c_448259,c_142]) ).
tff(c_448281,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_392,c_448277]) ).
tff(c_448282,plain,
memberP(sk7,sk8),
inference(splitRight,[status(thm)],[c_394]) ).
tff(c_461841,plain,
memberP(nil,sk8),
inference(demodulation,[status(thm),theory(equality)],[c_461790,c_448282]) ).
tff(c_461859,plain,
~ ssItem(sk8),
inference(resolution,[status(thm)],[c_461841,c_142]) ).
tff(c_461863,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_392,c_461859]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWC284-1 : TPTP v9.0.0. Released v2.4.0.
% 0.14/0.14 % 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.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 02:06:07 EDT 2025
% 0.14/0.35 % CPUTime :
% 249.48/226.39 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 249.66/226.47
% 249.66/226.47 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------