%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN250-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 : Thu Sep 24 03:19:12 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN250-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n016.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 10:52:14 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.39 % Drodi V4.1.1
% 0.15/5.41 % Refutation found
% 0.15/5.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.41 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.41 fof(f1,axiom,(
% 0.15/5.41 s0(d) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f9,axiom,(
% 0.15/5.41 r0(b) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f12,axiom,(
% 0.15/5.41 (![X]: (m0(a,X,a) ))),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f13,axiom,(
% 0.15/5.41 r0(e) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f14,axiom,(
% 0.15/5.41 (![X]: (p0(b,X) ))),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f20,axiom,(
% 0.15/5.41 l0(a) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f21,axiom,(
% 0.15/5.41 q0(b,e) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f36,axiom,(
% 0.15/5.41 q0(a,b) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f45,axiom,(
% 0.15/5.41 (![G,H,I]: (( m1(G,H,G)| ~ p0(I,H)| ~ r0(G) ) ))),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f54,axiom,(
% 0.15/5.41 (![H,I,J,A]: (( m1(H,I,I)| ~ m1(J,I,H)| ~ m1(J,A,I) ) ))),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f61,axiom,(
% 0.15/5.41 ( m1(a,a,a)| ~ l0(a)| ~ s0(d) ) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f62,axiom,(
% 0.15/5.41 (![F,G,H]: (( m1(F,a,G)| ~ m0(a,H,a)| ~ q0(F,G)| ~ m1(G,c,G) ) ))),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f369,negated_conjecture,(
% 0.15/5.41 ~ m1(e,a,a) ),
% 0.15/5.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.41 fof(f370,plain,(
% 0.15/5.41 s0(d)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/5.41 fof(f378,plain,(
% 0.15/5.41 r0(b)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/5.41 fof(f381,plain,(
% 0.15/5.41 ![X0]: (m0(a,X0,a))),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/5.41 fof(f382,plain,(
% 0.15/5.41 r0(e)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/5.41 fof(f383,plain,(
% 0.15/5.41 ![X0]: (p0(b,X0))),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f14])).
% 0.15/5.41 fof(f389,plain,(
% 0.15/5.41 l0(a)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f20])).
% 0.15/5.41 fof(f390,plain,(
% 0.15/5.41 q0(b,e)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/5.41 fof(f405,plain,(
% 0.15/5.41 q0(a,b)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/5.41 fof(f419,plain,(
% 0.15/5.41 ![G]: ((![H]: (m1(G,H,G)|(![I]: ~p0(I,H))))|~r0(G))),
% 0.15/5.41 inference(miniscoping,[status(thm)],[f45])).
% 0.15/5.41 fof(f420,plain,(
% 0.15/5.41 ![X0,X1,X2]: (m1(X0,X1,X0)|~p0(X2,X1)|~r0(X0))),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f419])).
% 0.15/5.41 fof(f434,plain,(
% 0.15/5.41 ![I,J]: ((![H]: (m1(H,I,I)|~m1(J,I,H)))|(![A]: ~m1(J,A,I)))),
% 0.15/5.41 inference(miniscoping,[status(thm)],[f54])).
% 0.15/5.41 fof(f435,plain,(
% 0.15/5.41 ![X0,X1,X2,X3]: (m1(X0,X1,X1)|~m1(X2,X1,X0)|~m1(X2,X3,X1))),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f434])).
% 0.15/5.41 fof(f445,plain,(
% 0.15/5.41 m1(a,a,a)|~l0(a)|~s0(d)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/5.41 fof(f446,plain,(
% 0.15/5.41 ![G]: ((![F]: ((m1(F,a,G)|(![H]: ~m0(a,H,a)))|~q0(F,G)))|~m1(G,c,G))),
% 0.15/5.41 inference(miniscoping,[status(thm)],[f62])).
% 0.15/5.41 fof(f447,plain,(
% 0.15/5.41 ![X0,X1,X2]: (m1(X0,a,X1)|~m0(a,X2,a)|~q0(X0,X1)|~m1(X1,c,X1))),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f446])).
% 0.15/5.41 fof(f924,plain,(
% 0.15/5.41 ~m1(e,a,a)),
% 0.15/5.41 inference(cnf_transformation,[status(thm)],[f369])).
% 0.15/5.41 fof(f925,plain,(
% 0.15/5.41 ![X0,X1]: (~m1(X0,a,e)|~m1(X0,X1,a))),
% 0.15/5.41 inference(resolution,[status(thm)],[f435,f924])).
% 0.15/5.41 fof(f1017,plain,(
% 0.15/5.41 m1(a,a,a)|~s0(d)),
% 0.15/5.41 inference(forward_subsumption_resolution,[status(thm)],[f445,f389])).
% 0.15/5.41 fof(f1021,plain,(
% 0.15/5.41 ![X0,X1]: (m1(X0,a,X1)|~q0(X0,X1)|~m1(X1,c,X1))),
% 0.15/5.41 inference(forward_subsumption_resolution,[status(thm)],[f447,f381])).
% 0.15/5.41 fof(f1024,plain,(
% 0.15/5.41 ![X0,X1]: (~q0(X0,e)|~m1(e,c,e)|~m1(X0,X1,a))),
% 0.15/5.41 inference(resolution,[status(thm)],[f1021,f925])).
% 0.15/5.41 fof(f1026,plain,(
% 0.15/5.41 ![X0]: (~m1(e,c,e)|~m1(b,X0,a))),
% 0.15/5.41 inference(resolution,[status(thm)],[f1024,f390])).
% 0.15/5.41 fof(f1028,plain,(
% 0.15/5.41 ![X0,X1]: (~m1(e,c,e)|~m1(X0,a,b)|~m1(X0,X1,a))),
% 0.15/5.41 inference(resolution,[status(thm)],[f1026,f435])).
% 0.15/5.41 fof(f1030,plain,(
% 0.15/5.41 ![X0,X1,X2]: (~m1(X0,a,b)|~m1(X0,X1,a)|~p0(X2,c)|~r0(e))),
% 0.15/5.41 inference(resolution,[status(thm)],[f1028,f420])).
% 0.15/5.41 fof(f1032,plain,(
% 0.15/5.41 ![X0,X1,X2]: (~m1(X0,a,b)|~m1(X0,X1,a)|~p0(X2,c))),
% 0.15/5.41 inference(forward_subsumption_resolution,[status(thm)],[f1030,f382])).
% 0.15/5.42 fof(f1033,plain,(
% 0.15/5.42 ![X0,X1]: (~m1(X0,a,b)|~m1(X0,X1,a))),
% 0.15/5.42 inference(resolution,[status(thm)],[f1032,f383])).
% 0.15/5.42 fof(f1034,plain,(
% 0.15/5.42 ![X0,X1]: (~m1(X0,X1,a)|~q0(X0,b)|~m1(b,c,b))),
% 0.15/5.42 inference(resolution,[status(thm)],[f1033,f1021])).
% 0.15/5.42 fof(f1053,plain,(
% 0.15/5.42 ![X0,X1,X2]: (~m1(X0,X1,a)|~q0(X0,b)|~p0(X2,c)|~r0(b))),
% 0.15/5.42 inference(resolution,[status(thm)],[f1034,f420])).
% 0.15/5.42 fof(f1055,plain,(
% 0.15/5.42 ![X0,X1,X2]: (~m1(X0,X1,a)|~q0(X0,b)|~p0(X2,c))),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f1053,f378])).
% 0.15/5.42 fof(f1056,plain,(
% 0.15/5.42 ![X0,X1]: (~m1(X0,X1,a)|~q0(X0,b))),
% 0.15/5.42 inference(resolution,[status(thm)],[f1055,f383])).
% 0.15/5.42 fof(f1057,plain,(
% 0.15/5.42 ![X0]: (~m1(a,X0,a))),
% 0.15/5.42 inference(resolution,[status(thm)],[f1056,f405])).
% 0.15/5.42 fof(f1060,plain,(
% 0.15/5.42 ~s0(d)),
% 0.15/5.42 inference(backward_subsumption_resolution,[status(thm)],[f1017,f1057])).
% 0.15/5.42 fof(f1070,plain,(
% 0.15/5.42 $false),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f1060,f370])).
% 0.15/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 1.53/6.64 % Elapsed time: 1.047722 seconds
% 1.53/6.64 % CPU time: 0.163168 seconds
% 1.53/6.64 % Total memory used: 48.861 MB
% 1.53/6.64 % Net memory used: 48.713 MB
%------------------------------------------------------------------------------