%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN214-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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.13s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN214-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n026.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 10:48:53 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.13/0.58 % Refutation found
% 0.13/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.58 fof(f1,axiom,(
% 0.13/0.58 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f6,axiom,(
% 0.13/0.58 s0(b) = true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f12,axiom,(
% 0.13/0.58 n0(e,b) = true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f15,axiom,(
% 0.13/0.58 (![X]: (p0(b,X) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f16,axiom,(
% 0.13/0.58 n0(a,b) = true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f29,axiom,(
% 0.13/0.58 k0(e) = true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f32,axiom,(
% 0.13/0.58 m0(b,b,e) = true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f40,axiom,(
% 0.13/0.58 (![J,I]: (ifeq(n0(J,I),true,k1(I),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f68,axiom,(
% 0.13/0.58 (![H,I]: (ifeq(p0(H,I),true,ifeq(s0(H),true,m1(H,I,H),true),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f79,axiom,(
% 0.13/0.58 (![C,D]: (ifeq(m0(C,D,e),true,ifeq(k1(C),true,n1(C,e,e),true),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f122,axiom,(
% 0.13/0.58 (![C,B]: (ifeq(p0(C,B),true,p1(B,B,B),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f173,axiom,(
% 0.13/0.58 (![B,C,A]: (ifeq(p1(B,C,A),true,n2(A),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f212,axiom,(
% 0.13/0.58 (![E,D]: (ifeq(m1(E,D,E),true,p2(D,E,D),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f213,axiom,(
% 0.13/0.58 (![E,F]: (ifeq(p1(E,E,E),true,ifeq(k0(F),true,q2(E,F,F),true),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f218,axiom,(
% 0.13/0.58 (![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.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f274,axiom,(
% 0.13/0.58 (![E,F,D]: (ifeq(p2(E,F,D),true,n3(D),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f278,axiom,(
% 0.13/0.58 (![H]: (ifeq(n2(H),true,p3(H,H,H),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f289,axiom,(
% 0.13/0.58 (![I,G,H]: (ifeq(q2(I,G,H),true,ifeq(n0(I,G),true,q3(G,H),true),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f310,axiom,(
% 0.13/0.58 (![A,B,J]: (ifeq(p3(A,B,J),true,l4(J),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f330,axiom,(
% 0.13/0.58 (![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.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f361,axiom,(
% 0.13/0.58 (![I,H]: (ifeq(r4(I),true,ifeq(l4(H),true,s5(H),true),true) = true ))),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f363,negated_conjecture,(
% 0.13/0.58 s5(c) != true ),
% 0.13/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f364,plain,(
% 0.13/0.58 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.58 fof(f369,plain,(
% 0.13/0.58 s0(b)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.58 fof(f375,plain,(
% 0.13/0.58 n0(e,b)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.58 fof(f378,plain,(
% 0.13/0.58 ![X0]: (p0(b,X0)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.58 fof(f379,plain,(
% 0.13/0.58 n0(a,b)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.58 fof(f392,plain,(
% 0.13/0.58 k0(e)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.58 fof(f395,plain,(
% 0.13/0.58 m0(b,b,e)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/0.58 fof(f403,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(n0(X0,X1),true,k1(X1),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.58 fof(f431,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(p0(X0,X1),true,ifeq(s0(X0),true,m1(X0,X1,X0),true),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f68])).
% 0.13/0.58 fof(f442,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(m0(X0,X1,e),true,ifeq(k1(X0),true,n1(X0,e,e),true),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f79])).
% 0.13/0.58 fof(f485,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(p0(X0,X1),true,p1(X1,X1,X1),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f122])).
% 0.13/0.58 fof(f536,plain,(
% 0.13/0.58 ![X0,X1,X2]: (ifeq(p1(X0,X1,X2),true,n2(X2),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f173])).
% 0.13/0.58 fof(f575,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(m1(X0,X1,X0),true,p2(X1,X0,X1),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f212])).
% 0.13/0.58 fof(f576,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(p1(X0,X0,X0),true,ifeq(k0(X1),true,q2(X0,X1,X1),true),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f213])).
% 0.13/0.58 fof(f581,plain,(
% 0.13/0.58 ![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.13/0.58 inference(cnf_transformation,[status(thm)],[f218])).
% 0.13/0.58 fof(f637,plain,(
% 0.13/0.58 ![X0,X1,X2]: (ifeq(p2(X0,X1,X2),true,n3(X2),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f274])).
% 0.13/0.58 fof(f641,plain,(
% 0.13/0.58 ![X0]: (ifeq(n2(X0),true,p3(X0,X0,X0),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f278])).
% 0.13/0.58 fof(f652,plain,(
% 0.13/0.58 ![X0,X1,X2]: (ifeq(q2(X0,X1,X2),true,ifeq(n0(X0,X1),true,q3(X1,X2),true),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f289])).
% 0.13/0.58 fof(f673,plain,(
% 0.13/0.58 ![X0,X1,X2]: (ifeq(p3(X0,X1,X2),true,l4(X2),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f310])).
% 0.13/0.58 fof(f693,plain,(
% 0.13/0.58 ![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.13/0.58 inference(cnf_transformation,[status(thm)],[f330])).
% 0.13/0.58 fof(f724,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(r4(X0),true,ifeq(l4(X1),true,s5(X1),true),true)=true)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f361])).
% 0.13/0.58 fof(f726,plain,(
% 0.13/0.58 ~s5(c)=true),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f363])).
% 0.13/0.58 fof(f727,definition,(
% 0.13/0.58 sF0_fnc=s5(c)),
% 0.13/0.58 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.13/0.58 fof(f728,plain,(
% 0.13/0.58 ~sF0_fnc=true),
% 0.13/0.58 inference(definition_folding,[],[f726,f727])).
% 0.13/0.58 fof(f737,plain,(
% 0.13/0.58 ifeq(true,true,k1(b),true)=true),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f379,f403])).
% 0.13/0.58 fof(f745,plain,(
% 0.13/0.58 k1(b)=true),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f737])).
% 0.13/0.58 fof(f1068,plain,(
% 0.13/0.58 ![X0]: (ifeq(true,true,ifeq(s0(b),true,m1(b,X0,b),true),true)=true)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f378,f431])).
% 0.13/0.58 fof(f1075,plain,(
% 0.13/0.58 ![X0]: (ifeq(s0(b),true,m1(b,X0,b),true)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f1068])).
% 0.13/0.58 fof(f1076,plain,(
% 0.13/0.58 ![X0]: (ifeq(true,true,m1(b,X0,b),true)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f369,f1075])).
% 0.13/0.58 fof(f1077,plain,(
% 0.13/0.58 ![X0]: (m1(b,X0,b)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f1076])).
% 0.13/0.58 fof(f1233,plain,(
% 0.13/0.58 ifeq(true,true,ifeq(k1(b),true,n1(b,e,e),true),true)=true),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f395,f442])).
% 0.13/0.58 fof(f1241,plain,(
% 0.13/0.58 ifeq(k1(b),true,n1(b,e,e),true)=true),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f1233])).
% 0.13/0.58 fof(f1242,plain,(
% 0.13/0.58 ifeq(true,true,n1(b,e,e),true)=true),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f745,f1241])).
% 0.13/0.58 fof(f1243,plain,(
% 0.13/0.58 n1(b,e,e)=true),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f1242])).
% 0.13/0.58 fof(f2609,plain,(
% 0.13/0.58 ![X0]: (ifeq(true,true,p1(X0,X0,X0),true)=true)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f378,f485])).
% 0.13/0.58 fof(f2617,plain,(
% 0.13/0.58 ![X0]: (p1(X0,X0,X0)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f2609])).
% 0.13/0.58 fof(f3586,plain,(
% 0.13/0.58 ![X0]: (ifeq(true,true,n2(X0),true)=true)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f2617,f536])).
% 0.13/0.58 fof(f3591,plain,(
% 0.13/0.58 ![X0]: (n2(X0)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f3586])).
% 0.13/0.58 fof(f3999,plain,(
% 0.13/0.58 ![X0]: (ifeq(true,true,p2(X0,b,X0),true)=true)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f1077,f575])).
% 0.13/0.58 fof(f4007,plain,(
% 0.13/0.58 ![X0]: (p2(X0,b,X0)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f364,f3999])).
% 0.13/0.58 fof(f4037,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(true,true,ifeq(k0(X0),true,q2(X1,X0,X0),true),true)=true)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f2617,f576])).
% 0.13/0.58 fof(f4038,plain,(
% 0.13/0.58 ![X0,X1]: (ifeq(k0(X0),true,q2(X1,X0,X0),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4037])).
% 0.13/0.60 fof(f4040,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,q2(X0,e,e),true)=true)),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f392,f4038])).
% 0.13/0.60 fof(f4042,plain,(
% 0.13/0.60 ![X0]: (q2(X0,e,e)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4040])).
% 0.13/0.60 fof(f4157,plain,(
% 0.13/0.60 ifeq(q2(b,e,e),true,ifeq(p1(e,e,e),true,ifeq(true,true,q2(e,b,e),true),true),true)=true),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f1243,f581])).
% 0.13/0.60 fof(f4191,plain,(
% 0.13/0.60 ifeq(true,true,ifeq(p1(e,e,e),true,ifeq(true,true,q2(e,b,e),true),true),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f4042,f4157])).
% 0.13/0.60 fof(f4192,plain,(
% 0.13/0.60 ifeq(p1(e,e,e),true,ifeq(true,true,q2(e,b,e),true),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4191])).
% 0.13/0.60 fof(f4193,plain,(
% 0.13/0.60 ifeq(true,true,ifeq(true,true,q2(e,b,e),true),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f2617,f4192])).
% 0.13/0.60 fof(f4194,plain,(
% 0.13/0.60 ifeq(true,true,q2(e,b,e),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4193])).
% 0.13/0.60 fof(f4195,plain,(
% 0.13/0.60 q2(e,b,e)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4194])).
% 0.13/0.60 fof(f4517,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,p3(X0,X0,X0),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f3591,f641])).
% 0.13/0.60 fof(f4518,plain,(
% 0.13/0.60 ![X0]: (p3(X0,X0,X0)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4517])).
% 0.13/0.60 fof(f4524,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,l4(X0),true)=true)),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f4518,f673])).
% 0.13/0.60 fof(f4525,plain,(
% 0.13/0.60 ![X0]: (l4(X0)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4524])).
% 0.13/0.60 fof(f4746,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,n3(X0),true)=true)),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f4007,f637])).
% 0.13/0.60 fof(f4752,plain,(
% 0.13/0.60 ![X0]: (n3(X0)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4746])).
% 0.13/0.60 fof(f4848,plain,(
% 0.13/0.60 ifeq(true,true,ifeq(n0(e,b),true,q3(b,e),true),true)=true),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f4195,f652])).
% 0.13/0.60 fof(f4860,plain,(
% 0.13/0.60 ifeq(n0(e,b),true,q3(b,e),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4848])).
% 0.13/0.60 fof(f4861,plain,(
% 0.13/0.60 ifeq(true,true,q3(b,e),true)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f375,f4860])).
% 0.13/0.60 fof(f4862,plain,(
% 0.13/0.60 q3(b,e)=true),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f4861])).
% 0.13/0.60 fof(f5390,plain,(
% 0.13/0.60 ![X0,X1,X2,X3]: (ifeq(q3(X0,X1),true,ifeq(true,true,ifeq(p0(X2,X3),true,r4(X3),true),true),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f4752,f693])).
% 0.13/0.60 fof(f5391,plain,(
% 0.13/0.60 ![X0,X1,X2,X3]: (ifeq(q3(X0,X1),true,ifeq(p0(X2,X3),true,r4(X3),true),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f5390])).
% 0.13/0.60 fof(f5394,plain,(
% 0.13/0.60 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,ifeq(true,true,r4(X2),true),true)=true)),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f378,f5391])).
% 0.13/0.60 fof(f5397,plain,(
% 0.13/0.60 ![X0,X1,X2]: (ifeq(q3(X0,X1),true,r4(X2),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f5394])).
% 0.13/0.60 fof(f5398,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,r4(X0),true)=true)),
% 0.13/0.60 inference(paramodulation,[status(thm)],[f4862,f5397])).
% 0.13/0.60 fof(f5399,plain,(
% 0.13/0.60 ![X0]: (r4(X0)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f5398])).
% 0.13/0.60 fof(f5601,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,ifeq(l4(X0),true,s5(X0),true),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f5399,f724])).
% 0.13/0.60 fof(f5602,plain,(
% 0.13/0.60 ![X0]: (ifeq(l4(X0),true,s5(X0),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f5601])).
% 0.13/0.60 fof(f5603,plain,(
% 0.13/0.60 ![X0]: (ifeq(true,true,s5(X0),true)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f4525,f5602])).
% 0.13/0.60 fof(f5604,plain,(
% 0.13/0.60 sF0_fnc=true),
% 0.13/0.60 inference(backward_demodulation,[status(thm)],[f5605,f727])).
% 0.13/0.60 fof(f5605,plain,(
% 0.13/0.60 ![X0]: (s5(X0)=true)),
% 0.13/0.60 inference(forward_demodulation,[status(thm)],[f364,f5603])).
% 0.13/0.60 fof(f5606,plain,(
% 0.13/0.60 $false),
% 0.13/0.60 inference(forward_subsumption_resolution,[status(thm)],[f5604,f728])).
% 0.13/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 1.38/0.61 % Elapsed time: 0.244206 seconds
% 1.38/0.61 % CPU time: 1.681016 seconds
% 1.38/0.61 % Total memory used: 86.859 MB
% 1.38/0.61 % Net memory used: 84.810 MB
%------------------------------------------------------------------------------