%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:06 PM UTC 2026
% Result : Unsatisfiable 0.96s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 10:45:27 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.96/0.67 % Refutation found
% 0.96/0.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.96/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.96/0.67 fof(f1,axiom,(
% 0.96/0.67 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f6,axiom,(
% 0.96/0.67 s0(b) = true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f12,axiom,(
% 0.96/0.67 n0(e,b) = true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f15,axiom,(
% 0.96/0.67 (![X]: (p0(b,X) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f16,axiom,(
% 0.96/0.67 n0(a,b) = true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f29,axiom,(
% 0.96/0.67 k0(e) = true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f32,axiom,(
% 0.96/0.67 m0(b,b,e) = true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f40,axiom,(
% 0.96/0.67 (![J,I]: (ifeq(n0(J,I),true,k1(I),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f68,axiom,(
% 0.96/0.67 (![H,I]: (ifeq(p0(H,I),true,ifeq(s0(H),true,m1(H,I,H),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f79,axiom,(
% 0.96/0.67 (![C,D]: (ifeq(m0(C,D,e),true,ifeq(k1(C),true,n1(C,e,e),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f122,axiom,(
% 0.96/0.67 (![C,B]: (ifeq(p0(C,B),true,p1(B,B,B),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f212,axiom,(
% 0.96/0.67 (![E,D]: (ifeq(m1(E,D,E),true,p2(D,E,D),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f213,axiom,(
% 0.96/0.67 (![E,F]: (ifeq(p1(E,E,E),true,ifeq(k0(F),true,q2(E,F,F),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f218,axiom,(
% 0.96/0.67 (![G,H,F]: (ifeq(q2(G,H,F),true,ifeq(p1(F,F,H),true,ifeq(n1(G,F,H),true,q2(F,G,F),true),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f274,axiom,(
% 0.96/0.67 (![E,F,D]: (ifeq(p2(E,F,D),true,n3(D),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f289,axiom,(
% 0.96/0.67 (![I,G,H]: (ifeq(q2(I,G,H),true,ifeq(n0(I,G),true,q3(G,H),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f330,axiom,(
% 0.96/0.67 (![H,I,G,J]: (ifeq(q3(H,I),true,ifeq(n3(G),true,ifeq(p0(J,G),true,r4(G),true),true),true) = true ))),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f363,negated_conjecture,(
% 0.96/0.67 r4(b) != true ),
% 0.96/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.96/0.67 fof(f364,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f1])).
% 0.96/0.67 fof(f369,plain,(
% 0.96/0.67 s0(b)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.96/0.67 fof(f375,plain,(
% 0.96/0.67 n0(e,b)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f12])).
% 0.96/0.67 fof(f378,plain,(
% 0.96/0.67 ![X0]: (p0(b,X0)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f15])).
% 0.96/0.67 fof(f379,plain,(
% 0.96/0.67 n0(a,b)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f16])).
% 0.96/0.67 fof(f392,plain,(
% 0.96/0.67 k0(e)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f29])).
% 0.96/0.67 fof(f395,plain,(
% 0.96/0.67 m0(b,b,e)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f32])).
% 0.96/0.67 fof(f403,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(n0(X0,X1),true,k1(X1),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f40])).
% 0.96/0.67 fof(f431,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(p0(X0,X1),true,ifeq(s0(X0),true,m1(X0,X1,X0),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f68])).
% 0.96/0.67 fof(f442,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(m0(X0,X1,e),true,ifeq(k1(X0),true,n1(X0,e,e),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f79])).
% 0.96/0.67 fof(f485,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(p0(X0,X1),true,p1(X1,X1,X1),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f122])).
% 0.96/0.67 fof(f575,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(m1(X0,X1,X0),true,p2(X1,X0,X1),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f212])).
% 0.96/0.67 fof(f576,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(p1(X0,X0,X0),true,ifeq(k0(X1),true,q2(X0,X1,X1),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f213])).
% 0.96/0.67 fof(f581,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q2(X0,X1,X2),true,ifeq(p1(X2,X2,X1),true,ifeq(n1(X0,X2,X1),true,q2(X2,X0,X2),true),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f218])).
% 0.96/0.67 fof(f637,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(p2(X0,X1,X2),true,n3(X2),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f274])).
% 0.96/0.67 fof(f652,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q2(X0,X1,X2),true,ifeq(n0(X0,X1),true,q3(X1,X2),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f289])).
% 0.96/0.67 fof(f693,plain,(
% 0.96/0.67 ![X0,X1,X2,X3]: (ifeq(q3(X0,X1),true,ifeq(n3(X2),true,ifeq(p0(X3,X2),true,r4(X2),true),true),true)=true)),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f330])).
% 0.96/0.67 fof(f726,plain,(
% 0.96/0.67 ~r4(b)=true),
% 0.96/0.67 inference(cnf_transformation,[status(thm)],[f363])).
% 0.96/0.67 fof(f860,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,ifeq(n3(X2),true,ifeq(true,true,r4(X2),true),true),true)=true)),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f378,f693])).
% 0.96/0.67 fof(f861,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,ifeq(n3(X2),true,r4(X2),true),true)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f860])).
% 0.96/0.67 fof(f868,plain,(
% 0.96/0.67 ifeq(true,true,k1(b),true)=true),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f379,f403])).
% 0.96/0.67 fof(f878,plain,(
% 0.96/0.67 k1(b)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f868])).
% 0.96/0.67 fof(f1147,plain,(
% 0.96/0.67 ![X0]: (ifeq(true,true,ifeq(s0(b),true,m1(b,X0,b),true),true)=true)),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f378,f431])).
% 0.96/0.67 fof(f1152,plain,(
% 0.96/0.67 ![X0]: (ifeq(s0(b),true,m1(b,X0,b),true)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f1147])).
% 0.96/0.67 fof(f1153,plain,(
% 0.96/0.67 ![X0]: (ifeq(true,true,m1(b,X0,b),true)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f369,f1152])).
% 0.96/0.67 fof(f1158,plain,(
% 0.96/0.67 ![X0]: (m1(b,X0,b)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f1153])).
% 0.96/0.67 fof(f1220,plain,(
% 0.96/0.67 ifeq(true,true,ifeq(k1(b),true,n1(b,e,e),true),true)=true),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f395,f442])).
% 0.96/0.67 fof(f1228,plain,(
% 0.96/0.67 ifeq(k1(b),true,n1(b,e,e),true)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f1220])).
% 0.96/0.67 fof(f1229,plain,(
% 0.96/0.67 ifeq(true,true,n1(b,e,e),true)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f878,f1228])).
% 0.96/0.67 fof(f1230,plain,(
% 0.96/0.67 n1(b,e,e)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f1229])).
% 0.96/0.67 fof(f2354,plain,(
% 0.96/0.67 ![X0]: (ifeq(true,true,p1(X0,X0,X0),true)=true)),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f378,f485])).
% 0.96/0.67 fof(f2390,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(true,true,ifeq(k0(X0),true,q2(X1,X0,X0),true),true)=true)),
% 0.96/0.67 inference(backward_demodulation,[status(thm)],[f2393,f576])).
% 0.96/0.67 fof(f2393,plain,(
% 0.96/0.67 ![X0]: (p1(X0,X0,X0)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f2354])).
% 0.96/0.67 fof(f2433,plain,(
% 0.96/0.67 ![X0,X1]: (ifeq(k0(X0),true,q2(X1,X0,X0),true)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f2390])).
% 0.96/0.67 fof(f3494,plain,(
% 0.96/0.67 ![X0]: (ifeq(true,true,p2(X0,b,X0),true)=true)),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f1158,f575])).
% 0.96/0.67 fof(f3500,plain,(
% 0.96/0.67 ![X0]: (p2(X0,b,X0)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f3494])).
% 0.96/0.67 fof(f3538,plain,(
% 0.96/0.67 ifeq(q2(b,e,e),true,ifeq(p1(e,e,e),true,ifeq(true,true,q2(e,b,e),true),true),true)=true),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f1230,f581])).
% 0.96/0.67 fof(f3563,plain,(
% 0.96/0.67 ifeq(q2(b,e,e),true,ifeq(true,true,ifeq(true,true,q2(e,b,e),true),true),true)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f2393,f3538])).
% 0.96/0.67 fof(f3564,plain,(
% 0.96/0.67 ifeq(q2(b,e,e),true,ifeq(true,true,q2(e,b,e),true),true)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f3563])).
% 0.96/0.67 fof(f3565,plain,(
% 0.96/0.67 ifeq(q2(b,e,e),true,q2(e,b,e),true)=true),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f3564])).
% 0.96/0.67 fof(f3828,plain,(
% 0.96/0.67 ![X0]: (ifeq(true,true,n3(X0),true)=true)),
% 0.96/0.67 inference(paramodulation,[status(thm)],[f3500,f637])).
% 0.96/0.67 fof(f3837,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,ifeq(true,true,r4(X2),true),true)=true)),
% 0.96/0.67 inference(backward_demodulation,[status(thm)],[f3847,f861])).
% 0.96/0.67 fof(f3847,plain,(
% 0.96/0.67 ![X0]: (n3(X0)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f3828])).
% 0.96/0.67 fof(f3850,plain,(
% 0.96/0.67 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,r4(X2),true)=true)),
% 0.96/0.67 inference(forward_demodulation,[status(thm)],[f364,f3837])).
% 0.96/0.68 fof(f4459,plain,(
% 0.96/0.68 ![X0]: (ifeq(true,true,q2(X0,e,e),true)=true)),
% 0.96/0.68 inference(paramodulation,[status(thm)],[f392,f2433])).
% 0.96/0.68 fof(f4462,plain,(
% 0.96/0.68 ifeq(true,true,q2(e,b,e),true)=true),
% 0.96/0.68 inference(backward_demodulation,[status(thm)],[f4463,f3565])).
% 0.96/0.68 fof(f4463,plain,(
% 0.96/0.68 ![X0]: (q2(X0,e,e)=true)),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f364,f4459])).
% 0.96/0.68 fof(f4464,plain,(
% 0.96/0.68 q2(e,b,e)=true),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f364,f4462])).
% 0.96/0.68 fof(f4542,plain,(
% 0.96/0.68 ifeq(true,true,ifeq(n0(e,b),true,q3(b,e),true),true)=true),
% 0.96/0.68 inference(paramodulation,[status(thm)],[f4464,f652])).
% 0.96/0.68 fof(f4548,plain,(
% 0.96/0.68 ifeq(n0(e,b),true,q3(b,e),true)=true),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f364,f4542])).
% 0.96/0.68 fof(f4549,plain,(
% 0.96/0.68 ifeq(true,true,q3(b,e),true)=true),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f375,f4548])).
% 0.96/0.68 fof(f4551,plain,(
% 0.96/0.68 q3(b,e)=true),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f364,f4549])).
% 0.96/0.68 fof(f4597,plain,(
% 0.96/0.68 ![X0]: (ifeq(true,true,r4(X0),true)=true)),
% 0.96/0.68 inference(paramodulation,[status(thm)],[f4551,f3850])).
% 0.96/0.68 fof(f4611,plain,(
% 0.96/0.68 ~true=true),
% 0.96/0.68 inference(backward_demodulation,[status(thm)],[f4616,f726])).
% 0.96/0.68 fof(f4616,plain,(
% 0.96/0.68 ![X0]: (r4(X0)=true)),
% 0.96/0.68 inference(forward_demodulation,[status(thm)],[f364,f4597])).
% 0.96/0.68 fof(f4618,plain,(
% 0.96/0.68 $false),
% 0.96/0.68 inference(trivial_equality_resolution,[status(thm)],[f4611])).
% 0.96/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.96/0.70 % Elapsed time: 0.333913 seconds
% 0.96/0.70 % CPU time: 2.342030 seconds
% 0.96/0.70 % Total memory used: 91.418 MB
% 0.96/0.70 % Net memory used: 87.869 MB
%------------------------------------------------------------------------------