%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN214-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 : n004.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.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN214-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/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 10:46:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f14,axiom,(
% 0.14/0.41 (![X]: (p0(b,X) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f24,axiom,(
% 0.14/0.41 l0(c) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f28,axiom,(
% 0.14/0.41 k0(e) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f30,axiom,(
% 0.14/0.41 n0(e,e) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f39,axiom,(
% 0.14/0.41 (![I,J]: (( k1(I)| ~ n0(J,I) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f117,axiom,(
% 0.14/0.41 (![A]: (( p1(A,A,A)| ~ k0(e)| ~ k1(A)| ~ l0(c) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f123,axiom,(
% 0.14/0.41 (![B,C]: (( p1(B,B,B)| ~ p0(C,B) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f175,axiom,(
% 0.14/0.41 (![A,B,C]: (( n2(A)| ~ p1(B,C,A) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f212,axiom,(
% 0.14/0.41 (![H]: (( p2(H,H,H)| ~ n2(H)| ~ k1(e) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f219,axiom,(
% 0.14/0.41 (![I]: (( q2(I,I,I)| ~ p1(I,I,I) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f278,axiom,(
% 0.14/0.41 (![D,E,F]: (( n3(D)| ~ p2(E,F,D) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f282,axiom,(
% 0.14/0.41 (![H]: (( p3(H,H,H)| ~ n2(H) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f293,axiom,(
% 0.14/0.41 (![G,H,I]: (( q3(G,H)| ~ q2(I,G,H)| ~ n0(I,G) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f315,axiom,(
% 0.14/0.41 (![J,A,B]: (( l4(J)| ~ p3(A,B,J) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f336,axiom,(
% 0.14/0.41 (![G,H,I,J]: (( r4(G)| ~ n3(G)| ~ q3(H,I)| ~ p0(J,G) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f367,axiom,(
% 0.14/0.41 (![H,I]: (( s5(H)| ~ l4(H)| ~ r4(I) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f369,negated_conjecture,(
% 0.14/0.41 ~ s5(c) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f383,plain,(
% 0.14/0.41 ![X0]: (p0(b,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/0.41 fof(f393,plain,(
% 0.14/0.41 l0(c)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.41 fof(f397,plain,(
% 0.14/0.41 k0(e)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.41 fof(f399,plain,(
% 0.14/0.41 n0(e,e)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.41 fof(f408,plain,(
% 0.14/0.41 ![I]: (k1(I)|(![J]: ~n0(J,I)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f39])).
% 0.14/0.41 fof(f409,plain,(
% 0.14/0.41 ![X0,X1]: (k1(X0)|~n0(X1,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f408])).
% 0.14/0.41 fof(f532,plain,(
% 0.14/0.41 (![A]: ((p1(A,A,A)|~k0(e))|~k1(A)))|~l0(c)),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f117])).
% 0.14/0.41 fof(f533,plain,(
% 0.14/0.41 ![X0]: (p1(X0,X0,X0)|~k0(e)|~k1(X0)|~l0(c))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f532])).
% 0.14/0.41 fof(f544,plain,(
% 0.14/0.41 ![B]: (p1(B,B,B)|(![C]: ~p0(C,B)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f123])).
% 0.14/0.41 fof(f545,plain,(
% 0.14/0.41 ![X0,X1]: (p1(X0,X0,X0)|~p0(X1,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f544])).
% 0.14/0.41 fof(f626,plain,(
% 0.14/0.41 ![A]: (n2(A)|(![B,C]: ~p1(B,C,A)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f175])).
% 0.14/0.41 fof(f627,plain,(
% 0.14/0.41 ![X0,X1,X2]: (n2(X0)|~p1(X1,X2,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f626])).
% 0.14/0.41 fof(f681,plain,(
% 0.14/0.41 (![H]: (p2(H,H,H)|~n2(H)))|~k1(e)),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f212])).
% 0.14/0.41 fof(f682,plain,(
% 0.14/0.41 ![X0]: (p2(X0,X0,X0)|~n2(X0)|~k1(e))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f681])).
% 0.14/0.41 fof(f692,plain,(
% 0.14/0.41 ![X0]: (q2(X0,X0,X0)|~p1(X0,X0,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f219])).
% 0.14/0.41 fof(f778,plain,(
% 0.14/0.41 ![D]: (n3(D)|(![E,F]: ~p2(E,F,D)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f278])).
% 0.14/0.41 fof(f779,plain,(
% 0.14/0.41 ![X0,X1,X2]: (n3(X0)|~p2(X1,X2,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f778])).
% 0.14/0.41 fof(f784,plain,(
% 0.14/0.41 ![X0]: (p3(X0,X0,X0)|~n2(X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f282])).
% 0.14/0.41 fof(f801,plain,(
% 0.14/0.41 ![G,I]: ((![H]: (q3(G,H)|~q2(I,G,H)))|~n0(I,G))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f293])).
% 0.14/0.41 fof(f802,plain,(
% 0.14/0.41 ![X0,X1,X2]: (q3(X0,X1)|~q2(X2,X0,X1)|~n0(X2,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f801])).
% 0.14/0.41 fof(f836,plain,(
% 0.14/0.41 ![J]: (l4(J)|(![A,B]: ~p3(A,B,J)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f315])).
% 0.14/0.41 fof(f837,plain,(
% 0.14/0.41 ![X0,X1,X2]: (l4(X0)|~p3(X1,X2,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f836])).
% 0.14/0.41 fof(f871,plain,(
% 0.14/0.41 ![G]: (((r4(G)|~n3(G))|(![H,I]: ~q3(H,I)))|(![J]: ~p0(J,G)))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f336])).
% 0.14/0.41 fof(f872,plain,(
% 0.14/0.41 ![X0,X1,X2,X3]: (r4(X0)|~n3(X0)|~q3(X1,X2)|~p0(X3,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f871])).
% 0.14/0.41 fof(f920,plain,(
% 0.14/0.41 (![H]: (s5(H)|~l4(H)))|(![I]: ~r4(I))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f367])).
% 0.14/0.41 fof(f921,plain,(
% 0.14/0.41 ![X0,X1]: (s5(X0)|~l4(X0)|~r4(X1))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f920])).
% 0.14/0.41 fof(f924,plain,(
% 0.14/0.41 ~s5(c)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f369])).
% 0.14/0.41 fof(f943,plain,(
% 0.14/0.41 ![X0]: (p1(X0,X0,X0)|~k1(X0)|~l0(c))),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f533,f397])).
% 0.14/0.41 fof(f969,plain,(
% 0.14/0.41 k1(e)),
% 0.14/0.41 inference(resolution,[status(thm)],[f409,f399])).
% 0.14/0.41 fof(f976,plain,(
% 0.14/0.41 ![X0]: (p2(X0,X0,X0)|~n2(X0))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f682,f969])).
% 0.14/0.41 fof(f1014,plain,(
% 0.14/0.41 ![X0]: (p1(X0,X0,X0)|~k1(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f943,f393])).
% 0.14/0.41 fof(f1031,plain,(
% 0.14/0.41 ![X0,X1]: (~p0(X0,X1)|n2(X1))),
% 0.14/0.41 inference(resolution,[status(thm)],[f545,f627])).
% 0.14/0.41 fof(f1043,plain,(
% 0.14/0.41 ![X0]: (n2(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1031,f383])).
% 0.14/0.41 fof(f1045,plain,(
% 0.14/0.41 ![X0]: (p2(X0,X0,X0))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f976,f1043])).
% 0.14/0.41 fof(f1046,plain,(
% 0.14/0.41 ![X0]: (p3(X0,X0,X0))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f784,f1043])).
% 0.14/0.41 fof(f1120,plain,(
% 0.14/0.41 ![X0]: (n3(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f779,f1045])).
% 0.14/0.41 fof(f1125,plain,(
% 0.14/0.41 ![X0,X1,X2,X3]: (r4(X0)|~q3(X1,X2)|~p0(X3,X0))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f872,f1120])).
% 0.14/0.41 fof(f1128,plain,(
% 0.14/0.41 ![X0]: (l4(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f837,f1046])).
% 0.14/0.41 fof(f1130,plain,(
% 0.14/0.41 ![X0,X1]: (s5(X0)|~r4(X1))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f921,f1128])).
% 0.14/0.41 fof(f1163,plain,(
% 0.14/0.41 ![X0]: (~k1(X0)|q2(X0,X0,X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1014,f692])).
% 0.14/0.41 fof(f1171,plain,(
% 0.14/0.41 ![X0]: (q3(e,X0)|~q2(e,e,X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f802,f399])).
% 0.14/0.41 fof(f1464,plain,(
% 0.14/0.41 q3(e,e)|~k1(e)),
% 0.14/0.41 inference(resolution,[status(thm)],[f1171,f1163])).
% 0.14/0.41 fof(f1472,plain,(
% 0.14/0.41 q3(e,e)),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1464,f969])).
% 0.14/0.41 fof(f1482,plain,(
% 0.14/0.41 ![X0,X1]: (r4(X0)|~p0(X1,X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1472,f1125])).
% 0.14/0.41 fof(f1487,plain,(
% 0.14/0.41 ![X0]: (r4(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f1482,f383])).
% 0.14/0.41 fof(f1488,plain,(
% 0.14/0.41 ![X0]: (s5(X0))),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f1130,f1487])).
% 0.14/0.41 fof(f1490,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(backward_subsumption_resolution,[status(thm)],[f924,f1488])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 1.37/1.66 % Elapsed time: 1.068325 seconds
% 1.37/1.66 % CPU time: 0.210767 seconds
% 1.37/1.66 % Total memory used: 45.539 MB
% 1.37/1.66 % Net memory used: 45.373 MB
%------------------------------------------------------------------------------