%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MSC008-2.002 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 01:28:21 PM UTC 2026
% Result : Unsatisfiable 0.24s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MSC008-2.002 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.66 % Computer : n017.cluster.edu
% 0.20/0.66 % Model : x86_64 x86_64
% 0.20/0.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.66 % Memory : 8046.5625MB
% 0.20/0.66 % OS : Linux 6.8.0-71-generic
% 0.20/0.67 % CPULimit : 300
% 0.20/0.67 % WCLimit : 300
% 0.20/0.67 % DateTime : Mon Sep 21 01:22:41 UTC 2026
% 0.20/0.67 % CPUTime :
% 0.20/0.68 % Drodi V4.1.1
% 0.24/0.87 % Refutation found
% 0.24/0.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/0.87 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.87 fof(f1,axiom,(
% 0.24/0.87 ~ eq(p1,p2) ),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f3,axiom,(
% 0.24/0.87 (![A,B]: (( ~ eq(A,B)| eq(B,A) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f5,axiom,(
% 0.24/0.87 (![A,B,C,D]: (( ~ latin(A,B,C)| ~ latin(A,D,C)| eq(D,B) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f6,axiom,(
% 0.24/0.87 (![A,B,C,D]: (( ~ latin(A,B,C)| ~ latin(D,B,C)| eq(D,A) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f8,axiom,(
% 0.24/0.87 (![A,B,C,D]: (( ~ greek(A,B,C)| ~ greek(A,D,C)| eq(D,B) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f9,axiom,(
% 0.24/0.87 (![A,B,C,D]: (( ~ greek(A,B,C)| ~ greek(D,B,C)| eq(D,A) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f10,axiom,(
% 0.24/0.87 (![E,F]: (( latin(E,F,p1)| latin(E,F,p2) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f11,axiom,(
% 0.24/0.87 (![G,H]: (( latin(G,p1,H)| latin(G,p2,H) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f12,axiom,(
% 0.24/0.87 (![I,J]: (( latin(p1,I,J)| latin(p2,I,J) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f13,axiom,(
% 0.24/0.87 (![K,L]: (( greek(K,L,p1)| greek(K,L,p2) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f14,axiom,(
% 0.24/0.87 (![M,N]: (( greek(M,p1,N)| greek(M,p2,N) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f15,axiom,(
% 0.24/0.87 (![O,P]: (( greek(p1,O,P)| greek(p2,O,P) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f16,negated_conjecture,(
% 0.24/0.87 (![A,B,C,D,E,F]: (( ~ greek(A,B,C)| ~ latin(A,B,D)| ~ greek(E,F,C)| ~ latin(E,F,D)| eq(F,B)| eq(E,A) ) ))),
% 0.24/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.87 fof(f17,plain,(
% 0.24/0.87 ~eq(p1,p2)),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f1])).
% 0.24/0.87 fof(f19,plain,(
% 0.24/0.87 ![X0,X1]: (~eq(X0,X1)|eq(X1,X0))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f3])).
% 0.24/0.87 fof(f22,plain,(
% 0.24/0.87 ![B,D]: ((![A,C]: (~latin(A,B,C)|~latin(A,D,C)))|eq(D,B))),
% 0.24/0.87 inference(miniscoping,[status(thm)],[f5])).
% 0.24/0.87 fof(f23,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (~latin(X0,X1,X2)|~latin(X0,X3,X2)|eq(X3,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f22])).
% 0.24/0.87 fof(f24,plain,(
% 0.24/0.87 ![A,D]: ((![B,C]: (~latin(A,B,C)|~latin(D,B,C)))|eq(D,A))),
% 0.24/0.87 inference(miniscoping,[status(thm)],[f6])).
% 0.24/0.87 fof(f25,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (~latin(X0,X1,X2)|~latin(X3,X1,X2)|eq(X3,X0))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f24])).
% 0.24/0.87 fof(f28,plain,(
% 0.24/0.87 ![B,D]: ((![A,C]: (~greek(A,B,C)|~greek(A,D,C)))|eq(D,B))),
% 0.24/0.87 inference(miniscoping,[status(thm)],[f8])).
% 0.24/0.87 fof(f29,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (~greek(X0,X1,X2)|~greek(X0,X3,X2)|eq(X3,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f28])).
% 0.24/0.87 fof(f30,plain,(
% 0.24/0.87 ![A,D]: ((![B,C]: (~greek(A,B,C)|~greek(D,B,C)))|eq(D,A))),
% 0.24/0.87 inference(miniscoping,[status(thm)],[f9])).
% 0.24/0.87 fof(f31,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (~greek(X0,X1,X2)|~greek(X3,X1,X2)|eq(X3,X0))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f30])).
% 0.24/0.87 fof(f32,plain,(
% 0.24/0.87 ![X0,X1]: (latin(X0,X1,p1)|latin(X0,X1,p2))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f10])).
% 0.24/0.87 fof(f33,plain,(
% 0.24/0.87 ![X0,X1]: (latin(X0,p1,X1)|latin(X0,p2,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f11])).
% 0.24/0.87 fof(f34,plain,(
% 0.24/0.87 ![X0,X1]: (latin(p1,X0,X1)|latin(p2,X0,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f12])).
% 0.24/0.87 fof(f35,plain,(
% 0.24/0.87 ![X0,X1]: (greek(X0,X1,p1)|greek(X0,X1,p2))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f13])).
% 0.24/0.87 fof(f36,plain,(
% 0.24/0.87 ![X0,X1]: (greek(X0,p1,X1)|greek(X0,p2,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f14])).
% 0.24/0.87 fof(f37,plain,(
% 0.24/0.87 ![X0,X1]: (greek(p1,X0,X1)|greek(p2,X0,X1))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f15])).
% 0.24/0.87 fof(f38,plain,(
% 0.24/0.87 ![A,E]: ((![B,F]: ((![D]: ((![C]: ((~greek(A,B,C)|~latin(A,B,D))|~greek(E,F,C)))|~latin(E,F,D)))|eq(F,B)))|eq(E,A))),
% 0.24/0.87 inference(miniscoping,[status(thm)],[f16])).
% 0.24/0.87 fof(f39,plain,(
% 0.24/0.87 ![X0,X1,X2,X3,X4,X5]: (~greek(X0,X1,X2)|~latin(X0,X1,X3)|~greek(X4,X5,X2)|~latin(X4,X5,X3)|eq(X5,X1)|eq(X4,X0))),
% 0.24/0.87 inference(cnf_transformation,[status(thm)],[f38])).
% 0.24/0.87 fof(f40,plain,(
% 0.24/0.87 ![X0,X1]: (~greek(p2,X0,X1)|~greek(p1,X0,X1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f17,f31])).
% 0.24/0.87 fof(f41,plain,(
% 0.24/0.87 ![X0,X1]: (~greek(X0,p2,X1)|~greek(X0,p1,X1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f17,f29])).
% 0.24/0.87 fof(f43,plain,(
% 0.24/0.87 ![X0,X1]: (~latin(p2,X0,X1)|~latin(p1,X0,X1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f17,f25])).
% 0.24/0.87 fof(f44,plain,(
% 0.24/0.87 ![X0,X1]: (~latin(X0,p2,X1)|~latin(X0,p1,X1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f17,f23])).
% 0.24/0.87 fof(f46,plain,(
% 0.24/0.87 ~eq(p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f17,f19])).
% 0.24/0.87 fof(f54,plain,(
% 0.24/0.87 ![X0,X1,X2,X3,X4]: (greek(X0,X1,p1)|~greek(X2,X3,p2)|~latin(X2,X3,X4)|~latin(X0,X1,X4)|eq(X1,X3)|eq(X0,X2))),
% 0.24/0.87 inference(resolution,[status(thm)],[f35,f39])).
% 0.24/0.87 fof(f55,plain,(
% 0.24/0.87 ![X0,X1,X2,X3,X4]: (greek(X0,p1,X1)|~greek(X2,X3,X1)|~latin(X2,X3,X4)|~latin(X0,p2,X4)|eq(p2,X3)|eq(X0,X2))),
% 0.24/0.87 inference(resolution,[status(thm)],[f36,f39])).
% 0.24/0.87 fof(f56,plain,(
% 0.24/0.87 ![X0,X1,X2,X3,X4]: (greek(p1,X0,X1)|~greek(X2,X3,X1)|~latin(X2,X3,X4)|~latin(p2,X0,X4)|eq(X0,X3)|eq(p2,X2))),
% 0.24/0.87 inference(resolution,[status(thm)],[f37,f39])).
% 0.24/0.87 fof(f57,plain,(
% 0.24/0.87 ![X0]: (~greek(p2,p2,X0)|greek(p1,p1,X0))),
% 0.24/0.87 inference(resolution,[status(thm)],[f40,f36])).
% 0.24/0.87 fof(f58,plain,(
% 0.24/0.87 ![X0]: (~greek(p2,X0,p2)|greek(p1,X0,p1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f40,f35])).
% 0.24/0.87 fof(f61,plain,(
% 0.24/0.87 ![X0,X1,X2,X3,X4]: (greek(X0,X1,p1)|~latin(X2,X3,X4)|~latin(X0,X1,X4)|eq(X1,X3)|eq(X0,X2)|greek(X2,X3,p1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f54,f35])).
% 0.24/0.87 fof(f64,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (greek(X0,X1,p1)|~latin(X0,X1,p2)|eq(X1,X2)|eq(X0,X3)|greek(X3,X2,p1)|latin(X3,X2,p1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f61,f32])).
% 0.24/0.87 fof(f65,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (greek(p2,p1,X0)|~greek(X1,X2,X0)|~latin(X1,X2,X3)|eq(p2,X2)|eq(p2,X1)|latin(p1,p2,X3))),
% 0.24/0.87 inference(resolution,[status(thm)],[f55,f34])).
% 0.24/0.87 fof(f72,plain,(
% 0.24/0.87 ![X0]: (~latin(p2,p2,X0)|latin(p1,p1,X0))),
% 0.24/0.87 inference(resolution,[status(thm)],[f43,f33])).
% 0.24/0.87 fof(f79,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (greek(p1,p2,X0)|~greek(X1,X2,X0)|~latin(X1,X2,X3)|eq(p2,X2)|eq(p2,X1)|latin(p2,p1,X3))),
% 0.24/0.87 inference(resolution,[status(thm)],[f56,f33])).
% 0.24/0.87 fof(f104,plain,(
% 0.24/0.87 ![X0,X1,X2]: (greek(p2,p1,p2)|~latin(X0,X1,X2)|eq(p2,X1)|eq(p2,X0)|latin(p1,p2,X2)|greek(X0,X1,p1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f65,f35])).
% 0.24/0.87 fof(f128,plain,(
% 0.24/0.87 ![X0,X1,X2,X3]: (greek(X0,X1,p1)|eq(X1,X2)|eq(X0,X3)|greek(X3,X2,p1)|latin(X3,X2,p1)|latin(X0,X1,p1))),
% 0.24/0.87 inference(resolution,[status(thm)],[f64,f32])).
% 0.24/0.87 fof(f147,plain,(
% 0.24/0.87 greek(p2,p2,p1)|greek(p1,p1,p1)|latin(p1,p1,p1)|latin(p2,p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f128,f46])).
% 0.24/0.87 fof(f172,plain,(
% 0.24/0.87 greek(p1,p1,p1)|latin(p1,p1,p1)|latin(p2,p2,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f147,f57])).
% 0.24/0.87 fof(f284,plain,(
% 0.24/0.87 greek(p1,p1,p1)|latin(p1,p1,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f172,f72])).
% 0.24/0.87 fof(f286,plain,(
% 0.24/0.87 latin(p1,p1,p1)|~greek(p1,p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f284,f41])).
% 0.24/0.87 fof(f288,plain,(
% 0.24/0.87 ![X0]: (latin(p1,p1,p1)|greek(p1,p2,p1)|~latin(p1,p1,X0)|eq(p2,p1)|eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(resolution,[status(thm)],[f284,f79])).
% 0.24/0.87 fof(f293,plain,(
% 0.24/0.87 ![X0]: (latin(p1,p1,p1)|greek(p1,p2,p1)|~latin(p1,p1,X0)|eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(duplicate_literals_removal,[status(thm)],[f288])).
% 0.24/0.87 fof(f294,plain,(
% 0.24/0.87 ![X0]: (latin(p1,p1,p1)|greek(p1,p2,p1)|~latin(p1,p1,X0)|eq(p2,p1))),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f293,f25])).
% 0.24/0.87 fof(f364,plain,(
% 0.24/0.87 ![X0]: (latin(p1,p1,p1)|~latin(p1,p1,X0)|eq(p2,p1))),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f294,f286])).
% 0.24/0.87 fof(f365,plain,(
% 0.24/0.87 latin(p1,p1,p1)|eq(p2,p1)|latin(p1,p1,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f364,f32])).
% 0.24/0.87 fof(f366,plain,(
% 0.24/0.87 latin(p1,p1,p1)|eq(p2,p1)),
% 0.24/0.87 inference(duplicate_literals_removal,[status(thm)],[f365])).
% 0.24/0.87 fof(f367,plain,(
% 0.24/0.87 latin(p1,p1,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f366,f46])).
% 0.24/0.87 fof(f368,plain,(
% 0.24/0.87 ~latin(p2,p1,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f367,f43])).
% 0.24/0.87 fof(f369,plain,(
% 0.24/0.87 ~latin(p1,p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f367,f44])).
% 0.24/0.87 fof(f403,plain,(
% 0.24/0.87 greek(p2,p1,p2)|eq(p2,p1)|eq(p2,p1)|latin(p1,p2,p1)|greek(p1,p1,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f104,f367])).
% 0.24/0.87 fof(f409,plain,(
% 0.24/0.87 greek(p2,p1,p2)|eq(p2,p1)|latin(p1,p2,p1)|greek(p1,p1,p1)),
% 0.24/0.87 inference(duplicate_literals_removal,[status(thm)],[f403])).
% 0.24/0.87 fof(f410,plain,(
% 0.24/0.87 eq(p2,p1)|latin(p1,p2,p1)|greek(p1,p1,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f409,f58])).
% 0.24/0.87 fof(f532,plain,(
% 0.24/0.87 latin(p1,p2,p1)|greek(p1,p1,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f410,f46])).
% 0.24/0.87 fof(f533,plain,(
% 0.24/0.87 latin(p1,p2,p1)|~greek(p2,p1,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f532,f40])).
% 0.24/0.87 fof(f534,plain,(
% 0.24/0.87 latin(p1,p2,p1)|~greek(p1,p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f532,f41])).
% 0.24/0.87 fof(f542,plain,(
% 0.24/0.87 ~greek(p2,p1,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f533,f369])).
% 0.24/0.87 fof(f543,plain,(
% 0.24/0.87 ~greek(p1,p2,p1)),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f534,f369])).
% 0.24/0.87 fof(f553,plain,(
% 0.24/0.87 greek(p1,p1,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f542,f37])).
% 0.24/0.87 fof(f614,plain,(
% 0.24/0.87 ![X0]: (greek(p1,p2,p1)|~latin(p1,p1,X0)|eq(p2,p1)|eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(resolution,[status(thm)],[f553,f79])).
% 0.24/0.87 fof(f619,plain,(
% 0.24/0.87 ![X0]: (greek(p1,p2,p1)|~latin(p1,p1,X0)|eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(duplicate_literals_removal,[status(thm)],[f614])).
% 0.24/0.87 fof(f620,plain,(
% 0.24/0.87 ![X0]: (~latin(p1,p1,X0)|eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f619,f543])).
% 0.24/0.87 fof(f869,plain,(
% 0.24/0.87 ![X0]: (eq(p2,p1)|latin(p2,p1,X0))),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f620,f34])).
% 0.24/0.87 fof(f870,plain,(
% 0.24/0.87 eq(p2,p1)),
% 0.24/0.87 inference(resolution,[status(thm)],[f869,f368])).
% 0.24/0.87 fof(f889,plain,(
% 0.24/0.87 $false),
% 0.24/0.87 inference(forward_subsumption_resolution,[status(thm)],[f870,f46])).
% 0.24/0.87 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.90 % Elapsed time: 0.215418 seconds
% 0.24/0.90 % CPU time: 1.407658 seconds
% 0.24/0.90 % Total memory used: 26.025 MB
% 0.24/0.90 % Net memory used: 24.292 MB
%------------------------------------------------------------------------------