%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX207-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 : n005.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:48 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX207-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n005.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 10:33:04 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 0.16/0.48 % Refutation found
% 0.16/0.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.48 fof(f1,axiom,(
% 0.16/0.48 (![Q]: (impl(btrue,Q) = Q ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f3,axiom,(
% 0.16/0.48 (![Y]: (append(nil,Y) = Y ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f4,axiom,(
% 0.16/0.48 (![Z,Xs,Y]: (append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f8,axiom,(
% 0.16/0.48 linP(pB) = cons(b,nil) ),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f9,axiom,(
% 0.16/0.48 linP(pE) = nil ),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f10,axiom,(
% 0.16/0.48 (![P,Q]: (linC(c2(P,Q)) = append(linP(P),linP(Q)) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f11,axiom,(
% 0.16/0.48 (![X,Y]: (unambig(X,Y) = impl(eq(linC(X),linC(Y)),eq4(X,Y)) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f19,axiom,(
% 0.16/0.48 eq3(pE,pB) = bfalse ),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f38,axiom,(
% 0.16/0.48 (![X,Z,Y,X2]: (( eq3(X,Z) != bfalse| eq4(c2(X,Y),c2(Z,X2)) = bfalse ) ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f40,axiom,(
% 0.16/0.48 (![X]: (eq(X,X) = btrue ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f44,axiom,(
% 0.16/0.48 (![X]: (eq5(X,X) = btrue ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f49,negated_conjecture,(
% 0.16/0.48 (![X,Y]: (eq5(unambig(X,Y),bfalse) != btrue ))),
% 0.16/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.48 fof(f50,plain,(
% 0.16/0.48 ![X0]: (impl(btrue,X0)=X0)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.48 fof(f52,plain,(
% 0.16/0.48 ![X0]: (append(nil,X0)=X0)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/0.48 fof(f53,plain,(
% 0.16/0.48 ![X0,X1,X2]: (append(cons(X0,X1),X2)=cons(X0,append(X1,X2)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.48 fof(f57,plain,(
% 0.16/0.48 linP(pB)=cons(b,nil)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/0.48 fof(f58,plain,(
% 0.16/0.48 linP(pE)=nil),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f9])).
% 0.16/0.48 fof(f59,plain,(
% 0.16/0.48 ![X0,X1]: (linC(c2(X0,X1))=append(linP(X0),linP(X1)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/0.48 fof(f60,plain,(
% 0.16/0.48 ![X0,X1]: (unambig(X0,X1)=impl(eq(linC(X0),linC(X1)),eq4(X0,X1)))),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f11])).
% 0.16/0.48 fof(f68,plain,(
% 0.16/0.48 eq3(pE,pB)=bfalse),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.16/0.48 fof(f87,plain,(
% 0.16/0.48 ![X,Z]: (~eq3(X,Z)=bfalse|(![Y,X2]: eq4(c2(X,Y),c2(Z,X2))=bfalse))),
% 0.16/0.48 inference(miniscoping,[status(thm)],[f38])).
% 0.16/0.48 fof(f88,plain,(
% 0.16/0.48 ![X0,X1,X2,X3]: (~eq3(X0,X1)=bfalse|eq4(c2(X0,X2),c2(X1,X3))=bfalse)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f87])).
% 0.16/0.48 fof(f91,plain,(
% 0.16/0.48 ![X0]: (eq(X0,X0)=btrue)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f40])).
% 0.16/0.48 fof(f95,plain,(
% 0.16/0.48 ![X0]: (eq5(X0,X0)=btrue)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f44])).
% 0.16/0.48 fof(f102,plain,(
% 0.16/0.48 ![X0,X1]: (~eq5(unambig(X0,X1),bfalse)=btrue)),
% 0.16/0.48 inference(cnf_transformation,[status(thm)],[f49])).
% 0.16/0.48 fof(f113,plain,(
% 0.16/0.48 ![X0,X1]: (append(cons(X0,nil),X1)=cons(X0,X1))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f52,f53])).
% 0.16/0.48 fof(f130,plain,(
% 0.16/0.48 ![X0]: (linC(c2(pE,X0))=append(nil,linP(X0)))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f58,f59])).
% 0.16/0.48 fof(f131,plain,(
% 0.16/0.48 ![X0]: (linC(c2(X0,pE))=append(linP(X0),nil))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f58,f59])).
% 0.16/0.48 fof(f133,plain,(
% 0.16/0.48 ![X0]: (linC(c2(pE,X0))=linP(X0))),
% 0.16/0.48 inference(forward_demodulation,[status(thm)],[f52,f130])).
% 0.16/0.48 fof(f200,plain,(
% 0.16/0.48 ![X0]: (append(linP(pB),X0)=cons(b,X0))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f57,f113])).
% 0.16/0.48 fof(f227,plain,(
% 0.16/0.48 ![X0,X1]: (unambig(X0,c2(X1,pE))=impl(eq(linC(X0),append(linP(X1),nil)),eq4(X0,c2(X1,pE))))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f131,f60])).
% 0.16/0.48 fof(f291,plain,(
% 0.16/0.48 ![X0,X1]: (eq4(c2(pE,X0),c2(pB,X1))=bfalse)),
% 0.16/0.48 inference(resolution,[status(thm)],[f88,f68])).
% 0.16/0.48 fof(f563,plain,(
% 0.16/0.48 ![X0]: (unambig(c2(pE,X0),c2(pB,pE))=impl(eq(linC(c2(pE,X0)),append(linP(pB),nil)),bfalse))),
% 0.16/0.48 inference(paramodulation,[status(thm)],[f291,f227])).
% 0.16/0.49 fof(f574,plain,(
% 0.16/0.49 ![X0]: (unambig(c2(pE,X0),c2(pB,pE))=impl(eq(linP(X0),append(linP(pB),nil)),bfalse))),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f133,f563])).
% 0.16/0.49 fof(f575,plain,(
% 0.16/0.49 ![X0]: (unambig(c2(pE,X0),c2(pB,pE))=impl(eq(linP(X0),cons(b,nil)),bfalse))),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f200,f574])).
% 0.16/0.49 fof(f576,plain,(
% 0.16/0.49 ![X0]: (unambig(c2(pE,X0),c2(pB,pE))=impl(eq(linP(X0),linP(pB)),bfalse))),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f57,f575])).
% 0.16/0.49 fof(f699,plain,(
% 0.16/0.49 ![X0]: (~eq5(impl(eq(linP(X0),linP(pB)),bfalse),bfalse)=btrue)),
% 0.16/0.49 inference(paramodulation,[status(thm)],[f576,f102])).
% 0.16/0.49 fof(f704,plain,(
% 0.16/0.49 ~eq5(impl(btrue,bfalse),bfalse)=btrue),
% 0.16/0.49 inference(paramodulation,[status(thm)],[f91,f699])).
% 0.16/0.49 fof(f706,plain,(
% 0.16/0.49 ~eq5(bfalse,bfalse)=btrue),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f50,f704])).
% 0.16/0.49 fof(f707,plain,(
% 0.16/0.49 ~btrue=btrue),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f95,f706])).
% 0.16/0.49 fof(f708,plain,(
% 0.16/0.49 $false),
% 0.16/0.49 inference(trivial_equality_resolution,[status(thm)],[f707])).
% 0.16/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.52 % Elapsed time: 0.076346 seconds
% 0.16/0.52 % CPU time: 0.287848 seconds
% 0.16/0.52 % Total memory used: 71.609 MB
% 0.16/0.52 % Net memory used: 71.568 MB
%------------------------------------------------------------------------------