%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SWC284+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 : n016.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:51 AM UTC 2026 % Result : Theorem 101.50s 15.52s % Output : CNFRefutation 101.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC284+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 : n016.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:46:30 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 101.50/15.52 % SZS status Theorem for theBenchmark.p % 101.50/15.52 % SZS output start CNFRefutation for theBenchmark.p % 101.50/15.52 fof(ax3, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => (memberP(X0,X1) <=> ? [X2] : ((ssList(X2) & ? [X3] : ((ssList(X3) & app(X2,cons(X1,X3)) = X0)))))))))). % 101.50/15.52 fof(ax4, axiom, ! [X0] : ((ssList(X0) => (singletonP(X0) <=> ? [X1] : ((ssItem(X1) & cons(X1,nil) = X0)))))). % 101.50/15.52 fof(ax5, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (frontsegP(X0,X1) <=> ? [X2] : ((ssList(X2) & app(X1,X2) = X0)))))))). % 101.50/15.52 fof(ax6, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (rearsegP(X0,X1) <=> ? [X2] : ((ssList(X2) & app(X2,X1) = X0)))))))). % 101.50/15.52 fof(ax7, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (segmentP(X0,X1) <=> ? [X2] : ((ssList(X2) & ? [X3] : ((ssList(X3) & app(app(X2,X1),X3) = X0)))))))))). % 101.50/15.52 fof(ax11, axiom, ! [X0] : ((ssList(X0) => (totalorderedP(X0) <=> ! [X1] : ((ssItem(X1) => ! [X2] : ((ssItem(X2) => ! [X3] : ((ssList(X3) => ! [X4] : ((ssList(X4) => ! [X5] : ((ssList(X5) => (app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0 => leq(X1,X2)))))))))))))))). % 101.50/15.52 fof(ax15, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => (neq(X0,X1) <=> X0 != X1)))))). % 101.50/15.52 fof(ax16, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => ssList(cons(X1,X0))))))). % 101.50/15.52 fof(ax17, axiom, ssList(nil)). % 101.50/15.52 fof(ax18, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => cons(X1,X0) != X0))))). % 101.50/15.52 fof(ax23, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => hd(cons(X1,X0)) = X1))))). % 101.50/15.52 fof(ax26, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ssList(app(X0,X1))))))). % 101.50/15.52 fof(ax31, axiom, ! [X0] : ((ssItem(X0) => leq(X0,X0)))). % 101.50/15.52 fof(ax36, axiom, ! [X0] : ((ssItem(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => (memberP(app(X1,X2),X0) <=> (memberP(X1,X0) | memberP(X2,X0)))))))))). % 101.50/15.52 fof(ax37, axiom, ! [X0] : ((ssItem(X0) => ! [X1] : ((ssItem(X1) => ! [X2] : ((ssList(X2) => (memberP(cons(X1,X2),X0) <=> (X0 = X1 | memberP(X2,X0)))))))))). % 101.50/15.52 fof(ax38, axiom, ! [X0] : ((ssItem(X0) => ~memberP(nil,X0)))). % 101.50/15.52 fof(ax39, axiom, ~singletonP(nil)). % 101.50/15.52 fof(ax45, axiom, ! [X0] : ((ssList(X0) => frontsegP(X0,nil)))). % 101.50/15.52 fof(ax48, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ((rearsegP(X0,X1) & rearsegP(X1,X0)) => X0 = X1)))))). % 101.50/15.52 fof(ax51, axiom, ! [X0] : ((ssList(X0) => rearsegP(X0,nil)))). % 101.50/15.52 fof(ax54, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ((segmentP(X0,X1) & segmentP(X1,X0)) => X0 = X1)))))). % 101.50/15.52 fof(ax58, axiom, ! [X0] : ((ssList(X0) => (segmentP(nil,X0) <=> nil = X0)))). % 101.50/15.52 fof(ax65, axiom, ! [X0] : ((ssItem(X0) => totalorderedP(cons(X0,nil))))). % 101.50/15.52 fof(ax67, axiom, ! [X0] : ((ssItem(X0) => ! [X1] : ((ssList(X1) => (totalorderedP(cons(X0,X1)) <=> (nil = X1 | (nil != X1 & (totalorderedP(X1) & leq(X0,hd(X1))))))))))). % 101.50/15.52 fof(ax81, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => cons(X1,X0) = app(cons(X1,nil),X0)))))). % 101.50/15.52 fof(ax82, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => app(app(X0,X1),X2) = app(X0,app(X1,X2))))))))). % 101.50/15.52 fof(co1, conjecture, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((~ssList(X3) | (X1 != X3 | (X0 != X2 | (! [X4] : ((ssItem(X4) => ! [X5] : ((ssList(X5) => ! [X6] : ((~ssList(X6) | (app(app(X5,cons(X4,nil)),X6) != X0 | ! [X7] : ((ssItem(X7) => ((~memberP(X5,X7) | leq(X7,X4)) & (~memberP(X6,X7) | leq(X4,X7)))))))))))) | ((nil != X2 & nil = X3) | (! [X8] : ((~ssItem(X8) | (cons(X8,nil) != X2 | ~memberP(X3,X8)))) & neq(X3,nil))))))))))))))). % 101.50/15.52 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((~ssList(X3) | (X1 != X3 | (X0 != X2 | (! [X4] : ((ssItem(X4) => ! [X5] : ((ssList(X5) => ! [X6] : ((~ssList(X6) | (app(app(X5,cons(X4,nil)),X6) != X0 | ! [X7] : ((ssItem(X7) => ((~memberP(X5,X7) | leq(X7,X4)) & (~memberP(X6,X7) | leq(X4,X7)))))))))))) | ((nil != X2 & nil = X3) | (! [X8] : ((~ssItem(X8) | (cons(X8,nil) != X2 | ~memberP(X3,X8)))) & neq(X3,nil)))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 101.50/15.52 cnf(c8, plain, ~ssItem(X0) | ~ssList(X1) | memberP(X2,X0) | ~ssList(X2) | app(X1,cons(X0,X3)) != X2 | ~ssList(X3), inference(clausification, [status(esa)], [ax3])). % 101.50/15.52 cnf(c11, plain, ~ssList(X0) | singletonP(X0) | ~ssItem(X1) | cons(X1,nil) != X0, inference(clausification, [status(esa)], [ax4])). % 101.50/15.52 cnf(c12, plain, ~ssList(X0) | ~ssList(X1) | ~frontsegP(X0,X1) | ssList(sK15(X0,X1)), inference(clausification, [status(esa)], [ax5])). % 101.50/15.52 cnf(c13, plain, ~ssList(X0) | ~ssList(X1) | ~frontsegP(X0,X1) | app(X1,sK15(X0,X1)) = X0, inference(clausification, [status(esa)], [ax5])). % 101.50/15.52 cnf(c17, plain, ~ssList(X0) | rearsegP(X1,X2) | ~ssList(X1) | ~ssList(X2) | app(X0,X2) != X1, inference(clausification, [status(esa)], [ax6])). % 101.50/15.52 cnf(c21, plain, segmentP(X0,X1) | ~ssList(X1) | app(app(X2,X1),X3) != X0 | ~ssList(X3) | ~ssList(X0) | ~ssList(X2), inference(clausification, [status(esa)], [ax7])). % 101.50/15.52 cnf(c55, plain, ~ssList(X0) | ~totalorderedP(X0) | X1(X0), inference(clausification, [status(esa)], [ax11])). % 101.50/15.52 cnf(c56, plain, ~ssList(X0) | totalorderedP(X0) | ~X1(X0), inference(clausification, [status(esa)], [ax11])). % 101.50/15.52 cnf(c95, plain, ~ssList(X0) | ~ssList(X1) | neq(X0,X1) | X0 = X1, inference(clausification, [status(esa)], [ax15])). % 101.50/15.52 cnf(c96, plain, ~ssList(X0) | ~ssItem(X1) | ssList(cons(X1,X0)), inference(clausification, [status(esa)], [ax16])). % 101.50/15.52 cnf(c97, plain, ssList(nil), inference(clausification, [status(esa)], [ax17])). % 101.50/15.52 cnf(c98, plain, ~ssList(X0) | ~ssItem(X1) | cons(X1,X0) != X0, inference(clausification, [status(esa)], [ax18])). % 101.50/15.52 cnf(c106, plain, ~ssList(X0) | ~ssItem(X1) | hd(cons(X1,X0)) = X1, inference(clausification, [status(esa)], [ax23])). % 101.50/15.52 cnf(c109, plain, ~ssList(X0) | ~ssList(X1) | ssList(app(X0,X1)), inference(clausification, [status(esa)], [ax26])). % 101.50/15.52 cnf(c114, plain, ~ssItem(X0) | leq(X0,X0), inference(clausification, [status(esa)], [ax31])). % 101.50/15.52 cnf(c122, plain, ~ssItem(X0) | ~ssList(X1) | ~ssList(X2) | memberP(app(X2,X1),X0) | ~memberP(X2,X0), inference(clausification, [status(esa)], [ax36])). % 101.50/15.52 cnf(c123, plain, ~memberP(X0,X1) | ~ssItem(X1) | ~ssList(X0) | memberP(app(X2,X0),X1) | ~ssList(X2), inference(clausification, [status(esa)], [ax36])). % 101.50/15.52 cnf(c124, plain, ~memberP(cons(X0,X1),X2) | X2 = X0 | ~ssList(X1) | ~ssItem(X0) | ~ssItem(X2) | memberP(X1,X2), inference(clausification, [status(esa)], [ax37])). % 101.50/15.52 cnf(c127, plain, ~ssItem(X0) | ~memberP(nil,X0), inference(clausification, [status(esa)], [ax38])). % 101.50/15.52 cnf(c128, plain, ~singletonP(nil), inference(clausification, [status(esa)], [ax39])). % 101.50/15.52 cnf(c136, plain, ~ssList(X0) | frontsegP(X0,nil), inference(clausification, [status(esa)], [ax45])). % 101.50/15.52 cnf(c140, plain, X0 = X1 | ~rearsegP(X0,X1) | ~rearsegP(X1,X0) | ~ssList(X1) | ~ssList(X0), inference(clausification, [status(esa)], [ax48])). % 101.50/15.52 cnf(c143, plain, ~ssList(X0) | rearsegP(X0,nil), inference(clausification, [status(esa)], [ax51])). % 101.50/15.52 cnf(c147, plain, ~segmentP(X0,X1) | X0 = X1 | ~segmentP(X1,X0) | ~ssList(X1) | ~ssList(X0), inference(clausification, [status(esa)], [ax54])). % 101.50/15.52 cnf(c151, plain, ~ssList(X0) | ~segmentP(nil,X0) | nil = X0, inference(clausification, [status(esa)], [ax58])). % 101.50/15.52 cnf(c159, plain, ~ssItem(X0) | totalorderedP(cons(X0,nil)), inference(clausification, [status(esa)], [ax65])). % 101.50/15.52 cnf(c165, plain, ~X0(X1,X2) | nil = X2 | leq(X1,hd(X2)), inference(clausification, [status(esa)], [ax67])). % 101.50/15.52 cnf(c167, plain, X0(X1,X2) | nil = X2 | ~totalorderedP(X2) | ~leq(X1,hd(X2)), inference(clausification, [status(esa)], [ax67])). % 101.50/15.52 cnf(c189, plain, ~ssList(X0) | ~ssItem(X1) | cons(X1,X0) = app(cons(X1,nil),X0), inference(clausification, [status(esa)], [ax81])). % 101.50/15.52 cnf(c190, plain, ~ssList(X0) | ~ssList(X1) | ~ssList(X2) | app(app(X0,X1),X2) = app(X0,app(X1,X2)), inference(clausification, [status(esa)], [ax82])). % 101.50/15.52 cnf(c210, plain, ssList(sK255), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c211, plain, ssList(sK256), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c213, plain, sK253 = sK255, inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c214, plain, ssItem(sK257), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c215, plain, ssList(sK258), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c216, plain, ssList(sK259), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c217, plain, app(app(sK258,cons(sK257,nil)),sK259) = sK253, inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c218, plain, ssItem(sK260), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c219, plain, memberP(sK258,sK260) | memberP(sK259,sK260), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c222, plain, ~leq(sK260,sK257) | ~leq(sK257,sK260), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c223, plain, nil = sK255 | nil != sK256, inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c224, plain, ssItem(sK261) | ~neq(sK256,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(c225, plain, cons(sK261,nil) = sK255 | ~neq(sK256,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 101.50/15.52 cnf(d0, plain, hd(sK255) = sK261 | ~ssItem(sK261) | ~ssList(nil) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,c106])). % 101.50/15.52 cnf(d1, plain, hd(sK255) = sK261 | ~ssItem(sK261) | ~neq(sK256,nil), inference(resolution, [status(thm)], [c97,d0])). % 101.50/15.52 cnf(d2, plain, app(app(sK258,cons(sK257,nil)),sK259) = sK255, inference(demodulation, [status(thm)], [c217,c213])). % 101.50/15.52 cnf(d3, plain, sK255 != X0 | ~ssList(X0) | ~ssList(sK259) | ~ssList(cons(sK257,nil)) | ~ssList(sK258) | segmentP(X0,cons(sK257,nil)), inference(superposition, [status(thm)], [d2,c21])). % 101.50/15.52 cnf(d4, plain, sK255 != X0 | ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK259) | segmentP(X0,cons(sK257,nil)), inference(resolution, [status(thm)], [c215,d3])). % 101.50/15.52 cnf(d5, plain, sK255 != X0 | ~ssList(X0) | ~ssList(cons(sK257,nil)) | segmentP(X0,cons(sK257,nil)), inference(resolution, [status(thm)], [c216,d4])). % 101.50/15.52 cnf(d6, plain, ~ssList(sK255) | ~ssList(cons(sK257,nil)) | segmentP(sK255,cons(sK257,nil)), inference(equality_resolution, [status(thm)], [d5])). % 101.50/15.52 cnf(d7, plain, ~ssList(cons(sK257,nil)) | segmentP(sK255,cons(sK257,nil)), inference(resolution, [status(thm)], [c210,d6])). % 101.50/15.52 cnf(d8, plain, sK256 = nil | ~ssList(nil) | ~ssList(sK256) | ssItem(sK261), inference(resolution, [status(thm)], [c95,c224])). % 101.50/15.52 cnf(d9, plain, sK256 = nil | ssItem(sK261) | ~ssList(nil), inference(resolution, [status(thm)], [c211,d8])). % 101.50/15.52 cnf(d10, plain, sK256 = nil | ssItem(sK261), inference(resolution, [status(thm)], [c97,d9])). % 101.50/15.52 cnf(d11, plain, nil != nil | nil = sK255 | ssItem(sK261), inference(superposition, [status(thm)], [d10,c223])). % 101.50/15.52 cnf(d12, plain, nil = sK255 | ssItem(sK261), inference(equality_resolution, [status(thm)], [d11])). % 101.50/15.52 cnf(d13, plain, segmentP(nil,cons(sK257,nil)) | ~ssList(cons(sK257,nil)) | ssItem(sK261), inference(superposition, [status(thm)], [d12,d7])). % 101.50/15.52 cnf(d14, plain, nil = cons(sK257,nil) | ~ssList(cons(sK257,nil)) | ssItem(sK261) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c151,d13])). % 101.50/15.52 cnf(d15, plain, nil != nil | ~ssItem(sK257) | ~ssList(nil) | ssItem(sK261) | ~ssList(cons(sK257,nil)), inference(superposition, [status(thm)], [d14,c98])). % 101.50/15.52 cnf(d16, plain, nil != nil | ssItem(sK261) | ~ssList(cons(sK257,nil)) | ~ssList(nil), inference(resolution, [status(thm)], [c214,d15])). % 101.50/15.52 cnf(d17, plain, nil != nil | ssItem(sK261) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c97,d16])). % 101.50/15.52 cnf(d18, plain, ssItem(sK261) | ~ssList(cons(sK257,nil)), inference(equality_resolution, [status(thm)], [d17])). % 101.50/15.52 cnf(d19, plain, ssItem(sK261) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d18,c96])). % 101.50/15.52 cnf(d20, plain, ssItem(sK261) | ~ssList(nil), inference(resolution, [status(thm)], [c214,d19])). % 101.50/15.52 cnf(d21, plain, ssItem(sK261), inference(resolution, [status(thm)], [c97,d20])). % 101.50/15.52 cnf(d22, plain, hd(sK255) = sK261 | ~neq(sK256,nil), inference(resolution, [status(thm)], [d21,d1])). % 101.50/15.52 cnf(d23, plain, leq(X0,sK261) | nil = sK255 | ~'Ts200'(X0,sK255) | ~neq(sK256,nil), inference(superposition, [status(thm)], [d22,c165])). % 101.50/15.52 cnf(d24, plain, ~leq(X0,sK261) | nil = sK255 | ~totalorderedP(sK255) | 'Ts200'(X0,sK255) | ~neq(sK256,nil), inference(superposition, [status(thm)], [d22,c167])). % 101.50/15.52 cnf(d25, plain, app(sK255,X0) != X1 | ~ssList(X1) | ~ssList(X0) | ~ssList(sK259) | ~ssList(app(sK258,cons(sK257,nil))) | segmentP(X1,sK259), inference(superposition, [status(thm)], [d2,c21])). % 101.50/15.52 cnf(d26, plain, app(sK255,X0) != X1 | ~ssList(X1) | ~ssList(X0) | ~ssList(app(sK258,cons(sK257,nil))) | segmentP(X1,sK259), inference(resolution, [status(thm)], [c216,d25])). % 101.50/15.52 cnf(d27, plain, X0 != X1 | ~ssList(X1) | ~ssList(sK15(X0,sK255)) | ~ssList(app(sK258,cons(sK257,nil))) | segmentP(X1,sK259) | ~ssList(sK255) | ~ssList(X0) | ~frontsegP(X0,sK255), inference(superposition, [status(thm)], [c13,d26])). % 101.50/15.52 cnf(d28, plain, X0 != X1 | ~ssList(X1) | ~ssList(X0) | ~ssList(app(sK258,cons(sK257,nil))) | ~ssList(sK15(X0,sK255)) | ~frontsegP(X0,sK255) | segmentP(X1,sK259), inference(resolution, [status(thm)], [c210,d27])). % 101.50/15.52 cnf(d29, plain, ~ssList(X0) | ~ssList(X0) | ~ssList(app(sK258,cons(sK257,nil))) | ~ssList(sK15(X0,sK255)) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(equality_resolution, [status(thm)], [d28])). % 101.50/15.52 cnf(d30, plain, ~ssList(cons(sK257,nil)) | ~ssList(sK258) | ~ssList(X0) | ~ssList(sK15(X0,sK255)) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(resolution, [status(thm)], [c109,d29])). % 101.50/15.52 cnf(d31, plain, ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK15(X0,sK255)) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(resolution, [status(thm)], [c215,d30])). % 101.50/15.52 cnf(d32, plain, ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~frontsegP(X0,sK255) | segmentP(X0,sK259) | ~ssList(sK255) | ~ssList(X0) | ~frontsegP(X0,sK255), inference(resolution, [status(thm)], [d31,c12])). % 101.50/15.52 cnf(d33, plain, ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(resolution, [status(thm)], [c210,d32])). % 101.50/15.52 cnf(d34, plain, ~ssList(X0) | ~frontsegP(X0,sK255) | segmentP(X0,sK259) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d33,c96])). % 101.50/15.52 cnf(d35, plain, ~ssList(X0) | ~ssList(nil) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(resolution, [status(thm)], [c214,d34])). % 101.50/15.52 cnf(d36, plain, ~ssList(X0) | ~frontsegP(X0,sK255) | segmentP(X0,sK259), inference(resolution, [status(thm)], [c97,d35])). % 101.50/15.52 cnf(d37, plain, ~ssList(cons(X0,nil)) | 'Ts63'(cons(X0,nil)) | ~ssItem(X0), inference(resolution, [status(thm)], [c55,c159])). % 101.50/15.52 cnf(d38, plain, ~ssList(sK255) | ~ssItem(sK261) | 'Ts63'(cons(sK261,nil)) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,d37])). % 101.50/15.52 cnf(d39, plain, ~ssItem(sK261) | ~neq(sK256,nil) | 'Ts63'(cons(sK261,nil)), inference(resolution, [status(thm)], [c210,d38])). % 101.50/15.52 cnf(d40, plain, 'Ts63'(sK255) | ~ssItem(sK261) | ~neq(sK256,nil) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,d39])). % 101.50/15.52 cnf(d41, plain, ~ssItem(sK261) | 'Ts63'(sK255) | sK256 = nil | ~ssList(nil) | ~ssList(sK256), inference(resolution, [status(thm)], [d40,c95])). % 101.50/15.52 cnf(d42, plain, sK256 = nil | ~ssItem(sK261) | ~ssList(nil) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c211,d41])). % 101.50/15.52 cnf(d43, plain, sK256 = nil | ~ssItem(sK261) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c97,d42])). % 101.50/15.52 cnf(d44, plain, nil != nil | nil = sK255 | ~ssItem(sK261) | 'Ts63'(sK255), inference(superposition, [status(thm)], [d43,c223])). % 101.50/15.52 cnf(d45, plain, nil = sK255 | ~ssItem(sK261) | 'Ts63'(sK255), inference(equality_resolution, [status(thm)], [d44])). % 101.50/15.52 cnf(d46, plain, ~frontsegP(X0,nil) | ~ssList(X0) | segmentP(X0,sK259) | ~ssItem(sK261) | 'Ts63'(sK255), inference(superposition, [status(thm)], [d45,d36])). % 101.50/15.52 cnf(d47, plain, ~ssItem(sK261) | ~ssList(X0) | segmentP(X0,sK259) | 'Ts63'(sK255) | ~ssList(X0), inference(resolution, [status(thm)], [d46,c136])). % 101.50/15.52 cnf(d48, plain, ~ssList(X0) | segmentP(X0,sK259) | 'Ts63'(sK255), inference(resolution, [status(thm)], [d21,d47])). % 101.50/15.52 cnf(d49, plain, ~ssList(X0) | 'Ts63'(sK255) | X0 = sK259 | ~ssList(sK259) | ~ssList(X0) | ~segmentP(sK259,X0), inference(resolution, [status(thm)], [d48,c147])). % 101.50/15.52 cnf(d50, plain, X0 = sK259 | ~ssList(X0) | ~segmentP(sK259,X0) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c216,d49])). % 101.50/15.52 cnf(d51, plain, sK255 != X0 | ~ssList(app(sK258,cons(sK257,nil))) | ~ssList(X0) | ~ssList(sK259) | rearsegP(X0,sK259), inference(superposition, [status(thm)], [d2,c17])). % 101.50/15.52 cnf(d52, plain, sK255 != X0 | ~ssList(X0) | ~ssList(app(sK258,cons(sK257,nil))) | rearsegP(X0,sK259), inference(resolution, [status(thm)], [c216,d51])). % 101.50/15.52 cnf(d53, plain, ~ssList(sK255) | ~ssList(app(sK258,cons(sK257,nil))) | rearsegP(sK255,sK259), inference(equality_resolution, [status(thm)], [d52])). % 101.50/15.52 cnf(d54, plain, ~ssList(app(sK258,cons(sK257,nil))) | rearsegP(sK255,sK259), inference(resolution, [status(thm)], [c210,d53])). % 101.50/15.52 cnf(d55, plain, ~ssList(cons(sK257,nil)) | ~ssList(sK258) | rearsegP(sK255,sK259), inference(resolution, [status(thm)], [c109,d54])). % 101.50/15.52 cnf(d56, plain, ~ssList(cons(sK257,nil)) | rearsegP(sK255,sK259), inference(resolution, [status(thm)], [c215,d55])). % 101.50/15.52 cnf(d57, plain, rearsegP(sK255,sK259) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d56,c96])). % 101.50/15.52 cnf(d58, plain, ~ssList(nil) | rearsegP(sK255,sK259), inference(resolution, [status(thm)], [c214,d57])). % 101.50/15.52 cnf(d59, plain, rearsegP(sK255,sK259), inference(resolution, [status(thm)], [c97,d58])). % 101.50/15.52 cnf(d60, plain, sK259 = sK255 | ~ssList(sK259) | ~ssList(sK255) | ~rearsegP(sK259,sK255), inference(resolution, [status(thm)], [c140,d59])). % 101.50/15.52 cnf(d61, plain, sK259 = sK255 | ~ssList(sK259) | ~rearsegP(sK259,sK255), inference(resolution, [status(thm)], [c210,d60])). % 101.50/15.52 cnf(d62, plain, sK259 = sK255 | ~rearsegP(sK259,sK255), inference(resolution, [status(thm)], [c216,d61])). % 101.50/15.52 cnf(d63, plain, ~rearsegP(sK259,nil) | sK259 = sK255 | ~ssItem(sK261) | 'Ts63'(sK255), inference(superposition, [status(thm)], [d45,d62])). % 101.50/15.52 cnf(d64, plain, sK259 = sK255 | ~ssItem(sK261) | 'Ts63'(sK255) | ~ssList(sK259), inference(resolution, [status(thm)], [d63,c143])). % 101.50/15.52 cnf(d65, plain, sK259 = sK255 | ~ssItem(sK261) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c216,d64])). % 101.50/15.52 cnf(d66, plain, sK259 = sK255 | 'Ts63'(sK255), inference(resolution, [status(thm)], [d21,d65])). % 101.50/15.52 cnf(d67, plain, ~segmentP(sK255,X0) | X0 = sK259 | ~ssList(X0) | 'Ts63'(sK255) | 'Ts63'(sK255), inference(superposition, [status(thm)], [d66,d50])). % 101.50/15.52 cnf(d68, plain, cons(sK257,nil) = sK259 | ~ssList(cons(sK257,nil)) | 'Ts63'(sK255) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [d67,d7])). % 101.50/15.52 cnf(d69, plain, totalorderedP(sK259) | ~ssItem(sK257) | ~ssList(cons(sK257,nil)) | 'Ts63'(sK255), inference(superposition, [status(thm)], [d68,c159])). % 101.50/15.52 cnf(d70, plain, ~ssList(cons(sK257,nil)) | totalorderedP(sK259) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c214,d69])). % 101.50/15.52 cnf(d71, plain, totalorderedP(sK259) | 'Ts63'(sK255) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d70,c96])). % 101.50/15.52 cnf(d72, plain, ~ssList(nil) | totalorderedP(sK259) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c214,d71])). % 101.50/15.52 cnf(d73, plain, totalorderedP(sK259) | 'Ts63'(sK255), inference(resolution, [status(thm)], [c97,d72])). % 101.50/15.52 cnf(d74, plain, totalorderedP(sK259) | ~ssList(sK255) | totalorderedP(sK255), inference(resolution, [status(thm)], [d73,c56])). % 101.50/15.52 cnf(d75, plain, totalorderedP(sK255) | totalorderedP(sK259), inference(resolution, [status(thm)], [c210,d74])). % 101.50/15.52 cnf(d76, plain, totalorderedP(sK255) | ~ssItem(sK261) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,c159])). % 101.50/15.52 cnf(d77, plain, sK256 = nil | ~ssList(nil) | ~ssList(sK256) | ~ssItem(sK261) | totalorderedP(sK255), inference(resolution, [status(thm)], [c95,d76])). % 101.50/15.52 cnf(d78, plain, sK256 = nil | ~ssItem(sK261) | ~ssList(nil) | totalorderedP(sK255), inference(resolution, [status(thm)], [c211,d77])). % 101.50/15.52 cnf(d79, plain, sK256 = nil | ~ssItem(sK261) | totalorderedP(sK255), inference(resolution, [status(thm)], [c97,d78])). % 101.50/15.52 cnf(d80, plain, nil != nil | nil = sK255 | ~ssItem(sK261) | totalorderedP(sK255), inference(superposition, [status(thm)], [d79,c223])). % 101.50/15.52 cnf(d81, plain, nil = sK255 | ~ssItem(sK261) | totalorderedP(sK255), inference(equality_resolution, [status(thm)], [d80])). % 101.50/15.52 cnf(d82, plain, ~rearsegP(sK259,nil) | sK259 = sK255 | ~ssItem(sK261) | totalorderedP(sK255), inference(superposition, [status(thm)], [d81,d62])). % 101.50/15.52 cnf(d83, plain, sK259 = sK255 | ~ssItem(sK261) | totalorderedP(sK255) | ~ssList(sK259), inference(resolution, [status(thm)], [d82,c143])). % 101.50/15.52 cnf(d84, plain, sK259 = sK255 | ~ssItem(sK261) | totalorderedP(sK255), inference(resolution, [status(thm)], [c216,d83])). % 101.50/15.52 cnf(d85, plain, sK259 = sK255 | totalorderedP(sK255), inference(resolution, [status(thm)], [d21,d84])). % 101.50/15.52 cnf(d86, plain, totalorderedP(sK255) | totalorderedP(sK255) | totalorderedP(sK255), inference(superposition, [status(thm)], [d85,d75])). % 101.50/15.52 cnf(d87, plain, nil = sK255 | ~neq(sK256,nil) | ~leq(X0,sK261) | 'Ts200'(X0,sK255), inference(resolution, [status(thm)], [d86,d24])). % 101.50/15.52 cnf(d88, plain, nil = sK255 | ~neq(sK256,nil) | 'Ts200'(sK261,sK255) | ~ssItem(sK261), inference(resolution, [status(thm)], [d87,c114])). % 101.50/15.52 cnf(d89, plain, nil = sK255 | ~neq(sK256,nil) | 'Ts200'(sK261,sK255), inference(resolution, [status(thm)], [d21,d88])). % 101.50/15.52 cnf(d90, plain, nil = sK255 | 'Ts200'(sK261,sK255) | sK256 = nil | ~ssList(nil) | ~ssList(sK256), inference(resolution, [status(thm)], [d89,c95])). % 101.50/15.52 cnf(d91, plain, nil = sK255 | sK256 = nil | ~ssList(nil) | 'Ts200'(sK261,sK255), inference(resolution, [status(thm)], [c211,d90])). % 101.50/15.52 cnf(d92, plain, nil = sK255 | sK256 = nil | 'Ts200'(sK261,sK255), inference(resolution, [status(thm)], [c97,d91])). % 101.50/15.52 cnf(d93, plain, nil = sK255 | sK256 = nil | nil = sK255 | ~neq(sK256,nil) | leq(sK261,sK261), inference(resolution, [status(thm)], [d92,d23])). % 101.50/15.52 cnf(d94, plain, nil = sK255 | sK256 = nil | leq(sK261,sK261) | sK256 = nil | ~ssList(nil) | ~ssList(sK256), inference(resolution, [status(thm)], [d93,c95])). % 101.50/15.52 cnf(d95, plain, nil = sK255 | sK256 = nil | ~ssList(nil) | leq(sK261,sK261), inference(resolution, [status(thm)], [c211,d94])). % 101.50/15.52 cnf(d96, plain, nil = sK255 | sK256 = nil | leq(sK261,sK261), inference(resolution, [status(thm)], [c97,d95])). % 101.50/15.52 cnf(d97, plain, ~memberP(sK255,X0) | X0 = sK261 | ~ssItem(sK261) | ~ssItem(X0) | memberP(nil,X0) | ~ssList(nil) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,c124])). % 101.50/15.52 cnf(d98, plain, X0 = sK261 | ~ssItem(X0) | ~ssItem(sK261) | ~neq(sK256,nil) | memberP(nil,X0) | ~memberP(sK255,X0), inference(resolution, [status(thm)], [c97,d97])). % 101.50/15.52 cnf(d99, plain, X0 = sK261 | ~ssItem(X0) | ~neq(sK256,nil) | memberP(nil,X0) | ~memberP(sK255,X0), inference(resolution, [status(thm)], [d21,d98])). % 101.50/15.52 cnf(d100, plain, app(sK258,app(cons(sK257,nil),sK259)) = sK255 | ~ssList(cons(sK257,nil)) | ~ssList(sK259) | ~ssList(sK258), inference(superposition, [status(thm)], [c190,d2])). % 101.50/15.52 cnf(d101, plain, app(sK258,app(cons(sK257,nil),sK259)) = sK255 | ~ssList(cons(sK257,nil)) | ~ssList(sK259), inference(resolution, [status(thm)], [c215,d100])). % 101.50/15.52 cnf(d102, plain, app(sK258,app(cons(sK257,nil),sK259)) = sK255 | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c216,d101])). % 101.50/15.52 cnf(d103, plain, app(sK258,cons(sK257,sK259)) = sK255 | ~ssList(cons(sK257,nil)) | ~ssItem(sK257) | ~ssList(sK259), inference(superposition, [status(thm)], [c189,d102])). % 101.50/15.52 cnf(d104, plain, app(sK258,cons(sK257,sK259)) = sK255 | ~ssList(cons(sK257,nil)) | ~ssList(sK259), inference(resolution, [status(thm)], [c214,d103])). % 101.50/15.52 cnf(d105, plain, app(sK258,cons(sK257,sK259)) = sK255 | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c216,d104])). % 101.50/15.52 cnf(d106, plain, sK255 != X0 | ~ssItem(sK257) | memberP(X0,sK257) | ~ssList(X0) | ~ssList(sK259) | ~ssList(sK258) | ~ssList(cons(sK257,nil)), inference(superposition, [status(thm)], [d105,c8])). % 101.50/15.52 cnf(d107, plain, sK255 != X0 | memberP(X0,sK257) | ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK258) | ~ssList(sK259), inference(resolution, [status(thm)], [c214,d106])). % 101.50/15.52 cnf(d108, plain, sK255 != X0 | memberP(X0,sK257) | ~ssList(X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK259), inference(resolution, [status(thm)], [c215,d107])). % 101.50/15.52 cnf(d109, plain, sK255 != X0 | memberP(X0,sK257) | ~ssList(X0) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c216,d108])). % 101.50/15.52 cnf(d110, plain, memberP(sK255,sK257) | ~ssList(sK255) | ~ssList(cons(sK257,nil)), inference(equality_resolution, [status(thm)], [d109])). % 101.50/15.52 cnf(d111, plain, memberP(sK255,sK257) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c210,d110])). % 101.50/15.52 cnf(d112, plain, memberP(sK255,sK257) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d111,c96])). % 101.50/15.52 cnf(d113, plain, memberP(sK255,sK257) | ~ssList(nil), inference(resolution, [status(thm)], [c214,d112])). % 101.50/15.52 cnf(d114, plain, memberP(sK255,sK257), inference(resolution, [status(thm)], [c97,d113])). % 101.50/15.52 cnf(d115, plain, sK257 = sK261 | ~ssItem(sK257) | ~neq(sK256,nil) | memberP(nil,sK257), inference(resolution, [status(thm)], [d114,d99])). % 101.50/15.52 cnf(d116, plain, sK257 = sK261 | ~neq(sK256,nil) | memberP(nil,sK257), inference(resolution, [status(thm)], [c214,d115])). % 101.50/15.52 cnf(d117, plain, sK257 = sK261 | memberP(nil,sK257) | sK256 = nil | ~ssList(nil) | ~ssList(sK256), inference(resolution, [status(thm)], [d116,c95])). % 101.50/15.52 cnf(d118, plain, sK256 = nil | sK257 = sK261 | memberP(nil,sK257) | ~ssList(nil), inference(resolution, [status(thm)], [c211,d117])). % 101.50/15.52 cnf(d119, plain, sK256 = nil | sK257 = sK261 | memberP(nil,sK257), inference(resolution, [status(thm)], [c97,d118])). % 101.50/15.52 cnf(d120, plain, sK256 = nil | sK257 = sK261 | ~ssItem(sK257), inference(resolution, [status(thm)], [d119,c127])). % 101.50/15.52 cnf(d121, plain, sK256 = nil | sK257 = sK261, inference(resolution, [status(thm)], [c214,d120])). % 101.50/15.52 cnf(d122, plain, leq(sK257,sK261) | nil = sK255 | sK256 = nil | sK256 = nil, inference(superposition, [status(thm)], [d121,d96])). % 101.50/15.52 cnf(d123, plain, memberP(sK255,X0) | ~ssItem(X0) | ~memberP(sK259,X0) | ~ssList(app(sK258,cons(sK257,nil))) | ~ssList(sK259), inference(superposition, [status(thm)], [d2,c123])). % 101.50/15.52 cnf(d124, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0) | ~ssList(app(sK258,cons(sK257,nil))), inference(resolution, [status(thm)], [c216,d123])). % 101.50/15.52 cnf(d125, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK258), inference(resolution, [status(thm)], [d124,c109])). % 101.50/15.52 cnf(d126, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c215,d125])). % 101.50/15.52 cnf(d127, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d126,c96])). % 101.50/15.52 cnf(d128, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0) | ~ssList(nil), inference(resolution, [status(thm)], [c214,d127])). % 101.50/15.52 cnf(d129, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK259,X0), inference(resolution, [status(thm)], [c97,d128])). % 101.50/15.52 cnf(d130, plain, ~ssItem(sK260) | memberP(sK255,sK260) | memberP(sK258,sK260), inference(resolution, [status(thm)], [d129,c219])). % 101.50/15.52 cnf(d131, plain, memberP(sK255,sK260) | memberP(sK258,sK260), inference(resolution, [status(thm)], [c218,d130])). % 101.50/15.52 cnf(d132, plain, memberP(sK255,X0) | ~ssItem(X0) | ~memberP(sK258,X0) | ~ssList(sK258) | ~ssList(cons(sK257,sK259)) | ~ssList(cons(sK257,nil)), inference(superposition, [status(thm)], [d105,c122])). % 101.50/15.52 cnf(d133, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssList(cons(sK257,nil)) | ~ssList(cons(sK257,sK259)), inference(resolution, [status(thm)], [c215,d132])). % 101.50/15.52 cnf(d134, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssList(cons(sK257,nil)) | ~ssItem(sK257) | ~ssList(sK259), inference(resolution, [status(thm)], [d133,c96])). % 101.50/15.52 cnf(d135, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssList(cons(sK257,nil)) | ~ssList(sK259), inference(resolution, [status(thm)], [c214,d134])). % 101.50/15.52 cnf(d136, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssList(cons(sK257,nil)), inference(resolution, [status(thm)], [c216,d135])). % 101.50/15.52 cnf(d137, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d136,c96])). % 101.50/15.52 cnf(d138, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0) | ~ssList(nil), inference(resolution, [status(thm)], [c214,d137])). % 101.50/15.52 cnf(d139, plain, ~ssItem(X0) | memberP(sK255,X0) | ~memberP(sK258,X0), inference(resolution, [status(thm)], [c97,d138])). % 101.50/15.52 cnf(d140, plain, ~ssItem(sK260) | memberP(sK255,sK260) | memberP(sK255,sK260), inference(resolution, [status(thm)], [d139,d131])). % 101.50/15.52 cnf(d141, plain, memberP(sK255,sK260), inference(resolution, [status(thm)], [c218,d140])). % 101.50/15.52 cnf(d142, plain, sK260 = sK261 | ~ssItem(sK260) | ~neq(sK256,nil) | memberP(nil,sK260), inference(resolution, [status(thm)], [d141,d99])). % 101.50/15.52 cnf(d143, plain, sK260 = sK261 | ~neq(sK256,nil) | memberP(nil,sK260), inference(resolution, [status(thm)], [c218,d142])). % 101.50/15.52 cnf(d144, plain, sK260 = sK261 | memberP(nil,sK260) | sK256 = nil | ~ssList(nil) | ~ssList(sK256), inference(resolution, [status(thm)], [d143,c95])). % 101.50/15.52 cnf(d145, plain, sK256 = nil | sK260 = sK261 | memberP(nil,sK260) | ~ssList(nil), inference(resolution, [status(thm)], [c211,d144])). % 101.50/15.52 cnf(d146, plain, sK256 = nil | sK260 = sK261 | memberP(nil,sK260), inference(resolution, [status(thm)], [c97,d145])). % 101.50/15.52 cnf(d147, plain, sK256 = nil | sK260 = sK261 | ~ssItem(sK260), inference(resolution, [status(thm)], [d146,c127])). % 101.50/15.52 cnf(d148, plain, sK256 = nil | sK260 = sK261, inference(resolution, [status(thm)], [c218,d147])). % 101.50/15.52 cnf(d149, plain, leq(sK257,sK260) | nil = sK255 | sK256 = nil | sK256 = nil, inference(superposition, [status(thm)], [d148,d122])). % 101.50/15.52 cnf(d150, plain, sK257 = sK260 | sK256 = nil | sK256 = nil, inference(superposition, [status(thm)], [d148,d121])). % 101.50/15.52 cnf(d151, plain, ~leq(sK260,sK260) | ~leq(sK257,sK260) | sK256 = nil, inference(superposition, [status(thm)], [d150,c222])). % 101.50/15.52 cnf(d152, plain, sK256 = nil | ~leq(sK257,sK260) | ~ssItem(sK260), inference(resolution, [status(thm)], [d151,c114])). % 101.50/15.52 cnf(d153, plain, sK256 = nil | ~leq(sK257,sK260), inference(resolution, [status(thm)], [c218,d152])). % 101.50/15.52 cnf(d154, plain, sK256 = nil | nil = sK255 | sK256 = nil, inference(resolution, [status(thm)], [d153,d149])). % 101.50/15.52 cnf(d155, plain, nil != nil | nil = sK255 | nil = sK255, inference(superposition, [status(thm)], [d154,c223])). % 101.50/15.52 cnf(d156, plain, nil = sK255, inference(equality_resolution, [status(thm)], [d155])). % 101.50/15.52 cnf(d157, plain, sK255 != X0 | ~ssItem(sK261) | ~ssList(X0) | singletonP(X0) | ~neq(sK256,nil), inference(superposition, [status(thm)], [c225,c11])). % 101.50/15.52 cnf(d158, plain, ~ssItem(sK261) | ~neq(sK256,nil) | ~ssList(sK255) | singletonP(sK255), inference(equality_resolution, [status(thm)], [d157])). % 101.50/15.52 cnf(d159, plain, ~ssItem(sK261) | ~neq(sK256,nil) | singletonP(sK255), inference(resolution, [status(thm)], [c210,d158])). % 101.50/15.52 cnf(d160, plain, sK256 = nil | ~ssList(nil) | ~ssList(sK256) | ~ssItem(sK261) | singletonP(sK255), inference(resolution, [status(thm)], [c95,d159])). % 101.50/15.52 cnf(d161, plain, sK256 = nil | ~ssItem(sK261) | ~ssList(nil) | singletonP(sK255), inference(resolution, [status(thm)], [c211,d160])). % 101.50/15.52 cnf(d162, plain, sK256 = nil | ~ssItem(sK261) | singletonP(sK255), inference(resolution, [status(thm)], [c97,d161])). % 101.50/15.52 cnf(d163, plain, nil != nil | nil = sK255 | ~ssItem(sK261) | singletonP(sK255), inference(superposition, [status(thm)], [d162,c223])). % 101.50/15.52 cnf(d164, plain, nil = sK255 | ~ssItem(sK261) | singletonP(sK255), inference(equality_resolution, [status(thm)], [d163])). % 101.50/15.52 cnf(d165, plain, segmentP(nil,cons(sK257,nil)) | ~ssList(cons(sK257,nil)) | ~ssItem(sK261) | singletonP(sK255), inference(superposition, [status(thm)], [d164,d7])). % 101.50/15.52 cnf(d166, plain, nil = cons(sK257,nil) | ~ssList(cons(sK257,nil)) | ~ssItem(sK261) | ~ssList(cons(sK257,nil)) | singletonP(sK255), inference(resolution, [status(thm)], [c151,d165])). % 101.50/15.52 cnf(d167, plain, nil = cons(sK257,nil) | ~ssList(cons(sK257,nil)) | singletonP(sK255), inference(resolution, [status(thm)], [d21,d166])). % 101.50/15.52 cnf(d168, plain, nil != nil | ~ssItem(sK257) | ~ssList(nil) | ~ssList(cons(sK257,nil)) | singletonP(sK255), inference(superposition, [status(thm)], [d167,c98])). % 101.50/15.52 cnf(d169, plain, nil != nil | ~ssList(cons(sK257,nil)) | ~ssList(nil) | singletonP(sK255), inference(resolution, [status(thm)], [c214,d168])). % 101.50/15.52 cnf(d170, plain, nil != nil | ~ssList(cons(sK257,nil)) | singletonP(sK255), inference(resolution, [status(thm)], [c97,d169])). % 101.50/15.52 cnf(d171, plain, ~ssList(cons(sK257,nil)) | singletonP(sK255), inference(equality_resolution, [status(thm)], [d170])). % 101.50/15.52 cnf(d172, plain, singletonP(sK255) | ~ssItem(sK257) | ~ssList(nil), inference(resolution, [status(thm)], [d171,c96])). % 101.50/15.52 cnf(d173, plain, ~ssList(nil) | singletonP(sK255), inference(resolution, [status(thm)], [c214,d172])). % 101.50/15.52 cnf(d174, plain, singletonP(sK255), inference(resolution, [status(thm)], [c97,d173])). % 101.50/15.52 cnf(d175, plain, singletonP(nil), inference(demodulation, [status(thm)], [d174,d156])). % 101.50/15.52 cnf(d176, plain, $false, inference(resolution, [status(thm)], [c128,d175])). % 101.50/15.52 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------