%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 03:13:44 PM UTC 2026
% Result : Theorem 91.85s 21.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/10.32 % Computer : n012.cluster.edu
% 0.03/10.32 % Model : x86_64 x86_64
% 0.03/10.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/10.32 % Memory : 8046.5625MB
% 0.03/10.32 % OS : Linux 6.8.0-71-generic
% 0.03/10.32 % CPULimit : 300
% 0.03/10.32 % WCLimit : 300
% 0.03/10.32 % DateTime : Mon Sep 21 10:30:48 UTC 2026
% 0.03/10.32 % CPUTime :
% 0.03/10.33 % Drodi V4.1.1
% 91.85/21.99 % Refutation found
% 91.85/21.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 91.85/21.99 % SZS output start CNFRefutation for theBenchmark
% 91.85/21.99 fof(f1,axiom,(
% 91.85/21.99 (! [X,X2] : head(cons(X,X2)) = X )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f2,axiom,(
% 91.85/21.99 (! [X,X2] : tail(cons(X,X2)) = X2 )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f6,axiom,(
% 91.85/21.99 c != y ),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f25,axiom,(
% 91.85/21.99 (! [X,X2] : z(X,X2) != eY )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f27,axiom,(
% 91.85/21.99 (! [X,X2] : x2(X,X2) != eY )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f29,axiom,(
% 91.85/21.99 (! [X] :( X != z(proj1(X),proj2(X))=> ( X != x2(proj12(X),proj22(X))=> assoc(X) = X ) ) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f32,axiom,(
% 91.85/21.99 (! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f33,axiom,(
% 91.85/21.99 (! [Y] : append(nil,Y) = Y )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f34,axiom,(
% 91.85/21.99 (! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f35,axiom,(
% 91.85/21.99 (! [X] :( X != x2(proj12(X),proj22(X))=> linTerm(X) = lin(X) ) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f36,axiom,(
% 91.85/21.99 (! [A,B] : linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil))) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f37,axiom,(
% 91.85/21.99 (! [A,B] : lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B))) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f38,axiom,(
% 91.85/21.99 (! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f40,axiom,(
% 91.85/21.99 lin(eY) = cons(y,nil) ),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f41,conjecture,(
% 91.85/21.99 (? [U,V] :~ ( lin(U) = lin(V)=> assoc(U) = assoc(V) ) )),
% 91.85/21.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 91.85/21.99 fof(f42,negated_conjecture,(
% 91.85/21.99 ~((? [U,V] :~ ( lin(U) = lin(V)=> assoc(U) = assoc(V) ) ))),
% 91.85/21.99 inference(negated_conjecture,[status(cth)],[f41])).
% 91.85/21.99 fof(f43,plain,(
% 91.85/21.99 ![X0,X1]: (head(cons(X0,X1))=X0)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f1])).
% 91.85/21.99 fof(f44,plain,(
% 91.85/21.99 ![X0,X1]: (tail(cons(X0,X1))=X1)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f2])).
% 91.85/21.99 fof(f48,plain,(
% 91.85/21.99 ~c=y),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f6])).
% 91.85/21.99 fof(f67,plain,(
% 91.85/21.99 ![X0,X1]: (~z(X0,X1)=eY)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f25])).
% 91.85/21.99 fof(f69,plain,(
% 91.85/21.99 ![X0,X1]: (~x2(X0,X1)=eY)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f27])).
% 91.85/21.99 fof(f71,plain,(
% 91.85/21.99 ![X]: (X=z(proj1(X),proj2(X))|(X=x2(proj12(X),proj22(X))|assoc(X)=X))),
% 91.85/21.99 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 91.85/21.99 fof(f72,plain,(
% 91.85/21.99 ![X0]: (X0=z(proj1(X0),proj2(X0))|X0=x2(proj12(X0),proj22(X0))|assoc(X0)=X0)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f71])).
% 91.85/21.99 fof(f77,plain,(
% 91.85/21.99 ![X0,X1]: (assoc(x2(X0,X1))=x2(assoc(X0),assoc(X1)))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f32])).
% 91.85/21.99 fof(f78,plain,(
% 91.85/21.99 ![X0]: (append(nil,X0)=X0)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f33])).
% 91.85/21.99 fof(f79,plain,(
% 91.85/21.99 ![X0,X1,X2]: (append(cons(X0,X1),X2)=cons(X0,append(X1,X2)))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f34])).
% 91.85/21.99 fof(f80,plain,(
% 91.85/21.99 ![X]: (X=x2(proj12(X),proj22(X))|linTerm(X)=lin(X))),
% 91.85/21.99 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 91.85/21.99 fof(f81,plain,(
% 91.85/21.99 ![X0]: (X0=x2(proj12(X0),proj22(X0))|linTerm(X0)=lin(X0))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f80])).
% 91.85/21.99 fof(f82,plain,(
% 91.85/21.99 ![X0,X1]: (linTerm(x2(X0,X1))=append(cons(c,nil),append(lin(z(X0,X1)),cons(d,nil))))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f36])).
% 91.85/21.99 fof(f83,plain,(
% 91.85/21.99 ![X0,X1]: (lin(z(X0,X1))=append(linTerm(X0),append(cons(plus,nil),linTerm(X1))))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f37])).
% 91.85/21.99 fof(f84,plain,(
% 91.85/21.99 ![X0,X1]: (lin(x2(X0,X1))=append(lin(X0),append(cons(mul,nil),lin(X1))))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f38])).
% 91.85/21.99 fof(f86,plain,(
% 91.85/21.99 lin(eY)=cons(y,nil)),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f40])).
% 91.85/21.99 fof(f87,plain,(
% 91.85/21.99 (![U,V]: (~lin(U)=lin(V)|assoc(U)=assoc(V)))),
% 91.85/21.99 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 91.85/21.99 fof(f88,plain,(
% 91.85/21.99 ![X0,X1]: (~lin(X0)=lin(X1)|assoc(X0)=assoc(X1))),
% 91.85/21.99 inference(cnf_transformation,[status(thm)],[f87])).
% 91.85/21.99 fof(f2019,plain,(
% 91.85/21.99 ![X0,X1]: (~assoc(x2(X0,X1))=eY)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f77,f69])).
% 91.85/21.99 fof(f2102,plain,(
% 91.85/21.99 ![X0]: (~X0=eY|X0=x2(proj12(X0),proj22(X0))|assoc(X0)=X0)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f72,f67])).
% 91.85/21.99 fof(f2154,plain,(
% 91.85/21.99 eY=x2(proj12(eY),proj22(eY))|assoc(eY)=eY),
% 91.85/21.99 inference(destructive_equality_resolution,[status(thm)],[f2102])).
% 91.85/21.99 fof(f2155,plain,(
% 91.85/21.99 assoc(eY)=eY),
% 91.85/21.99 inference(forward_subsumption_resolution,[status(thm)],[f2154,f69])).
% 91.85/21.99 fof(f2211,plain,(
% 91.85/21.99 ![X0,X1]: (append(cons(X0,nil),X1)=cons(X0,X1))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f78,f79])).
% 91.85/21.99 fof(f2213,plain,(
% 91.85/21.99 ![X0,X1,X2]: (tail(append(cons(X0,X1),X2))=append(X1,X2))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f79,f44])).
% 91.85/21.99 fof(f2214,plain,(
% 91.85/21.99 ![X0,X1,X2]: (head(append(cons(X0,X1),X2))=X0)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f79,f43])).
% 91.85/21.99 fof(f2929,plain,(
% 91.85/21.99 ![X0]: (assoc(x2(eY,X0))=x2(eY,assoc(X0)))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f2155,f77])).
% 91.85/21.99 fof(f2940,plain,(
% 91.85/21.99 ![X0,X1,X2,X3]: (head(append(append(cons(X0,X1),X2),X3))=X0)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f79,f2214])).
% 91.85/21.99 fof(f2965,plain,(
% 91.85/21.99 ![X0]: (~assoc(X0)=eY|linTerm(X0)=lin(X0))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f81,f2019])).
% 91.85/21.99 fof(f2987,plain,(
% 91.85/21.99 linTerm(eY)=lin(eY)),
% 91.85/21.99 inference(resolution,[status(thm)],[f2965,f2155])).
% 91.85/21.99 fof(f4192,plain,(
% 91.85/21.99 ![X0,X1]: (lin(z(X0,X1))=append(linTerm(X0),cons(plus,linTerm(X1))))),
% 91.85/21.99 inference(backward_demodulation,[status(thm)],[f2211,f83])).
% 91.85/21.99 fof(f4193,plain,(
% 91.85/21.99 ![X0,X1]: (linTerm(x2(X0,X1))=cons(c,append(lin(z(X0,X1)),cons(d,nil))))),
% 91.85/21.99 inference(backward_demodulation,[status(thm)],[f2211,f82])).
% 91.85/21.99 fof(f4194,plain,(
% 91.85/21.99 ![X0]: (append(lin(eY),X0)=cons(y,X0))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f86,f2211])).
% 91.85/21.99 fof(f4199,plain,(
% 91.85/21.99 ![X0,X1]: (linTerm(x2(X0,X1))=append(cons(c,lin(z(X0,X1))),cons(d,nil)))),
% 91.85/21.99 inference(forward_demodulation,[status(thm)],[f79,f4193])).
% 91.85/21.99 fof(f4204,plain,(
% 91.85/21.99 ![X0,X1]: (lin(x2(X0,X1))=append(lin(X0),cons(mul,lin(X1))))),
% 91.85/21.99 inference(forward_demodulation,[status(thm)],[f2211,f84])).
% 91.85/21.99 fof(f4209,plain,(
% 91.85/21.99 ![X0,X1,X2]: (append(cons(X0,lin(X1)),cons(mul,lin(X2)))=cons(X0,lin(x2(X1,X2))))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4204,f79])).
% 91.85/21.99 fof(f4211,plain,(
% 91.85/21.99 ![X0]: (lin(z(eY,X0))=append(lin(eY),cons(plus,linTerm(X0))))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f2987,f4192])).
% 91.85/21.99 fof(f4755,plain,(
% 91.85/21.99 ![X0]: (lin(x2(eY,X0))=cons(y,cons(mul,lin(X0))))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4204,f4194])).
% 91.85/21.99 fof(f4765,plain,(
% 91.85/21.99 ![X0,X1]: (tail(linTerm(x2(X0,X1)))=append(lin(z(X0,X1)),cons(d,nil)))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4199,f2213])).
% 91.85/21.99 fof(f5540,plain,(
% 91.85/21.99 ![X0,X1,X2,X3,X4]: (head(append(append(append(cons(X0,X1),X2),X3),X4))=X0)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f79,f2940])).
% 91.85/21.99 fof(f7619,plain,(
% 91.85/21.99 ![X0,X1,X2,X3]: (append(cons(X0,cons(X1,lin(X2))),cons(mul,lin(X3)))=cons(X0,cons(X1,lin(x2(X2,X3)))))),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4209,f79])).
% 91.85/21.99 fof(f11591,plain,(
% 91.85/21.99 ![X0,X1,X2,X3]: (head(append(append(linTerm(x2(X0,X1)),X2),X3))=c)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4199,f5540])).
% 91.85/21.99 fof(f14651,plain,(
% 91.85/21.99 ![X0,X1,X2,X3]: (head(append(lin(z(x2(X0,X1),X2)),X3))=c)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4192,f11591])).
% 91.85/21.99 fof(f14802,plain,(
% 91.85/21.99 ![X0,X1,X2]: (head(tail(linTerm(x2(x2(X0,X1),X2))))=c)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f4765,f14651])).
% 91.85/21.99 fof(f14816,plain,(
% 91.85/21.99 ![X0,X1,X2]: (head(tail(linTerm(x2(assoc(x2(X0,X1)),X2))))=c)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f77,f14802])).
% 91.85/21.99 fof(f20725,plain,(
% 91.85/21.99 ![X0,X1,X2]: (head(tail(linTerm(assoc(x2(x2(X0,X1),X2)))))=c)),
% 91.85/21.99 inference(paramodulation,[status(thm)],[f77,f14816])).
% 91.85/21.99 fof(f20942,plain,(
% 87.40/22.17 ![X0,X1,X2]: (head(tail(linTerm(assoc(x2(assoc(x2(X0,X1)),X2)))))=c)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f77,f20725])).
% 87.40/22.17 fof(f27945,plain,(
% 87.40/22.17 ![X0,X1]: (append(lin(x2(eY,X0)),cons(mul,lin(X1)))=cons(y,cons(mul,lin(x2(X0,X1)))))),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f4755,f7619])).
% 87.40/22.17 fof(f27976,plain,(
% 87.40/22.17 ![X0,X1]: (lin(x2(x2(eY,X0),X1))=cons(y,cons(mul,lin(x2(X0,X1)))))),
% 87.40/22.17 inference(forward_demodulation,[status(thm)],[f4204,f27945])).
% 87.40/22.17 fof(f27977,plain,(
% 87.40/22.17 ![X0,X1]: (lin(x2(x2(eY,X0),X1))=lin(x2(eY,x2(X0,X1))))),
% 87.40/22.17 inference(forward_demodulation,[status(thm)],[f4755,f27976])).
% 87.40/22.17 fof(f56362,plain,(
% 87.40/22.17 ![X0,X1,X2]: (head(tail(linTerm(assoc(assoc(x2(x2(X0,X1),X2))))))=c)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f77,f20942])).
% 87.40/22.17 fof(f108923,plain,(
% 87.40/22.17 ![X0]: (lin(z(eY,X0))=cons(y,cons(plus,linTerm(X0))))),
% 87.40/22.17 inference(forward_demodulation,[status(thm)],[f4194,f4211])).
% 87.40/22.17 fof(f108944,plain,(
% 87.40/22.17 ![X0,X1]: (head(append(lin(z(eY,X0)),X1))=y)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f108923,f2214])).
% 87.40/22.17 fof(f111079,plain,(
% 87.40/22.17 ![X0]: (head(tail(linTerm(x2(eY,X0))))=y)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f4765,f108944])).
% 87.40/22.17 fof(f111093,plain,(
% 87.40/22.17 ![X0]: (head(tail(linTerm(assoc(x2(eY,X0)))))=y)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f2929,f111079])).
% 87.40/22.17 fof(f112254,plain,(
% 87.40/22.17 ![X0]: (head(tail(linTerm(assoc(assoc(x2(eY,X0))))))=y)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f2929,f111093])).
% 87.40/22.17 fof(f193640,plain,(
% 87.40/22.17 ![X0,X1]: (assoc(x2(x2(eY,X0),X1))=assoc(x2(eY,x2(X0,X1))))),
% 87.40/22.17 inference(resolution,[status(thm)],[f27977,f88])).
% 87.40/22.17 fof(f196875,plain,(
% 87.40/22.17 ![X0,X1]: (head(tail(linTerm(assoc(assoc(x2(eY,x2(X0,X1)))))))=c)),
% 87.40/22.17 inference(paramodulation,[status(thm)],[f193640,f56362])).
% 87.40/22.17 fof(f197375,plain,(
% 87.40/22.17 y=c),
% 87.40/22.17 inference(forward_demodulation,[status(thm)],[f112254,f196875])).
% 87.40/22.17 fof(f197376,plain,(
% 87.40/22.17 $false),
% 87.40/22.17 inference(forward_subsumption_resolution,[status(thm)],[f197375,f48])).
% 87.40/22.17 % SZS output end CNFRefutation for theBenchmark.p
% 5.89/22.19 % Elapsed time: 11.855366 seconds
% 5.89/22.19 % CPU time: 94.032084 seconds
% 5.89/22.19 % Total memory used: 1.910 GB
% 5.89/22.19 % Net memory used: 1.878 GB
%------------------------------------------------------------------------------