%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SWC316+1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n026.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 : Sun Sep 27 08:54:57 AM UTC 2026 % Result : Theorem 36.16s 56.87s % Output : CNFRefutation 36.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC316+1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.37 % Computer : n026.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 : Sat Sep 26 12:49:41 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 36.16/56.87 % SZS status Theorem for theBenchmark.p % 36.16/56.87 % SZS output start CNFRefutation for theBenchmark.p % 36.16/56.87 fof(ax6, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (rearsegP(X0,X1) <=> ? [X2] : ((ssList(X2) & app(X2,X1) = X0)))))))). % 36.16/56.87 fof(ax15, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (neq(X0,X1) <=> X0 != X1)))))). % 36.16/56.87 fof(ax16, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => ssList(cons(X1,X0))))))). % 36.16/56.87 fof(ax17, axiom, ssList(nil)). % 36.16/56.87 fof(ax18, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => cons(X1,X0) != X0))))). % 36.16/56.87 fof(ax20, axiom, ! [X0] : ((ssList(X0) => (nil = X0 | ? [X1] : ((ssList(X1) & ? [X2] : ((ssItem(X2) & cons(X2,X1) = X0)))))))). % 36.16/56.87 fof(ax21, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => nil != cons(X1,X0)))))). % 36.16/56.87 fof(ax22, axiom, ! [X0] : ((ssList(X0) => (nil != X0 => ssItem(hd(X0)))))). % 36.16/56.87 fof(ax23, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => hd(cons(X1,X0)) = X1))))). % 36.16/56.87 fof(ax25, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => tl(cons(X1,X0)) = X0))))). % 36.16/56.87 fof(ax48, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ((rearsegP(X0,X1) & rearsegP(X1,X0)) => X0 = X1)))))). % 36.16/56.87 fof(ax50, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => (rearsegP(X0,X1) => rearsegP(app(X2,X0),X1))))))))). % 36.16/56.87 fof(ax51, axiom, ! [X0] : ((ssList(X0) => rearsegP(X0,nil)))). % 36.16/56.87 fof(ax75, axiom, ! [X0] : ((ssList(X0) => (nil != X0 => ? [X1] : ((ssItem(X1) & hd(X0) = X1)))))). % 36.16/56.87 fof(ax78, axiom, ! [X0] : ((ssList(X0) => (nil != X0 => cons(hd(X0),tl(X0)) = X0)))). % 36.16/56.87 fof(ax81, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => cons(X1,X0) = app(cons(X1,nil),X0)))))). % 36.16/56.87 fof(ax84, axiom, ! [X0] : ((ssList(X0) => app(X0,nil) = X0))). % 36.16/56.87 fof(co1, conjecture, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | ((~neq(X1,nil) | (! [X4] : ((ssItem(X4) => ! [X5] : ((ssList(X5) => (app(cons(X4,nil),X5) != X2 | app(X5,cons(X4,nil)) != X3))))) | (? [X6] : ((ssList(X6) & (X1 = X6 & ? [X7] : ((ssList(X7) & ? [X8] : ((ssList(X8) & (tl(X0) = X7 & (app(X7,X8) = X6 & (? [X9] : ((ssItem(X9) & (cons(X9,nil) = X8 & (hd(X0) = X9 & neq(nil,X0))))) & neq(nil,X0))))))))))) & neq(X0,nil)))) & (~neq(X1,nil) | neq(X3,nil)))))))))))))). % 36.16/56.87 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | ((~neq(X1,nil) | (! [X4] : ((ssItem(X4) => ! [X5] : ((ssList(X5) => (app(cons(X4,nil),X5) != X2 | app(X5,cons(X4,nil)) != X3))))) | (? [X6] : ((ssList(X6) & (X1 = X6 & ? [X7] : ((ssList(X7) & ? [X8] : ((ssList(X8) & (tl(X0) = X7 & (app(X7,X8) = X6 & (? [X9] : ((ssItem(X9) & (cons(X9,nil) = X8 & (hd(X0) = X9 & neq(nil,X0))))) & neq(nil,X0))))))))))) & neq(X0,nil)))) & (~neq(X1,nil) | neq(X3,nil))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 36.16/56.87 cnf(c17, plain, ~ssList(X0) | rearsegP(X1,X2) | ~ssList(X1) | ~ssList(X2) | app(X0,X2) != X1, inference(clausification, [status(esa)], [ax6])). % 36.16/56.87 cnf(c95, plain, ~ssList(X0) | ~ssList(X1) | neq(X0,X1) | X0 = X1, inference(clausification, [status(esa)], [ax15])). % 36.16/56.87 cnf(c96, plain, ~ssList(X0) | ~ssItem(X1) | ssList(cons(X1,X0)), inference(clausification, [status(esa)], [ax16])). % 36.16/56.87 cnf(c97, plain, ssList(nil), inference(clausification, [status(esa)], [ax17])). % 36.16/56.87 cnf(c98, plain, ~ssList(X0) | ~ssItem(X1) | cons(X1,X0) != X0, inference(clausification, [status(esa)], [ax18])). % 36.16/56.87 cnf(c101, plain, ~ssList(X0) | nil = X0 | ssList(sK120(X0)), inference(clausification, [status(esa)], [ax20])). % 36.16/56.87 cnf(c102, plain, ~ssList(X0) | nil = X0 | ssItem(sK121(X0)), inference(clausification, [status(esa)], [ax20])). % 36.16/56.87 cnf(c103, plain, ~ssList(X0) | nil = X0 | cons(sK121(X0),sK120(X0)) = X0, inference(clausification, [status(esa)], [ax20])). % 36.16/56.87 cnf(c104, plain, ~ssList(X0) | ~ssItem(X1) | nil != cons(X1,X0), inference(clausification, [status(esa)], [ax21])). % 36.16/56.87 cnf(c105, plain, ~ssList(X0) | nil = X0 | ssItem(hd(X0)), inference(clausification, [status(esa)], [ax22])). % 36.16/56.87 cnf(c106, plain, ~ssList(X0) | ~ssItem(X1) | hd(cons(X1,X0)) = X1, inference(clausification, [status(esa)], [ax23])). % 36.16/56.87 cnf(c108, plain, ~ssList(X0) | ~ssItem(X1) | tl(cons(X1,X0)) = X0, inference(clausification, [status(esa)], [ax25])). % 36.16/56.87 cnf(c140, plain, X0 = X1 | ~rearsegP(X0,X1) | ~rearsegP(X1,X0) | ~ssList(X1) | ~ssList(X0), inference(clausification, [status(esa)], [ax48])). % 36.16/56.87 cnf(c142, plain, ~ssList(X0) | ~ssList(X1) | ~ssList(X2) | rearsegP(app(X1,X2),X0) | ~rearsegP(X2,X0), inference(clausification, [status(esa)], [ax50])). % 36.16/56.87 cnf(c143, plain, ~ssList(X0) | rearsegP(X0,nil), inference(clausification, [status(esa)], [ax51])). % 36.16/56.87 cnf(c181, plain, ~ssList(X0) | nil = X0 | ssItem(sK210(X0)), inference(clausification, [status(esa)], [ax75])). % 36.16/56.87 cnf(c182, plain, ~ssList(X0) | nil = X0 | hd(X0) = sK210(X0), inference(clausification, [status(esa)], [ax75])). % 36.16/56.87 cnf(c186, plain, ~ssList(X0) | nil = X0 | cons(hd(X0),tl(X0)) = X0, inference(clausification, [status(esa)], [ax78])). % 36.16/56.87 cnf(c189, plain, ~ssList(X0) | ~ssItem(X1) | cons(X1,X0) = app(cons(X1,nil),X0), inference(clausification, [status(esa)], [ax81])). % 36.16/56.87 cnf(c194, plain, ~ssList(X0) | app(X0,nil) = X0, inference(clausification, [status(esa)], [ax84])). % 36.16/56.87 cnf(c208, plain, ssList(sK254), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c209, plain, ssList(sK255), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c212, plain, sK255 = sK257, inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c213, plain, sK254 = sK256, inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c214, plain, ~X0(sK254,sK255,sK256,sK257) | neq(sK255,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c215, plain, ~X0(sK254,sK255,sK256,sK257) | ~neq(sK257,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c216, plain, X0(X1,X2,X3,X4) | neq(X2,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c217, plain, X0(X1,X2,X3,X4) | ssItem(sK258(X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c218, plain, X0(X1,X2,X3,X4) | ssList(sK259(X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c219, plain, X0(X1,X2,X3,X4) | app(cons(sK258(X3,X4),nil),sK259(X3,X4)) = X3, inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c220, plain, X0(X1,X2,X3,X4) | app(sK259(X3,X4),cons(sK258(X3,X4),nil)) = X4, inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(c221, plain, app(X0,X1) != X2 | hd(X3) != X4 | ~neq(nil,X3) | tl(X3) != X0 | ~neq(X3,nil) | ~ssList(X2) | cons(X4,nil) != X1 | X5(X3,X6,X7,X8) | ~ssItem(X4) | ~ssList(X1) | ~ssList(X0) | X6 != X2, inference(clausification, [status(esa)], [negated_conjecture])). % 36.16/56.87 cnf(d0, plain, ~neq(sK255,nil) | ~'Ts253'(sK254,sK255,sK256,sK257), inference(demodulation, [status(thm)], [c215,c212])). % 36.16/56.87 cnf(d1, plain, ~neq(sK255,nil) | ~'Ts253'(sK254,sK255,sK254,sK257), inference(demodulation, [status(thm)], [d0,c213])). % 36.16/56.87 cnf(d2, plain, ~neq(sK255,nil) | ~'Ts253'(sK254,sK255,sK254,sK255), inference(demodulation, [status(thm)], [d1,c212])). % 36.16/56.87 cnf(d3, plain, neq(sK255,nil) | ~'Ts253'(sK254,sK255,sK254,sK257), inference(demodulation, [status(thm)], [c214,c213])). % 36.16/56.87 cnf(d4, plain, neq(sK255,nil) | ~'Ts253'(sK254,sK255,sK254,sK255), inference(demodulation, [status(thm)], [d3,c212])). % 36.16/56.87 cnf(d5, plain, neq(sK255,nil) | neq(sK255,nil), inference(resolution, [status(thm)], [c216,d4])). % 36.16/56.87 cnf(d6, plain, ~'Ts253'(sK254,sK255,sK254,sK255), inference(resolution, [status(thm)], [d5,d2])). % 36.16/56.87 cnf(d7, plain, app(cons(sK258(sK254,sK255),nil),sK259(sK254,sK255)) = sK254, inference(resolution, [status(thm)], [c219,d6])). % 36.16/56.87 cnf(d8, plain, ssItem(sK258(sK254,sK255)), inference(resolution, [status(thm)], [c217,d6])). % 36.16/56.87 cnf(d9, plain, ssList(sK259(sK254,sK255)), inference(resolution, [status(thm)], [c218,d6])). % 36.16/56.87 cnf(d10, plain, cons(X0,sK259(sK254,sK255)) = app(cons(X0,nil),sK259(sK254,sK255)) | ~ssItem(X0), inference(resolution, [status(thm)], [c189,d9])). % 36.16/56.87 cnf(d11, plain, cons(sK258(sK254,sK255),sK259(sK254,sK255)) = app(cons(sK258(sK254,sK255),nil),sK259(sK254,sK255)), inference(resolution, [status(thm)], [d10,d8])). % 36.16/56.87 cnf(d12, plain, cons(sK258(sK254,sK255),sK259(sK254,sK255)) = sK254, inference(demodulation, [status(thm)], [d11,d7])). % 36.16/56.87 cnf(d13, plain, tl(cons(X0,sK259(sK254,sK255))) = sK259(sK254,sK255) | ~ssItem(X0), inference(resolution, [status(thm)], [c108,d9])). % 36.16/56.87 cnf(d14, plain, tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))) = sK259(sK254,sK255), inference(resolution, [status(thm)], [d13,d8])). % 36.16/56.87 cnf(d15, plain, tl(sK254) = sK259(sK254,sK255), inference(demodulation, [status(thm)], [d14,d12])). % 36.16/56.87 cnf(d16, plain, hd(cons(X0,sK259(sK254,sK255))) = X0 | ~ssItem(X0), inference(resolution, [status(thm)], [c106,d9])). % 36.16/56.87 cnf(d17, plain, hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))) = sK258(sK254,sK255), inference(resolution, [status(thm)], [d16,d8])). % 36.16/56.87 cnf(d18, plain, hd(sK254) = sK258(sK254,sK255), inference(demodulation, [status(thm)], [d17,d12])). % 36.16/56.87 cnf(d19, plain, app(sK259(sK254,sK255),cons(sK258(sK254,sK255),nil)) = sK255, inference(resolution, [status(thm)], [c220,d6])). % 36.16/56.87 cnf(d20, plain, app(sK259(sK254,sK255),cons(hd(sK254),nil)) = sK255, inference(demodulation, [status(thm)], [d19,d18])). % 36.16/56.87 cnf(d21, plain, app(tl(sK254),cons(hd(sK254),nil)) = sK255, inference(demodulation, [status(thm)], [d20,d15])). % 36.16/56.87 cnf(d22, plain, cons(hd(sK254),sK259(sK254,sK255)) = sK254, inference(demodulation, [status(thm)], [d12,d18])). % 36.16/56.87 cnf(d23, plain, cons(hd(sK254),tl(sK254)) = sK254, inference(demodulation, [status(thm)], [d22,d15])). % 36.16/56.87 cnf(d24, plain, X0 != X1 | app(X2,cons(X3,nil)) != X1 | hd(X4) != X3 | tl(X4) != X2 | ~ssItem(X3) | ~neq(X4,nil) | ~neq(nil,X4) | ~ssList(X2) | ~ssList(cons(X3,nil)) | ~ssList(X1) | 'Ts253'(X4,X0,X5,X6), inference(equality_resolution, [status(thm)], [c221])). % 36.16/56.87 cnf(d25, plain, X0 != app(X1,cons(X2,nil)) | hd(X3) != X2 | tl(X3) != X1 | ~ssItem(X2) | ~neq(X3,nil) | ~neq(nil,X3) | ~ssList(X1) | ~ssList(app(X1,cons(X2,nil))) | ~ssList(cons(X2,nil)) | 'Ts253'(X3,X0,X4,X5), inference(equality_resolution, [status(thm)], [d24])). % 36.16/56.87 cnf(d26, plain, hd(X0) != X1 | tl(X0) != X2 | ~ssItem(X1) | ~neq(X0,nil) | ~neq(nil,X0) | ~ssList(X2) | ~ssList(app(X2,cons(X1,nil))) | ~ssList(cons(X1,nil)) | 'Ts253'(X0,app(X2,cons(X1,nil)),X3,X4), inference(equality_resolution, [status(thm)], [d25])). % 36.16/56.87 cnf(d27, plain, hd(X0) != X1 | ~ssItem(X1) | ~neq(X0,nil) | ~neq(nil,X0) | ~ssList(tl(X0)) | ~ssList(app(tl(X0),cons(X1,nil))) | ~ssList(cons(X1,nil)) | 'Ts253'(X0,app(tl(X0),cons(X1,nil)),X2,X3), inference(equality_resolution, [status(thm)], [d26])). % 36.16/56.87 cnf(d28, plain, ~ssItem(hd(X0)) | ~neq(X0,nil) | ~neq(nil,X0) | ~ssList(app(tl(X0),cons(hd(X0),nil))) | ~ssList(cons(hd(X0),nil)) | ~ssList(tl(X0)) | 'Ts253'(X0,app(tl(X0),cons(hd(X0),nil)),X1,X2), inference(equality_resolution, [status(thm)], [d27])). % 36.16/56.87 cnf(d29, plain, 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1) | ~ssItem(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | ~neq(cons(sK258(sK254,sK255),sK259(sK254,sK255)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))), inference(superposition, [status(thm)], [d14,d28])). % 36.16/56.87 cnf(d30, plain, ~ssItem(hd(cons(hd(sK254),sK259(sK254,sK255)))) | ~neq(cons(sK258(sK254,sK255),sK259(sK254,sK255)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d29,d18])). % 36.16/56.87 cnf(d31, plain, ~ssItem(hd(cons(hd(sK254),tl(sK254)))) | ~neq(cons(sK258(sK254,sK255),sK259(sK254,sK255)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d30,d15])). % 36.16/56.87 cnf(d32, plain, ~ssItem(hd(sK254)) | ~neq(cons(sK258(sK254,sK255),sK259(sK254,sK255)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d31,d23])). % 36.16/56.87 cnf(d33, plain, ~ssItem(hd(sK254)) | ~neq(cons(hd(sK254),sK259(sK254,sK255)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d32,d18])). % 36.16/56.87 cnf(d34, plain, ~ssItem(hd(sK254)) | ~neq(cons(hd(sK254),tl(sK254)),nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d33,d15])). % 36.16/56.87 cnf(d35, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,cons(sK258(sK254,sK255),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d34,d23])). % 36.16/56.87 cnf(d36, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,cons(hd(sK254),sK259(sK254,sK255))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d35,d18])). % 36.16/56.87 cnf(d37, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,cons(hd(sK254),tl(sK254))) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d36,d15])). % 36.16/56.87 cnf(d38, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d37,d23])). % 36.16/56.87 cnf(d39, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(cons(hd(sK254),sK259(sK254,sK255))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d38,d18])). % 36.16/56.87 cnf(d40, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(cons(hd(sK254),tl(sK254))),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d39,d15])). % 36.16/56.87 cnf(d41, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(sK254),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d40,d23])). % 36.16/56.87 cnf(d42, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(sK254),cons(hd(cons(hd(sK254),sK259(sK254,sK255))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d41,d18])). % 36.16/56.87 cnf(d43, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(sK254),cons(hd(cons(hd(sK254),tl(sK254))),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d42,d15])). % 36.16/56.87 cnf(d44, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(app(tl(sK254),cons(hd(sK254),nil))) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d43,d23])). % 36.16/56.87 cnf(d45, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d44,d21])). % 36.16/56.87 cnf(d46, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(cons(hd(sK254),sK259(sK254,sK255))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d45,d18])). % 36.16/56.87 cnf(d47, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(cons(hd(sK254),tl(sK254))),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d46,d15])). % 36.16/56.87 cnf(d48, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(cons(sK258(sK254,sK255),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d47,d23])). % 36.16/56.87 cnf(d49, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(cons(hd(sK254),sK259(sK254,sK255)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d48,d18])). % 36.16/56.87 cnf(d50, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(cons(hd(sK254),tl(sK254)))) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d49,d15])). % 36.16/56.87 cnf(d51, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(cons(sK258(sK254,sK255),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d50,d23])). % 36.16/56.87 cnf(d52, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(cons(hd(sK254),sK259(sK254,sK255)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d51,d18])). % 36.16/56.87 cnf(d53, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(cons(hd(sK254),tl(sK254)),app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d52,d15])). % 36.16/56.87 cnf(d54, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,app(sK259(sK254,sK255),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d53,d23])). % 36.16/56.87 cnf(d55, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,app(tl(sK254),cons(hd(cons(sK258(sK254,sK255),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d54,d15])). % 36.16/56.87 cnf(d56, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,app(tl(sK254),cons(hd(cons(hd(sK254),sK259(sK254,sK255))),nil)),X0,X1), inference(demodulation, [status(thm)], [d55,d18])). % 36.16/56.87 cnf(d57, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,app(tl(sK254),cons(hd(cons(hd(sK254),tl(sK254))),nil)),X0,X1), inference(demodulation, [status(thm)], [d56,d15])). % 36.16/56.87 cnf(d58, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,app(tl(sK254),cons(hd(sK254),nil)),X0,X1), inference(demodulation, [status(thm)], [d57,d23])). % 36.16/56.87 cnf(d59, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(sK255) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,sK255,X0,X1), inference(demodulation, [status(thm)], [d58,d21])). % 36.16/56.87 cnf(d60, plain, ~ssItem(hd(sK254)) | ~neq(sK254,nil) | ~neq(nil,sK254) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,sK255,X0,X1), inference(resolution, [status(thm)], [c209,d59])). % 36.16/56.87 cnf(d61, plain, ssItem(hd(sK254)), inference(demodulation, [status(thm)], [d8,d18])). % 36.16/56.87 cnf(d62, plain, ~neq(nil,sK254) | ~neq(sK254,nil) | ~ssList(cons(hd(sK254),nil)) | ~ssList(tl(sK254)) | 'Ts253'(sK254,sK255,X0,X1), inference(resolution, [status(thm)], [d61,d60])). % 36.16/56.87 cnf(d63, plain, ssList(tl(sK254)), inference(demodulation, [status(thm)], [d9,d15])). % 36.16/56.87 cnf(d64, plain, ~neq(nil,sK254) | ~neq(sK254,nil) | ~ssList(cons(hd(sK254),nil)) | 'Ts253'(sK254,sK255,X0,X1), inference(resolution, [status(thm)], [d63,d62])). % 36.16/56.87 cnf(d65, plain, nil = sK254 | hd(sK254) = sK210(sK254), inference(resolution, [status(thm)], [c182,c208])). % 36.16/56.87 cnf(d66, plain, nil != sK254 | ~ssItem(hd(sK254)) | ~ssList(tl(sK254)), inference(superposition, [status(thm)], [d23,c104])). % 36.16/56.87 cnf(d67, plain, nil != sK254 | ~ssList(tl(sK254)), inference(resolution, [status(thm)], [d61,d66])). % 36.16/56.87 cnf(d68, plain, nil != sK254, inference(resolution, [status(thm)], [d63,d67])). % 36.16/56.87 cnf(d69, plain, hd(sK254) = sK210(sK254), inference(resolution, [status(thm)], [d68,d65])). % 36.16/56.87 cnf(d70, plain, hd(cons(X0,nil)) = X0 | ~ssItem(X0), inference(resolution, [status(thm)], [c106,c97])). % 36.16/56.87 cnf(d71, plain, hd(cons(sK210(X0),nil)) = sK210(X0) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d70,c181])). % 36.16/56.87 cnf(d72, plain, nil = sK254 | hd(cons(sK210(sK254),nil)) = sK210(sK254), inference(resolution, [status(thm)], [d71,c208])). % 36.16/56.87 cnf(d73, plain, hd(cons(X0,sK254)) = X0 | ~ssItem(X0), inference(resolution, [status(thm)], [c106,c208])). % 36.16/56.87 cnf(d74, plain, hd(cons(hd(X0),sK254)) = hd(X0) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d73,c105])). % 36.16/56.87 cnf(d75, plain, nil = sK254 | hd(cons(hd(sK254),sK254)) = hd(sK254), inference(resolution, [status(thm)], [d74,c208])). % 36.16/56.87 cnf(d76, plain, nil = X0 | ~ssList(X0) | hd(cons(sK210(X0),sK254)) = sK210(X0), inference(resolution, [status(thm)], [c181,d73])). % 36.16/56.87 cnf(d77, plain, nil = sK254 | hd(cons(sK210(sK254),sK254)) = sK210(sK254), inference(resolution, [status(thm)], [d76,c208])). % 36.16/56.87 cnf(d78, plain, hd(cons(hd(sK254),sK254)) = sK210(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d65,d77])). % 36.16/56.87 cnf(d79, plain, sK210(sK254) = hd(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d78,d75])). % 36.16/56.87 cnf(d80, plain, hd(cons(hd(sK254),nil)) = sK210(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d79,d72])). % 36.16/56.87 cnf(d81, plain, hd(cons(sK121(X0),nil)) = sK121(X0) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d70,c102])). % 36.16/56.87 cnf(d82, plain, nil = sK254 | hd(cons(sK121(sK254),nil)) = sK121(sK254), inference(resolution, [status(thm)], [d81,c208])). % 36.16/56.87 cnf(d83, plain, hd(cons(X0,sK120(X1))) = X0 | ~ssItem(X0) | nil = X1 | ~ssList(X1), inference(resolution, [status(thm)], [c106,c101])). % 36.16/56.87 cnf(d84, plain, nil = sK254 | hd(cons(X0,sK120(sK254))) = X0 | ~ssItem(X0), inference(resolution, [status(thm)], [d83,c208])). % 36.16/56.87 cnf(d85, plain, nil = sK254 | hd(cons(sK121(X0),sK120(sK254))) = sK121(X0) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d84,c102])). % 36.16/56.87 cnf(d86, plain, nil = sK254 | nil = sK254 | hd(cons(sK121(sK254),sK120(sK254))) = sK121(sK254), inference(resolution, [status(thm)], [d85,c208])). % 36.16/56.87 cnf(d87, plain, cons(sK121(sK254),sK120(sK254)) = sK254 | nil = sK254, inference(resolution, [status(thm)], [c103,c208])). % 36.16/56.87 cnf(d88, plain, hd(sK254) = sK121(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d87,d86])). % 36.16/56.87 cnf(d89, plain, hd(cons(hd(sK254),nil)) = sK121(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d88,d82])). % 36.16/56.87 cnf(d90, plain, sK121(sK254) = sK210(sK254) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d89,d80])). % 36.16/56.87 cnf(d91, plain, sK121(sK254) = sK210(sK254), inference(resolution, [status(thm)], [d68,d90])). % 36.16/56.87 cnf(d92, plain, sK121(sK254) = hd(sK254), inference(demodulation, [status(thm)], [d91,d69])). % 36.16/56.87 cnf(d93, plain, cons(X0,nil) = app(cons(X0,nil),nil) | ~ssItem(X0), inference(resolution, [status(thm)], [c189,c97])). % 36.16/56.87 cnf(d94, plain, cons(hd(X0),nil) = app(cons(hd(X0),nil),nil) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d93,c105])). % 36.16/56.87 cnf(d95, plain, cons(hd(sK254),nil) = app(cons(hd(sK254),nil),nil) | nil = sK254, inference(resolution, [status(thm)], [d94,c208])). % 36.16/56.87 cnf(d96, plain, cons(sK121(X0),nil) = app(cons(sK121(X0),nil),nil) | nil = X0 | ~ssList(X0), inference(resolution, [status(thm)], [d93,c102])). % 36.16/56.87 cnf(d97, plain, cons(sK121(sK254),nil) = app(cons(sK121(sK254),nil),nil) | nil = sK254, inference(resolution, [status(thm)], [d96,c208])). % 36.16/56.87 cnf(d98, plain, cons(sK121(sK254),nil) = app(cons(hd(sK254),nil),nil) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d88,d97])). % 36.16/56.87 cnf(d99, plain, cons(hd(sK254),nil) = cons(sK121(sK254),nil) | nil = sK254 | nil = sK254, inference(superposition, [status(thm)], [d98,d95])). % 36.16/56.87 cnf(d100, plain, ssList(cons(hd(sK254),nil)) | ~ssItem(sK121(sK254)) | ~ssList(nil) | nil = sK254, inference(superposition, [status(thm)], [d99,c96])). % 36.16/56.87 cnf(d101, plain, nil = sK254 | ~ssItem(sK121(sK254)) | ssList(cons(hd(sK254),nil)), inference(resolution, [status(thm)], [c97,d100])). % 36.16/56.87 cnf(d102, plain, ~ssItem(sK121(sK254)) | ssList(cons(hd(sK254),nil)), inference(resolution, [status(thm)], [d68,d101])). % 36.16/56.87 cnf(d103, plain, ~ssItem(hd(sK254)) | ssList(cons(hd(sK254),nil)), inference(demodulation, [status(thm)], [d102,d92])). % 36.16/56.87 cnf(d104, plain, ssList(cons(hd(sK254),nil)), inference(resolution, [status(thm)], [d61,d103])). % 36.16/56.87 cnf(d105, plain, ~neq(nil,sK254) | ~neq(sK254,nil) | 'Ts253'(sK254,sK255,X0,X1), inference(resolution, [status(thm)], [d104,d64])). % 36.16/56.87 cnf(d106, plain, ~neq(nil,sK254) | ~neq(sK254,nil), inference(resolution, [status(thm)], [d105,d6])). % 36.16/56.87 cnf(d107, plain, ~neq(nil,sK254) | sK254 = nil | ~ssList(nil) | ~ssList(sK254), inference(resolution, [status(thm)], [d106,c95])). % 36.16/56.87 cnf(d108, plain, sK254 = nil | ~neq(nil,sK254) | ~ssList(nil), inference(resolution, [status(thm)], [c208,d107])). % 36.16/56.87 cnf(d109, plain, sK254 = nil | ~neq(nil,sK254), inference(resolution, [status(thm)], [c97,d108])). % 36.16/56.87 cnf(d110, plain, sK254 = nil | nil = sK254 | ~ssList(sK254) | ~ssList(nil), inference(resolution, [status(thm)], [d109,c95])). % 36.16/56.87 cnf(d111, plain, nil = sK254 | sK254 = nil | ~ssList(nil), inference(resolution, [status(thm)], [c208,d110])). % 36.16/56.87 cnf(d112, plain, nil = sK254 | sK254 = nil, inference(resolution, [status(thm)], [c97,d111])). % 36.16/56.87 cnf(d113, plain, sK254 = nil, inference(resolution, [status(thm)], [d68,d112])). % 36.16/56.87 cnf(d114, plain, sK254 != X0 | ~ssList(cons(sK258(sK254,sK255),nil)) | ~ssList(X0) | ~ssList(sK259(sK254,sK255)) | rearsegP(X0,sK259(sK254,sK255)), inference(superposition, [status(thm)], [d7,c17])). % 36.16/56.87 cnf(d115, plain, sK254 != X0 | ~ssList(X0) | ~ssList(cons(sK258(sK254,sK255),nil)) | rearsegP(X0,sK259(sK254,sK255)), inference(resolution, [status(thm)], [d9,d114])). % 36.16/56.87 cnf(d116, plain, ~ssList(sK254) | ~ssList(cons(sK258(sK254,sK255),nil)) | rearsegP(sK254,sK259(sK254,sK255)), inference(equality_resolution, [status(thm)], [d115])). % 36.16/56.87 cnf(d117, plain, ~ssList(cons(sK258(sK254,sK255),nil)) | rearsegP(sK254,sK259(sK254,sK255)), inference(resolution, [status(thm)], [c208,d116])). % 36.16/56.87 cnf(d118, plain, ~ssItem(sK258(sK254,sK255)) | ~ssList(nil) | rearsegP(sK254,sK259(sK254,sK255)), inference(resolution, [status(thm)], [c96,d117])). % 36.16/56.87 cnf(d119, plain, ~ssList(nil) | rearsegP(sK254,sK259(sK254,sK255)), inference(resolution, [status(thm)], [d8,d118])). % 36.16/56.87 cnf(d120, plain, rearsegP(sK254,sK259(sK254,sK255)), inference(resolution, [status(thm)], [c97,d119])). % 36.16/56.87 cnf(d121, plain, app(sK259(sK254,sK255),nil) = sK259(sK254,sK255), inference(resolution, [status(thm)], [c194,d9])). % 36.16/56.87 cnf(d122, plain, ~ssList(X0) | ~ssList(X1) | ~ssList(X2) | ~rearsegP(X1,X2) | X2 = app(X0,X1) | ~ssList(X2) | ~ssList(app(X0,X1)) | ~rearsegP(X2,app(X0,X1)), inference(resolution, [status(thm)], [c142,c140])). % 36.16/56.87 cnf(d123, plain, ~rearsegP(X0,sK259(sK254,sK255)) | X0 = app(sK259(sK254,sK255),nil) | ~ssList(X0) | ~ssList(nil) | ~ssList(sK259(sK254,sK255)) | ~ssList(app(sK259(sK254,sK255),nil)) | ~rearsegP(nil,X0), inference(superposition, [status(thm)], [d121,d122])). % 36.16/56.87 cnf(d124, plain, X0 = sK259(sK254,sK255) | ~ssList(X0) | ~ssList(app(sK259(sK254,sK255),nil)) | ~ssList(nil) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(X0,sK259(sK254,sK255)) | ~rearsegP(nil,X0), inference(demodulation, [status(thm)], [d123,d121])). % 36.16/56.87 cnf(d125, plain, X0 = sK259(sK254,sK255) | ~ssList(X0) | ~ssList(sK259(sK254,sK255)) | ~ssList(nil) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(X0,sK259(sK254,sK255)) | ~rearsegP(nil,X0), inference(demodulation, [status(thm)], [d124,d121])). % 36.16/56.87 cnf(d126, plain, X0 = sK259(sK254,sK255) | ~ssList(X0) | ~ssList(nil) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(X0,sK259(sK254,sK255)) | ~rearsegP(nil,X0), inference(resolution, [status(thm)], [d9,d125])). % 36.16/56.87 cnf(d127, plain, X0 = sK259(sK254,sK255) | ~ssList(X0) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(X0,sK259(sK254,sK255)) | ~rearsegP(nil,X0), inference(resolution, [status(thm)], [c97,d126])). % 36.16/56.87 cnf(d128, plain, sK254 = sK259(sK254,sK255) | ~ssList(sK254) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(nil,sK254), inference(resolution, [status(thm)], [d127,d120])). % 36.16/56.87 cnf(d129, plain, sK254 = sK259(sK254,sK255) | ~ssList(sK259(sK254,sK255)) | ~rearsegP(nil,sK254), inference(resolution, [status(thm)], [c208,d128])). % 36.16/56.87 cnf(d130, plain, sK254 = sK259(sK254,sK255) | ~rearsegP(nil,sK254), inference(resolution, [status(thm)], [d9,d129])). % 36.16/56.87 cnf(d131, plain, sK254 = tl(sK254) | ~rearsegP(nil,sK254), inference(demodulation, [status(thm)], [d130,d15])). % 36.16/56.87 cnf(d132, plain, cons(hd(sK254),tl(sK254)) = sK254 | nil = sK254, inference(resolution, [status(thm)], [c186,c208])). % 36.16/56.87 cnf(d133, plain, sK254 != tl(sK254) | ~ssItem(hd(sK254)) | ~ssList(tl(sK254)) | nil = sK254, inference(superposition, [status(thm)], [d132,c98])). % 36.16/56.87 cnf(d134, plain, nil = sK254 | sK254 != tl(sK254) | ~ssList(tl(sK254)), inference(resolution, [status(thm)], [d61,d133])). % 36.16/56.87 cnf(d135, plain, nil = sK254 | sK254 != tl(sK254), inference(resolution, [status(thm)], [d63,d134])). % 36.16/56.87 cnf(d136, plain, sK254 != tl(sK254), inference(resolution, [status(thm)], [d68,d135])). % 36.16/56.87 cnf(d137, plain, ~rearsegP(nil,sK254), inference(resolution, [status(thm)], [d136,d131])). % 36.16/56.87 cnf(d138, plain, ~rearsegP(nil,nil), inference(demodulation, [status(thm)], [d137,d113])). % 36.16/56.87 cnf(d139, plain, ~ssList(nil), inference(resolution, [status(thm)], [d138,c143])). % 36.16/56.87 cnf(d140, plain, $false, inference(resolution, [status(thm)], [c97,d139])). % 36.16/56.87 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------