%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN216-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 : 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:19:09 PM UTC 2026
% Result : Unsatisfiable 0.03s 0.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN216-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 10:45:51 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.03/0.32 % Refutation found
% 0.03/0.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/0.32 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.32 fof(f5,axiom,(
% 0.03/0.32 s0(b) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f12,axiom,(
% 0.03/0.32 (![X]: (m0(a,X,a) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f14,axiom,(
% 0.03/0.32 (![X]: (p0(b,X) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f20,axiom,(
% 0.03/0.32 l0(a) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f32,axiom,(
% 0.03/0.32 k0(b) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f36,axiom,(
% 0.03/0.32 q0(a,b) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f38,axiom,(
% 0.03/0.32 m0(b,a,a) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f54,axiom,(
% 0.03/0.32 (![H,I,J,A]: (( m1(H,I,I)| ~ m1(J,I,H)| ~ m1(J,A,I) ) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f59,axiom,(
% 0.03/0.32 (![I,J]: (( m1(I,J,I)| ~ l0(I)| ~ k0(J) ) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f62,axiom,(
% 0.03/0.32 (![F,G,H]: (( m1(F,a,G)| ~ m0(a,H,a)| ~ q0(F,G)| ~ m1(G,c,G) ) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f67,axiom,(
% 0.03/0.32 (![H,I]: (( m1(H,I,H)| ~ p0(H,I)| ~ s0(H) ) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f172,axiom,(
% 0.03/0.32 (![G,H,I]: (( l2(G,G)| ~ m0(H,G,I)| ~ m1(I,H,H)| ~ p0(H,G) ) ))),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f369,negated_conjecture,(
% 0.03/0.32 ~ l2(a,a) ),
% 0.03/0.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.32 fof(f374,plain,(
% 0.03/0.32 s0(b)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f5])).
% 0.03/0.32 fof(f381,plain,(
% 0.03/0.32 ![X0]: (m0(a,X0,a))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f12])).
% 0.03/0.32 fof(f383,plain,(
% 0.03/0.32 ![X0]: (p0(b,X0))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f14])).
% 0.03/0.32 fof(f389,plain,(
% 0.03/0.32 l0(a)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f20])).
% 0.03/0.32 fof(f401,plain,(
% 0.03/0.32 k0(b)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f32])).
% 0.03/0.32 fof(f405,plain,(
% 0.03/0.32 q0(a,b)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f36])).
% 0.03/0.32 fof(f407,plain,(
% 0.03/0.32 m0(b,a,a)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f38])).
% 0.03/0.32 fof(f434,plain,(
% 0.03/0.32 ![I,J]: ((![H]: (m1(H,I,I)|~m1(J,I,H)))|(![A]: ~m1(J,A,I)))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f54])).
% 0.03/0.32 fof(f435,plain,(
% 0.03/0.32 ![X0,X1,X2,X3]: (m1(X0,X1,X1)|~m1(X2,X1,X0)|~m1(X2,X3,X1))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f434])).
% 0.03/0.32 fof(f442,plain,(
% 0.03/0.32 ![J]: ((![I]: (m1(I,J,I)|~l0(I)))|~k0(J))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f59])).
% 0.03/0.32 fof(f443,plain,(
% 0.03/0.32 ![X0,X1]: (m1(X0,X1,X0)|~l0(X0)|~k0(X1))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f442])).
% 0.03/0.32 fof(f446,plain,(
% 0.03/0.32 ![G]: ((![F]: ((m1(F,a,G)|(![H]: ~m0(a,H,a)))|~q0(F,G)))|~m1(G,c,G))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f62])).
% 0.03/0.32 fof(f447,plain,(
% 0.03/0.32 ![X0,X1,X2]: (m1(X0,a,X1)|~m0(a,X2,a)|~q0(X0,X1)|~m1(X1,c,X1))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f446])).
% 0.03/0.32 fof(f454,plain,(
% 0.03/0.32 ![H]: ((![I]: (m1(H,I,H)|~p0(H,I)))|~s0(H))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f67])).
% 0.03/0.32 fof(f455,plain,(
% 0.03/0.32 ![X0,X1]: (m1(X0,X1,X0)|~p0(X0,X1)|~s0(X0))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f454])).
% 0.03/0.32 fof(f621,plain,(
% 0.03/0.32 ![G,H]: ((![I]: ((l2(G,G)|~m0(H,G,I))|~m1(I,H,H)))|~p0(H,G))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f172])).
% 0.03/0.32 fof(f622,plain,(
% 0.03/0.32 ![X0,X1,X2]: (l2(X0,X0)|~m0(X1,X0,X2)|~m1(X2,X1,X1)|~p0(X1,X0))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f621])).
% 0.03/0.32 fof(f924,plain,(
% 0.03/0.32 ~l2(a,a)),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f369])).
% 0.03/0.32 fof(f926,plain,(
% 0.03/0.32 ![X0,X1]: (l2(X0,X0)|~m0(b,X0,X1)|~m1(X1,b,b))),
% 0.03/0.32 inference(resolution,[status(thm)],[f383,f622])).
% 0.03/0.32 fof(f994,plain,(
% 0.03/0.32 ![X0,X1,X2,X3]: (~m1(X0,b,X1)|~m1(X0,X2,b)|l2(X3,X3)|~m0(b,X3,X1))),
% 0.03/0.32 inference(resolution,[status(thm)],[f435,f926])).
% 0.03/0.32 fof(f1005,plain,(
% 0.03/0.32 ![X0,X1,X2]: (~m1(X0,b,X1)|~m1(X0,X2,b)|~m0(b,a,X1))),
% 0.03/0.32 inference(resolution,[status(thm)],[f994,f924])).
% 0.03/0.32 fof(f1006,plain,(
% 0.03/0.32 ![X0,X1]: (~m1(X0,b,a)|~m1(X0,X1,b))),
% 0.03/0.32 inference(resolution,[status(thm)],[f1005,f407])).
% 0.03/0.32 fof(f1028,plain,(
% 0.03/0.32 ![X0]: (m1(X0,b,X0)|~l0(X0))),
% 0.03/0.32 inference(resolution,[status(thm)],[f443,f401])).
% 0.03/0.32 fof(f1031,plain,(
% 0.03/0.32 ![X0,X1]: (m1(X0,a,X1)|~q0(X0,X1)|~m1(X1,c,X1))),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f447,f381])).
% 0.03/0.32 fof(f1034,plain,(
% 0.03/0.32 m1(a,b,a)),
% 0.03/0.32 inference(resolution,[status(thm)],[f1028,f389])).
% 0.03/0.32 fof(f1035,plain,(
% 0.03/0.32 ![X0]: (~m1(a,X0,b))),
% 0.03/0.32 inference(resolution,[status(thm)],[f1034,f1006])).
% 0.03/0.32 fof(f1036,plain,(
% 0.03/0.32 ~q0(a,b)|~m1(b,c,b)),
% 0.03/0.32 inference(resolution,[status(thm)],[f1035,f1031])).
% 0.03/0.32 fof(f1038,plain,(
% 0.03/0.32 ~m1(b,c,b)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f1036,f405])).
% 0.03/0.32 fof(f1077,plain,(
% 0.03/0.32 ![X0]: (m1(b,X0,b)|~p0(b,X0))),
% 0.03/0.32 inference(resolution,[status(thm)],[f455,f374])).
% 0.03/0.32 fof(f1079,plain,(
% 0.03/0.32 ![X0]: (m1(b,X0,b))),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f1077,f383])).
% 0.03/0.32 fof(f1081,plain,(
% 0.03/0.32 $false),
% 0.03/0.32 inference(backward_subsumption_resolution,[status(thm)],[f1038,f1079])).
% 0.03/0.32 % SZS output end CNFRefutation for theBenchmark.p
% 1.27/1.54 % Elapsed time: 1.029481 seconds
% 1.27/1.54 % CPU time: 0.055037 seconds
% 1.27/1.54 % Total memory used: 11.395 MB
% 1.27/1.54 % Net memory used: 11.357 MB
%------------------------------------------------------------------------------