%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWC096-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:01:25 AM UTC 2026
% Result : Unsatisfiable 71.56s 71.83s
% Output : Proof 71.83s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,axiom,
equalelemsP(nil),
file('SWC001-0.ax',clause1) ).
cnf(clause2,axiom,
duplicatefreeP(nil),
file('SWC001-0.ax',clause2) ).
cnf(clause3,axiom,
strictorderedP(nil),
file('SWC001-0.ax',clause3) ).
cnf(clause4,axiom,
totalorderedP(nil),
file('SWC001-0.ax',clause4) ).
cnf(clause5,axiom,
strictorderP(nil),
file('SWC001-0.ax',clause5) ).
cnf(clause6,axiom,
totalorderP(nil),
file('SWC001-0.ax',clause6) ).
cnf(clause7,axiom,
cyclefreeP(nil),
file('SWC001-0.ax',clause7) ).
cnf(clause8,axiom,
ssList(nil),
file('SWC001-0.ax',clause8) ).
cnf(clause9,axiom,
ssItem(skac3),
file('SWC001-0.ax',clause9) ).
cnf(clause10,axiom,
ssItem(skac2),
file('SWC001-0.ax',clause10) ).
cnf(clause11,axiom,
~ singletonP(nil),
file('SWC001-0.ax',clause11) ).
cnf(clause12,axiom,
ssItem(skaf83(U)),
file('SWC001-0.ax',clause12) ).
cnf(clause13,axiom,
ssList(skaf82(U)),
file('SWC001-0.ax',clause13) ).
cnf(clause14,axiom,
ssList(skaf81(U)),
file('SWC001-0.ax',clause14) ).
cnf(clause15,axiom,
ssList(skaf80(U)),
file('SWC001-0.ax',clause15) ).
cnf(clause16,axiom,
ssItem(skaf79(U)),
file('SWC001-0.ax',clause16) ).
cnf(clause17,axiom,
ssItem(skaf78(U)),
file('SWC001-0.ax',clause17) ).
cnf(clause18,axiom,
ssList(skaf77(U)),
file('SWC001-0.ax',clause18) ).
cnf(clause19,axiom,
ssList(skaf76(U)),
file('SWC001-0.ax',clause19) ).
cnf(clause20,axiom,
ssList(skaf75(U)),
file('SWC001-0.ax',clause20) ).
cnf(clause21,axiom,
ssItem(skaf74(U)),
file('SWC001-0.ax',clause21) ).
cnf(clause22,axiom,
ssList(skaf73(U)),
file('SWC001-0.ax',clause22) ).
cnf(clause23,axiom,
ssList(skaf72(U)),
file('SWC001-0.ax',clause23) ).
cnf(clause24,axiom,
ssList(skaf71(U)),
file('SWC001-0.ax',clause24) ).
cnf(clause25,axiom,
ssItem(skaf70(U)),
file('SWC001-0.ax',clause25) ).
cnf(clause26,axiom,
ssItem(skaf69(U)),
file('SWC001-0.ax',clause26) ).
cnf(clause27,axiom,
ssList(skaf68(U)),
file('SWC001-0.ax',clause27) ).
cnf(clause28,axiom,
ssList(skaf67(U)),
file('SWC001-0.ax',clause28) ).
cnf(clause29,axiom,
ssList(skaf66(U)),
file('SWC001-0.ax',clause29) ).
cnf(clause30,axiom,
ssItem(skaf65(U)),
file('SWC001-0.ax',clause30) ).
cnf(clause31,axiom,
ssItem(skaf64(U)),
file('SWC001-0.ax',clause31) ).
cnf(clause32,axiom,
ssList(skaf63(U)),
file('SWC001-0.ax',clause32) ).
cnf(clause33,axiom,
ssList(skaf62(U)),
file('SWC001-0.ax',clause33) ).
cnf(clause34,axiom,
ssList(skaf61(U)),
file('SWC001-0.ax',clause34) ).
cnf(clause35,axiom,
ssItem(skaf60(U)),
file('SWC001-0.ax',clause35) ).
cnf(clause36,axiom,
ssItem(skaf59(U)),
file('SWC001-0.ax',clause36) ).
cnf(clause37,axiom,
ssList(skaf58(U)),
file('SWC001-0.ax',clause37) ).
cnf(clause38,axiom,
ssList(skaf57(U)),
file('SWC001-0.ax',clause38) ).
cnf(clause39,axiom,
ssList(skaf56(U)),
file('SWC001-0.ax',clause39) ).
cnf(clause40,axiom,
ssItem(skaf55(U)),
file('SWC001-0.ax',clause40) ).
cnf(clause41,axiom,
ssItem(skaf54(U)),
file('SWC001-0.ax',clause41) ).
cnf(clause42,axiom,
ssList(skaf53(U)),
file('SWC001-0.ax',clause42) ).
cnf(clause43,axiom,
ssList(skaf52(U)),
file('SWC001-0.ax',clause43) ).
cnf(clause44,axiom,
ssList(skaf51(U)),
file('SWC001-0.ax',clause44) ).
cnf(clause45,axiom,
ssItem(skaf50(U)),
file('SWC001-0.ax',clause45) ).
cnf(clause46,axiom,
ssItem(skaf49(U)),
file('SWC001-0.ax',clause46) ).
cnf(clause47,axiom,
ssItem(skaf44(U)),
file('SWC001-0.ax',clause47) ).
cnf(clause48,axiom,
ssList(skaf48(U,V)),
file('SWC001-0.ax',clause48) ).
cnf(clause49,axiom,
ssList(skaf47(U,V)),
file('SWC001-0.ax',clause49) ).
cnf(clause50,axiom,
ssList(skaf46(U,V)),
file('SWC001-0.ax',clause50) ).
cnf(clause51,axiom,
ssList(skaf45(U,V)),
file('SWC001-0.ax',clause51) ).
cnf(clause52,axiom,
ssList(skaf43(U,V)),
file('SWC001-0.ax',clause52) ).
cnf(clause53,axiom,
ssList(skaf42(U,V)),
file('SWC001-0.ax',clause53) ).
cnf(clause54,axiom,
skac3 != skac2,
file('SWC001-0.ax',clause54) ).
cnf(clause55,axiom,
( geq(U,U)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause55) ).
cnf(clause56,axiom,
( segmentP(U,nil)
| ~ ssList(U) ),
file('SWC001-0.ax',clause56) ).
cnf(clause57,axiom,
( segmentP(U,U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause57) ).
cnf(clause58,axiom,
( rearsegP(U,nil)
| ~ ssList(U) ),
file('SWC001-0.ax',clause58) ).
cnf(clause59,axiom,
( rearsegP(U,U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause59) ).
cnf(clause60,axiom,
( frontsegP(U,nil)
| ~ ssList(U) ),
file('SWC001-0.ax',clause60) ).
cnf(clause61,axiom,
( frontsegP(U,U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause61) ).
cnf(clause62,axiom,
( leq(U,U)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause62) ).
cnf(clause63,axiom,
( ~ ssItem(U)
| ~ lt(U,U) ),
file('SWC001-0.ax',clause63) ).
cnf(clause64,axiom,
( equalelemsP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause64) ).
cnf(clause65,axiom,
( duplicatefreeP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause65) ).
cnf(clause66,axiom,
( strictorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause66) ).
cnf(clause67,axiom,
( totalorderedP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause67) ).
cnf(clause68,axiom,
( strictorderP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause68) ).
cnf(clause69,axiom,
( totalorderP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause69) ).
cnf(clause70,axiom,
( cyclefreeP(cons(U,nil))
| ~ ssItem(U) ),
file('SWC001-0.ax',clause70) ).
cnf(clause71,axiom,
( ~ ssItem(U)
| ~ memberP(nil,U) ),
file('SWC001-0.ax',clause71) ).
cnf(clause72,axiom,
( ssItem(V)
| duplicatefreeP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause72) ).
cnf(clause73,axiom,
( app(U,nil) = U
| ~ ssList(U) ),
file('SWC001-0.ax',clause73) ).
cnf(clause74,axiom,
( app(nil,U) = U
| ~ ssList(U) ),
file('SWC001-0.ax',clause74) ).
cnf(clause75,axiom,
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('SWC001-0.ax',clause75) ).
cnf(clause76,axiom,
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('SWC001-0.ax',clause76) ).
cnf(clause77,axiom,
( nil = U
| ssList(tl(U))
| ~ ssList(U) ),
file('SWC001-0.ax',clause77) ).
cnf(clause78,axiom,
( nil = U
| ssItem(hd(U))
| ~ ssList(U) ),
file('SWC001-0.ax',clause78) ).
cnf(clause79,axiom,
( segmentP(nil,U)
| ~ ssList(U)
| nil != U ),
file('SWC001-0.ax',clause79) ).
cnf(clause80,axiom,
( nil = U
| ~ ssList(U)
| ~ segmentP(nil,U) ),
file('SWC001-0.ax',clause80) ).
cnf(clause81,axiom,
( rearsegP(nil,U)
| ~ ssList(U)
| nil != U ),
file('SWC001-0.ax',clause81) ).
cnf(clause82,axiom,
( nil = U
| ~ ssList(U)
| ~ rearsegP(nil,U) ),
file('SWC001-0.ax',clause82) ).
cnf(clause83,axiom,
( frontsegP(nil,U)
| ~ ssList(U)
| nil != U ),
file('SWC001-0.ax',clause83) ).
cnf(clause84,axiom,
( nil = U
| ~ ssList(U)
| ~ frontsegP(nil,U) ),
file('SWC001-0.ax',clause84) ).
cnf(clause85,axiom,
( ssList(app(V,U))
| ~ ssList(V)
| ~ ssList(U) ),
file('SWC001-0.ax',clause85) ).
cnf(clause86,axiom,
( ssList(cons(U,V))
| ~ ssList(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause86) ).
cnf(clause87,axiom,
( leq(skaf50(U),skaf49(U))
| cyclefreeP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause87) ).
cnf(clause88,axiom,
( leq(skaf49(U),skaf50(U))
| cyclefreeP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause88) ).
cnf(clause89,axiom,
( equalelemsP(U)
| ~ ssList(U)
| skaf79(U) != skaf78(U) ),
file('SWC001-0.ax',clause89) ).
cnf(clause90,axiom,
( strictorderedP(U)
| ~ ssList(U)
| ~ lt(skaf69(U),skaf70(U)) ),
file('SWC001-0.ax',clause90) ).
cnf(clause91,axiom,
( totalorderedP(U)
| ~ ssList(U)
| ~ leq(skaf64(U),skaf65(U)) ),
file('SWC001-0.ax',clause91) ).
cnf(clause92,axiom,
( strictorderP(U)
| ~ ssList(U)
| ~ lt(skaf60(U),skaf59(U)) ),
file('SWC001-0.ax',clause92) ).
cnf(clause93,axiom,
( strictorderP(U)
| ~ ssList(U)
| ~ lt(skaf59(U),skaf60(U)) ),
file('SWC001-0.ax',clause93) ).
cnf(clause94,axiom,
( totalorderP(U)
| ~ ssList(U)
| ~ leq(skaf55(U),skaf54(U)) ),
file('SWC001-0.ax',clause94) ).
cnf(clause95,axiom,
( totalorderP(U)
| ~ ssList(U)
| ~ leq(skaf54(U),skaf55(U)) ),
file('SWC001-0.ax',clause95) ).
cnf(clause96,axiom,
( tl(cons(U,V)) = V
| ~ ssList(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause96) ).
cnf(clause97,axiom,
( hd(cons(U,V)) = U
| ~ ssList(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause97) ).
cnf(clause98,axiom,
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != nil ),
file('SWC001-0.ax',clause98) ).
cnf(clause99,axiom,
( ~ ssList(V)
| ~ ssItem(U)
| cons(U,V) != V ),
file('SWC001-0.ax',clause99) ).
cnf(clause100,axiom,
( V = U
| neq(V,U)
| ~ ssList(V)
| ~ ssList(U) ),
file('SWC001-0.ax',clause100) ).
cnf(clause101,axiom,
( cons(skaf44(U),nil) = U
| ~ ssList(U)
| ~ singletonP(U) ),
file('SWC001-0.ax',clause101) ).
cnf(clause102,axiom,
( V = U
| neq(V,U)
| ~ ssItem(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause102) ).
cnf(clause103,axiom,
( leq(U,V)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ lt(U,V) ),
file('SWC001-0.ax',clause103) ).
cnf(clause104,axiom,
( nil = U
| cons(hd(U),tl(U)) = U
| ~ ssList(U) ),
file('SWC001-0.ax',clause104) ).
cnf(clause105,axiom,
( lt(V,U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ gt(U,V) ),
file('SWC001-0.ax',clause105) ).
cnf(clause106,axiom,
( gt(V,U)
| ~ ssItem(V)
| ~ ssItem(U)
| ~ lt(U,V) ),
file('SWC001-0.ax',clause106) ).
cnf(clause107,axiom,
( leq(V,U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ geq(U,V) ),
file('SWC001-0.ax',clause107) ).
cnf(clause108,axiom,
( geq(V,U)
| ~ ssItem(V)
| ~ ssItem(U)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause108) ).
cnf(clause109,axiom,
( nil = U
| cons(skaf83(U),skaf82(U)) = U
| ~ ssList(U) ),
file('SWC001-0.ax',clause109) ).
cnf(clause110,axiom,
( ~ ssItem(V)
| ~ ssItem(U)
| ~ gt(V,U)
| ~ gt(U,V) ),
file('SWC001-0.ax',clause110) ).
cnf(clause111,axiom,
( ~ ssItem(U)
| ~ ssItem(V)
| ~ lt(U,V)
| U != V ),
file('SWC001-0.ax',clause111) ).
cnf(clause112,axiom,
( strictorderedP(cons(V,U))
| ~ ssItem(V)
| ~ ssList(U)
| nil != U ),
file('SWC001-0.ax',clause112) ).
cnf(clause113,axiom,
( totalorderedP(cons(V,U))
| ~ ssItem(V)
| ~ ssList(U)
| nil != U ),
file('SWC001-0.ax',clause113) ).
cnf(clause114,axiom,
( ~ ssItem(V)
| ~ ssItem(U)
| ~ lt(V,U)
| ~ lt(U,V) ),
file('SWC001-0.ax',clause114) ).
cnf(clause115,axiom,
( ~ ssList(U)
| ~ ssList(V)
| ~ neq(U,V)
| U != V ),
file('SWC001-0.ax',clause115) ).
cnf(clause116,axiom,
( singletonP(V)
| ~ ssList(V)
| ~ ssItem(U)
| cons(U,nil) != V ),
file('SWC001-0.ax',clause116) ).
cnf(clause117,axiom,
( ~ ssItem(U)
| ~ ssItem(V)
| ~ neq(U,V)
| U != V ),
file('SWC001-0.ax',clause117) ).
cnf(clause118,axiom,
( nil = U
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('SWC001-0.ax',clause118) ).
cnf(clause119,axiom,
( nil = V
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != nil ),
file('SWC001-0.ax',clause119) ).
cnf(clause120,axiom,
( app(cons(U,nil),V) = cons(U,V)
| ~ ssList(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause120) ).
cnf(clause121,axiom,
( U = V
| lt(U,V)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause121) ).
cnf(clause122,axiom,
( U = V
| lt(U,V)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause122) ).
cnf(clause123,axiom,
( hd(app(V,U)) = hd(V)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('SWC001-0.ax',clause123) ).
cnf(clause124,axiom,
( nil = V
| strictorderedP(V)
| ~ ssItem(U)
| ~ ssList(V)
| ~ strictorderedP(cons(U,V)) ),
file('SWC001-0.ax',clause124) ).
cnf(clause125,axiom,
( nil = V
| totalorderedP(V)
| ~ ssItem(U)
| ~ ssList(V)
| ~ totalorderedP(cons(U,V)) ),
file('SWC001-0.ax',clause125) ).
cnf(clause126,axiom,
( V = U
| ~ ssItem(V)
| ~ ssItem(U)
| ~ geq(V,U)
| ~ geq(U,V) ),
file('SWC001-0.ax',clause126) ).
cnf(clause127,axiom,
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ segmentP(V,U)
| ~ segmentP(U,V) ),
file('SWC001-0.ax',clause127) ).
cnf(clause128,axiom,
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ rearsegP(V,U)
| ~ rearsegP(U,V) ),
file('SWC001-0.ax',clause128) ).
cnf(clause129,axiom,
( V = U
| ~ ssList(V)
| ~ ssList(U)
| ~ frontsegP(V,U)
| ~ frontsegP(U,V) ),
file('SWC001-0.ax',clause129) ).
cnf(clause130,axiom,
( V = U
| ~ ssItem(V)
| ~ ssItem(U)
| ~ leq(V,U)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause130) ).
cnf(clause131,axiom,
( app(skaf46(U,V),V) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ rearsegP(U,V) ),
file('SWC001-0.ax',clause131) ).
cnf(clause132,axiom,
( app(V,skaf45(U,V)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ frontsegP(U,V) ),
file('SWC001-0.ax',clause132) ).
cnf(clause133,axiom,
( tl(app(V,U)) = app(tl(V),U)
| nil = V
| ~ ssList(V)
| ~ ssList(U) ),
file('SWC001-0.ax',clause133) ).
cnf(clause134,axiom,
( nil = V
| lt(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ strictorderedP(cons(U,V)) ),
file('SWC001-0.ax',clause134) ).
cnf(clause135,axiom,
( nil = V
| leq(U,hd(V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ totalorderedP(cons(U,V)) ),
file('SWC001-0.ax',clause135) ).
cnf(clause136,axiom,
( rearsegP(app(W,U),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(U,V) ),
file('SWC001-0.ax',clause136) ).
cnf(clause137,axiom,
( frontsegP(app(U,W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(U,V) ),
file('SWC001-0.ax',clause137) ).
cnf(clause138,axiom,
( memberP(cons(V,W),U)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| U != V ),
file('SWC001-0.ax',clause138) ).
cnf(clause139,axiom,
( memberP(cons(W,U),V)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('SWC001-0.ax',clause139) ).
cnf(clause140,axiom,
( memberP(app(U,W),V)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ memberP(U,V) ),
file('SWC001-0.ax',clause140) ).
cnf(clause141,axiom,
( memberP(app(W,U),V)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(U)
| ~ memberP(U,V) ),
file('SWC001-0.ax',clause141) ).
cnf(clause142,axiom,
( app(skaf80(U),cons(skaf78(U),cons(skaf79(U),skaf81(U)))) = U
| equalelemsP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause142) ).
cnf(clause143,axiom,
( rearsegP(W,V)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != W ),
file('SWC001-0.ax',clause143) ).
cnf(clause144,axiom,
( frontsegP(W,U)
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != W ),
file('SWC001-0.ax',clause144) ).
cnf(clause145,axiom,
( app(U,V) = nil
| ~ ssList(U)
| ~ ssList(V)
| nil != V
| nil != U ),
file('SWC001-0.ax',clause145) ).
cnf(clause146,axiom,
( gt(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ gt(V,W)
| ~ gt(U,V) ),
file('SWC001-0.ax',clause146) ).
cnf(clause147,axiom,
( lt(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ lt(V,W)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause147) ).
cnf(clause148,axiom,
( geq(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ geq(V,W)
| ~ geq(U,V) ),
file('SWC001-0.ax',clause148) ).
cnf(clause149,axiom,
( app(app(W,V),U) = app(W,app(V,U))
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U) ),
file('SWC001-0.ax',clause149) ).
cnf(clause150,axiom,
( V = W
| ~ ssList(W)
| ~ ssList(U)
| ~ ssList(V)
| app(U,V) != app(U,W) ),
file('SWC001-0.ax',clause150) ).
cnf(clause151,axiom,
( U = W
| ~ ssList(W)
| ~ ssList(V)
| ~ ssList(U)
| app(U,V) != app(W,V) ),
file('SWC001-0.ax',clause151) ).
cnf(clause152,axiom,
( segmentP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ segmentP(V,W)
| ~ segmentP(U,V) ),
file('SWC001-0.ax',clause152) ).
cnf(clause153,axiom,
( rearsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ rearsegP(V,W)
| ~ rearsegP(U,V) ),
file('SWC001-0.ax',clause153) ).
cnf(clause154,axiom,
( frontsegP(U,W)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V) ),
file('SWC001-0.ax',clause154) ).
cnf(clause155,axiom,
( lt(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ lt(V,W)
| ~ lt(U,V) ),
file('SWC001-0.ax',clause155) ).
cnf(clause156,axiom,
( leq(U,W)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ leq(V,W)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause156) ).
cnf(clause157,axiom,
( cons(U,app(V,W)) = app(cons(U,V),W)
| ~ ssList(W)
| ~ ssList(V)
| ~ ssItem(U) ),
file('SWC001-0.ax',clause157) ).
cnf(clause158,axiom,
( memberP(U,W)
| memberP(V,W)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(V)
| ~ memberP(app(U,V),W) ),
file('SWC001-0.ax',clause158) ).
cnf(clause159,axiom,
( nil = V
| totalorderedP(cons(U,V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ totalorderedP(V)
| ~ leq(U,hd(V)) ),
file('SWC001-0.ax',clause159) ).
cnf(clause160,axiom,
( nil = V
| strictorderedP(cons(U,V))
| ~ ssItem(U)
| ~ ssList(V)
| ~ strictorderedP(V)
| ~ lt(U,hd(V)) ),
file('SWC001-0.ax',clause160) ).
cnf(clause161,axiom,
( W = U
| memberP(V,W)
| ~ ssItem(W)
| ~ ssItem(U)
| ~ ssList(V)
| ~ memberP(cons(U,V),W) ),
file('SWC001-0.ax',clause161) ).
cnf(clause162,axiom,
( app(app(skaf75(U),cons(skaf74(U),skaf76(U))),cons(skaf74(U),skaf77(U))) = U
| duplicatefreeP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause162) ).
cnf(clause163,axiom,
( app(app(skaf71(U),cons(skaf69(U),skaf72(U))),cons(skaf70(U),skaf73(U))) = U
| strictorderedP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause163) ).
cnf(clause164,axiom,
( app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U
| totalorderedP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause164) ).
cnf(clause165,axiom,
( app(app(skaf61(U),cons(skaf59(U),skaf62(U))),cons(skaf60(U),skaf63(U))) = U
| strictorderP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause165) ).
cnf(clause166,axiom,
( app(app(skaf56(U),cons(skaf54(U),skaf57(U))),cons(skaf55(U),skaf58(U))) = U
| totalorderP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause166) ).
cnf(clause167,axiom,
( app(app(skaf51(U),cons(skaf49(U),skaf52(U))),cons(skaf50(U),skaf53(U))) = U
| cyclefreeP(U)
| ~ ssList(U) ),
file('SWC001-0.ax',clause167) ).
cnf(clause168,axiom,
( app(app(skaf47(U,V),V),skaf48(V,U)) = U
| ~ ssList(U)
| ~ ssList(V)
| ~ segmentP(U,V) ),
file('SWC001-0.ax',clause168) ).
cnf(clause169,axiom,
( app(skaf42(U,V),cons(V,skaf43(V,U))) = U
| ~ ssList(U)
| ~ ssItem(V)
| ~ memberP(U,V) ),
file('SWC001-0.ax',clause169) ).
cnf(clause170,axiom,
( U = W
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('SWC001-0.ax',clause170) ).
cnf(clause171,axiom,
( X = V
| ~ ssList(V)
| ~ ssList(X)
| ~ ssItem(U)
| ~ ssItem(W)
| cons(U,V) != cons(W,X) ),
file('SWC001-0.ax',clause171) ).
cnf(clause172,axiom,
( segmentP(app(app(X,U),W),V)
| ~ ssList(U)
| ~ ssList(V)
| ~ ssList(X)
| ~ ssList(W)
| ~ segmentP(U,V) ),
file('SWC001-0.ax',clause172) ).
cnf(clause173,axiom,
( segmentP(X,V)
| ~ ssList(X)
| ~ ssList(V)
| ~ ssList(U)
| ~ ssList(W)
| app(app(U,V),W) != X ),
file('SWC001-0.ax',clause173) ).
cnf(clause174,axiom,
( frontsegP(V,X)
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('SWC001-0.ax',clause174) ).
cnf(clause175,axiom,
( memberP(X,V)
| ~ ssList(X)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| app(U,cons(V,W)) != X ),
file('SWC001-0.ax',clause175) ).
cnf(clause176,axiom,
( U = W
| ~ ssItem(U)
| ~ ssItem(W)
| ~ ssList(V)
| ~ ssList(X)
| ~ frontsegP(cons(U,V),cons(W,X)) ),
file('SWC001-0.ax',clause176) ).
cnf(clause177,axiom,
( nil = U
| U = V
| nil = V
| ~ ssList(V)
| ~ ssList(U)
| hd(U) != hd(V)
| tl(U) != tl(V) ),
file('SWC001-0.ax',clause177) ).
cnf(clause178,axiom,
( frontsegP(cons(W,U),cons(X,V))
| ~ ssItem(W)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(V)
| W != X
| ~ frontsegP(U,V) ),
file('SWC001-0.ax',clause178) ).
cnf(clause179,axiom,
( ~ ssList(Y)
| ~ duplicatefreeP(Y)
| ~ ssItem(V)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(X)
| app(app(U,cons(V,W)),cons(V,X)) != Y ),
file('SWC001-0.ax',clause179) ).
cnf(clause180,axiom,
( V = W
| ~ ssList(Y)
| ~ equalelemsP(Y)
| ~ ssItem(V)
| ~ ssItem(W)
| ~ ssList(U)
| ~ ssList(X)
| app(U,cons(V,cons(W,X))) != Y ),
file('SWC001-0.ax',clause180) ).
cnf(clause181,axiom,
( lt(V,X)
| ~ ssList(Z)
| ~ strictorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('SWC001-0.ax',clause181) ).
cnf(clause182,axiom,
( leq(V,X)
| ~ ssList(Z)
| ~ totalorderedP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('SWC001-0.ax',clause182) ).
cnf(clause183,axiom,
( lt(X,V)
| lt(V,X)
| ~ ssList(Z)
| ~ strictorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('SWC001-0.ax',clause183) ).
cnf(clause184,axiom,
( leq(X,V)
| leq(V,X)
| ~ ssList(Z)
| ~ totalorderP(Z)
| ~ ssItem(V)
| ~ ssItem(X)
| ~ ssList(U)
| ~ ssList(W)
| ~ ssList(Y)
| app(app(U,cons(V,W)),cons(X,Y)) != Z ),
file('SWC001-0.ax',clause184) ).
cnf(clause185,axiom,
( ~ ssList(Z)
| ~ cyclefreeP(Z)
| ~ ssItem(U)
| ~ ssItem(V)
| ~ ssList(W)
| ~ ssList(X)
| ~ ssList(Y)
| app(app(W,cons(U,X)),cons(V,Y)) != Z
| ~ leq(V,U)
| ~ leq(U,V) ),
file('SWC001-0.ax',clause185) ).
cnf(co1_1,negated_conjecture,
ssList(sk1),
file('theBenchmark.p',co1_1) ).
cnf(co1_2,negated_conjecture,
ssList(sk2),
file('theBenchmark.p',co1_2) ).
cnf(co1_3,negated_conjecture,
ssList(sk3),
file('theBenchmark.p',co1_3) ).
cnf(co1_4,negated_conjecture,
ssList(sk4),
file('theBenchmark.p',co1_4) ).
cnf(co1_5,negated_conjecture,
sk2 = sk4,
file('theBenchmark.p',co1_5) ).
cnf(co1_6,negated_conjecture,
sk1 = sk3,
file('theBenchmark.p',co1_6) ).
cnf(co1_7,negated_conjecture,
( neq(sk2,nil)
| neq(sk2,nil) ),
file('theBenchmark.p',co1_7) ).
cnf(co1_8,negated_conjecture,
( ~ neq(sk4,nil)
| neq(sk2,nil) ),
file('theBenchmark.p',co1_8) ).
cnf(co1_9,negated_conjecture,
( neq(sk2,nil)
| app(B,cons(A,nil)) != sk2
| cons(A,nil) != sk1
| ~ ssList(B)
| ~ ssItem(A) ),
file('theBenchmark.p',co1_9) ).
cnf(co1_10,negated_conjecture,
( neq(sk2,nil)
| ssItem(sk5) ),
file('theBenchmark.p',co1_10) ).
cnf(co1_11,negated_conjecture,
( neq(sk2,nil)
| ssList(sk6) ),
file('theBenchmark.p',co1_11) ).
cnf(co1_12,negated_conjecture,
( neq(sk2,nil)
| cons(sk5,nil) = sk3 ),
file('theBenchmark.p',co1_12) ).
cnf(co1_13,negated_conjecture,
( neq(sk2,nil)
| app(sk6,cons(sk5,nil)) = sk4 ),
file('theBenchmark.p',co1_13) ).
cnf(co1_14,negated_conjecture,
( ~ neq(sk4,nil)
| app(B,cons(A,nil)) != sk2
| cons(A,nil) != sk1
| ~ ssList(B)
| ~ ssItem(A) ),
file('theBenchmark.p',co1_14) ).
cnf(co1_15,negated_conjecture,
( ~ neq(sk4,nil)
| ssItem(sk5) ),
file('theBenchmark.p',co1_15) ).
cnf(co1_16,negated_conjecture,
( ~ neq(sk4,nil)
| ssList(sk6) ),
file('theBenchmark.p',co1_16) ).
cnf(co1_17,negated_conjecture,
( ~ neq(sk4,nil)
| cons(sk5,nil) = sk3 ),
file('theBenchmark.p',co1_17) ).
cnf(co1_18,negated_conjecture,
( ~ neq(sk4,nil)
| app(sk6,cons(sk5,nil)) = sk4 ),
file('theBenchmark.p',co1_18) ).
cnf(co1_7_simplified,negated_conjecture,
neq(sk2,nil),
inference(simplify_clause,[status(thm)],[co1_7]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( skaf83(Eq_x_0) = skaf83(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( skaf82(Eq_x_0) = skaf82(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( skaf81(Eq_x_0) = skaf81(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( skaf80(Eq_x_0) = skaf80(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( skaf79(Eq_x_0) = skaf79(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( skaf78(Eq_x_0) = skaf78(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( skaf77(Eq_x_0) = skaf77(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( skaf76(Eq_x_0) = skaf76(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( skaf75(Eq_x_0) = skaf75(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( skaf74(Eq_x_0) = skaf74(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( skaf73(Eq_x_0) = skaf73(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( skaf72(Eq_x_0) = skaf72(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( skaf71(Eq_x_0) = skaf71(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( skaf70(Eq_x_0) = skaf70(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( skaf69(Eq_x_0) = skaf69(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( skaf68(Eq_x_0) = skaf68(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( skaf67(Eq_x_0) = skaf67(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( skaf66(Eq_x_0) = skaf66(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( skaf65(Eq_x_0) = skaf65(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( skaf64(Eq_x_0) = skaf64(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( skaf63(Eq_x_0) = skaf63(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( skaf62(Eq_x_0) = skaf62(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( skaf61(Eq_x_0) = skaf61(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( skaf60(Eq_x_0) = skaf60(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( skaf59(Eq_x_0) = skaf59(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( skaf58(Eq_x_0) = skaf58(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( skaf57(Eq_x_0) = skaf57(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( skaf56(Eq_x_0) = skaf56(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( skaf55(Eq_x_0) = skaf55(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( skaf54(Eq_x_0) = skaf54(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( skaf53(Eq_x_0) = skaf53(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( skaf52(Eq_x_0) = skaf52(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( skaf51(Eq_x_0) = skaf51(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( skaf50(Eq_x_0) = skaf50(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( skaf49(Eq_x_0) = skaf49(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( skaf44(Eq_x_0) = skaf44(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( skaf48(Eq_x_0,Eq_x_1) = skaf48(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( skaf47(Eq_x_0,Eq_x_1) = skaf47(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( skaf46(Eq_x_0,Eq_x_1) = skaf46(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( skaf45(Eq_x_0,Eq_x_1) = skaf45(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( skaf43(Eq_x_0,Eq_x_1) = skaf43(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( skaf42(Eq_x_0,Eq_x_1) = skaf42(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( cons(Eq_x_0,Eq_x_1) = cons(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( app(Eq_x_0,Eq_x_1) = app(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,axiom,
( tl(Eq_x_0) = tl(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_49,axiom,
( hd(Eq_x_0) = hd(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_50,axiom,
( equalelemsP(Eq_y_0)
| ~ equalelemsP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,axiom,
( duplicatefreeP(Eq_y_0)
| ~ duplicatefreeP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_52,axiom,
( strictorderedP(Eq_y_0)
| ~ strictorderedP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_53,axiom,
( totalorderedP(Eq_y_0)
| ~ totalorderedP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_54,axiom,
( strictorderP(Eq_y_0)
| ~ strictorderP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,axiom,
( totalorderP(Eq_y_0)
| ~ totalorderP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_56,axiom,
( cyclefreeP(Eq_y_0)
| ~ cyclefreeP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_57,axiom,
( ssList(Eq_y_0)
| ~ ssList(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_58,axiom,
( ssItem(Eq_y_0)
| ~ ssItem(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( singletonP(Eq_y_0)
| ~ singletonP(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( geq(Eq_y_0,Eq_y_1)
| ~ geq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( segmentP(Eq_y_0,Eq_y_1)
| ~ segmentP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( rearsegP(Eq_y_0,Eq_y_1)
| ~ rearsegP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( frontsegP(Eq_y_0,Eq_y_1)
| ~ frontsegP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( leq(Eq_y_0,Eq_y_1)
| ~ leq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( lt(Eq_y_0,Eq_y_1)
| ~ lt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( memberP(Eq_y_0,Eq_y_1)
| ~ memberP(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( neq(Eq_y_0,Eq_y_1)
| ~ neq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( gt(Eq_y_0,Eq_y_1)
| ~ gt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC096-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 01:51:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 71.56/71.83 % SZS status Unsatisfiable for theBenchmark
% 71.56/71.83 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------