%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:01 PM UTC 2026
% Result : Unsatisfiable 2.95s 0.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:47:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 2.95/0.80 % Refutation found
% 2.95/0.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.95/0.80 % SZS output start CNFRefutation for theBenchmark
% 2.95/0.80 fof(f1,axiom,(
% 2.95/0.80 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f6,axiom,(
% 2.95/0.80 s0(b) = true ),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f15,axiom,(
% 2.95/0.80 (![X]: (p0(b,X) = true ))),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f18,axiom,(
% 2.95/0.80 (![X]: (q0(X,d) = true ))),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f20,axiom,(
% 2.95/0.80 (![X,Y]: (m0(X,d,Y) = true ))),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f21,axiom,(
% 2.95/0.80 l0(a) = true ),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f33,axiom,(
% 2.95/0.80 k0(b) = true ),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f35,axiom,(
% 2.95/0.80 n0(c,d) = true ),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.80 fof(f38,axiom,(
% 2.95/0.80 n0(b,a) = true ),
% 2.95/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f41,axiom,(
% 2.95/0.81 (![H,G]: (ifeq(n0(H,G),true,l1(G,G),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f88,axiom,(
% 2.95/0.81 (![D,E]: (ifeq(l0(D),true,ifeq(p0(b,E),true,ifeq(s0(b),true,n1(D,E,D),true),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f92,axiom,(
% 2.95/0.81 (![E,F,G]: (ifeq(n1(E,F,E),true,ifeq(l0(G),true,ifeq(l1(G,E),true,n1(E,F,F),true),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f122,axiom,(
% 2.95/0.81 (![C,B]: (ifeq(p0(C,B),true,p1(B,B,B),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f144,axiom,(
% 2.95/0.81 (![A]: (ifeq(m0(e,d,A),true,ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f162,axiom,(
% 2.95/0.81 (![I]: (ifeq(p0(I,I),true,s1(I),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f163,axiom,(
% 2.95/0.81 (![H,F,G]: (ifeq(s1(H),true,ifeq(q0(F,G),true,s1(F),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f166,axiom,(
% 2.95/0.81 (![A,J]: (ifeq(q1(A,J,J),true,k2(J,J),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f169,axiom,(
% 2.95/0.81 (![B,A,C,J]: (ifeq(s1(B),true,ifeq(p0(A,A),true,ifeq(m0(C,B,J),true,l2(J,J),true),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f213,axiom,(
% 2.95/0.81 (![E,F]: (ifeq(p1(E,E,E),true,ifeq(k0(F),true,q2(E,F,F),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f217,axiom,(
% 2.95/0.81 (![I]: (ifeq(p1(I,I,I),true,q2(I,I,I),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f218,axiom,(
% 2.95/0.81 (![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 ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f225,axiom,(
% 2.95/0.81 (![H]: (ifeq(q2(b,H,b),true,ifeq(s1(b),true,s2(H),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f275,axiom,(
% 2.95/0.81 (![F,C,D,E]: (ifeq(q2(F,d,C),true,ifeq(k2(D,E),true,p3(C,D,E),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f307,axiom,(
% 2.95/0.81 (![I,A,B,J]: (ifeq(s2(I),true,ifeq(q2(A,I,A),true,ifeq(m0(A,B,J),true,s3(I,J),true),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f312,axiom,(
% 2.95/0.81 (![E,G,F]: (ifeq(s3(a,E),true,ifeq(l2(G,F),true,m4(E,F),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f331,axiom,(
% 2.95/0.81 (![B,C,D,A]: (ifeq(p3(B,C,D),true,ifeq(l1(A,C),true,s4(A),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f337,axiom,(
% 2.95/0.81 (![B]: (ifeq(s4(B),true,ifeq(m4(e,e),true,m5(B,B),true),true) = true ))),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f363,negated_conjecture,(
% 2.95/0.81 m5(d,d) != true ),
% 2.95/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.95/0.81 fof(f364,plain,(
% 2.95/0.81 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f1])).
% 2.95/0.81 fof(f369,plain,(
% 2.95/0.81 s0(b)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f6])).
% 2.95/0.81 fof(f378,plain,(
% 2.95/0.81 ![X0]: (p0(b,X0)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f15])).
% 2.95/0.81 fof(f381,plain,(
% 2.95/0.81 ![X0]: (q0(X0,d)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f18])).
% 2.95/0.81 fof(f383,plain,(
% 2.95/0.81 ![X0,X1]: (m0(X0,d,X1)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f20])).
% 2.95/0.81 fof(f384,plain,(
% 2.95/0.81 l0(a)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f21])).
% 2.95/0.81 fof(f396,plain,(
% 2.95/0.81 k0(b)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f33])).
% 2.95/0.81 fof(f398,plain,(
% 2.95/0.81 n0(c,d)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f35])).
% 2.95/0.81 fof(f401,plain,(
% 2.95/0.81 n0(b,a)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f38])).
% 2.95/0.81 fof(f404,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(n0(X0,X1),true,l1(X1,X1),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f41])).
% 2.95/0.81 fof(f451,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l0(X0),true,ifeq(p0(b,X1),true,ifeq(s0(b),true,n1(X0,X1,X0),true),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f88])).
% 2.95/0.81 fof(f455,plain,(
% 2.95/0.81 ![X0,X1,X2]: (ifeq(n1(X0,X1,X0),true,ifeq(l0(X2),true,ifeq(l1(X2,X0),true,n1(X0,X1,X1),true),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f92])).
% 2.95/0.81 fof(f485,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(p0(X0,X1),true,p1(X1,X1,X1),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f122])).
% 2.95/0.81 fof(f507,plain,(
% 2.95/0.81 ![X0]: (ifeq(m0(e,d,X0),true,ifeq(m0(X0,d,X0),true,q1(e,X0,X0),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f144])).
% 2.95/0.81 fof(f525,plain,(
% 2.95/0.81 ![X0]: (ifeq(p0(X0,X0),true,s1(X0),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f162])).
% 2.95/0.81 fof(f526,plain,(
% 2.95/0.81 ![X0,X1,X2]: (ifeq(s1(X0),true,ifeq(q0(X1,X2),true,s1(X1),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f163])).
% 2.95/0.81 fof(f529,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(q1(X0,X1,X1),true,k2(X1,X1),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f166])).
% 2.95/0.81 fof(f532,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(s1(X0),true,ifeq(p0(X1,X1),true,ifeq(m0(X2,X0,X3),true,l2(X3,X3),true),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f169])).
% 2.95/0.81 fof(f576,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(p1(X0,X0,X0),true,ifeq(k0(X1),true,q2(X0,X1,X1),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f213])).
% 2.95/0.81 fof(f580,plain,(
% 2.95/0.81 ![X0]: (ifeq(p1(X0,X0,X0),true,q2(X0,X0,X0),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f217])).
% 2.95/0.81 fof(f581,plain,(
% 2.95/0.81 ![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)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f218])).
% 2.95/0.81 fof(f588,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(b,X0,b),true,ifeq(s1(b),true,s2(X0),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f225])).
% 2.95/0.81 fof(f638,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(q2(X0,d,X1),true,ifeq(k2(X2,X3),true,p3(X1,X2,X3),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f275])).
% 2.95/0.81 fof(f670,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(s2(X0),true,ifeq(q2(X1,X0,X1),true,ifeq(m0(X1,X2,X3),true,s3(X0,X3),true),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f307])).
% 2.95/0.81 fof(f675,plain,(
% 2.95/0.81 ![X0,X1,X2]: (ifeq(s3(a,X0),true,ifeq(l2(X1,X2),true,m4(X0,X2),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f312])).
% 2.95/0.81 fof(f694,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(p3(X0,X1,X2),true,ifeq(l1(X3,X1),true,s4(X3),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f331])).
% 2.95/0.81 fof(f700,plain,(
% 2.95/0.81 ![X0]: (ifeq(s4(X0),true,ifeq(m4(e,e),true,m5(X0,X0),true),true)=true)),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f337])).
% 2.95/0.81 fof(f726,plain,(
% 2.95/0.81 ~m5(d,d)=true),
% 2.95/0.81 inference(cnf_transformation,[status(thm)],[f363])).
% 2.95/0.81 fof(f727,definition,(
% 2.95/0.81 sF0_fnc=m5(d,d)),
% 2.95/0.81 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 2.95/0.81 fof(f728,plain,(
% 2.95/0.81 ~sF0_fnc=true),
% 2.95/0.81 inference(definition_folding,[],[f726,f727])).
% 2.95/0.81 fof(f766,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l0(X0),true,ifeq(true,true,ifeq(s0(b),true,n1(X0,X1,X0),true),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f378,f451])).
% 2.95/0.81 fof(f767,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l0(X0),true,ifeq(s0(b),true,n1(X0,X1,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f766])).
% 2.95/0.81 fof(f768,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l0(X0),true,ifeq(true,true,n1(X0,X1,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f369,f767])).
% 2.95/0.81 fof(f769,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l0(X0),true,n1(X0,X1,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f768])).
% 2.95/0.81 fof(f807,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,ifeq(m0(X0,d,X0),true,q1(e,X0,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f383,f507])).
% 2.95/0.81 fof(f808,plain,(
% 2.95/0.81 ![X0]: (ifeq(m0(X0,d,X0),true,q1(e,X0,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f807])).
% 2.95/0.81 fof(f809,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,q1(e,X0,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f383,f808])).
% 2.95/0.81 fof(f810,plain,(
% 2.95/0.81 ![X0]: (q1(e,X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f809])).
% 2.95/0.81 fof(f894,plain,(
% 2.95/0.81 ifeq(true,true,l1(a,a),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f401,f404])).
% 2.95/0.81 fof(f895,plain,(
% 2.95/0.81 ifeq(true,true,l1(d,d),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f398,f404])).
% 2.95/0.81 fof(f902,plain,(
% 2.95/0.81 l1(a,a)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f894])).
% 2.95/0.81 fof(f903,plain,(
% 2.95/0.81 l1(d,d)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f895])).
% 2.95/0.81 fof(f1077,plain,(
% 2.95/0.81 ifeq(true,true,s1(b),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f378,f525])).
% 2.95/0.81 fof(f1078,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(b,X0,b),true,ifeq(true,true,s2(X0),true),true)=true)),
% 2.95/0.81 inference(backward_demodulation,[status(thm)],[f1079,f588])).
% 2.95/0.81 fof(f1079,plain,(
% 2.95/0.81 s1(b)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f1077])).
% 2.95/0.81 fof(f1080,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(b,X0,b),true,s2(X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f1078])).
% 2.95/0.81 fof(f1272,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,n1(a,X0,a),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f384,f769])).
% 2.95/0.81 fof(f1277,plain,(
% 2.95/0.81 ![X0]: (n1(a,X0,a)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f1272])).
% 2.95/0.81 fof(f2102,plain,(
% 2.95/0.81 ![X0]: (ifeq(n1(a,X0,a),true,ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f902,f455])).
% 2.95/0.81 fof(f2134,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f1277,f2102])).
% 2.95/0.81 fof(f2135,plain,(
% 2.95/0.81 ![X0]: (ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f2134])).
% 2.95/0.81 fof(f2136,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,ifeq(true,true,n1(a,X0,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f384,f2135])).
% 2.95/0.81 fof(f2137,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,n1(a,X0,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f2136])).
% 2.95/0.81 fof(f2141,plain,(
% 2.95/0.81 ![X0]: (n1(a,X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f2137])).
% 2.95/0.81 fof(f2984,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,p1(X0,X0,X0),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f378,f485])).
% 2.95/0.81 fof(f3011,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,q2(X0,X0,X0),true)=true)),
% 2.95/0.81 inference(backward_demodulation,[status(thm)],[f3018,f580])).
% 2.95/0.81 fof(f3012,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(true,true,ifeq(k0(X0),true,q2(X1,X0,X0),true),true)=true)),
% 2.95/0.81 inference(backward_demodulation,[status(thm)],[f3018,f576])).
% 2.95/0.81 fof(f3018,plain,(
% 2.95/0.81 ![X0]: (p1(X0,X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f2984])).
% 2.95/0.81 fof(f3040,plain,(
% 2.95/0.81 ![X0]: (q2(X0,X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f3011])).
% 2.95/0.81 fof(f3041,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(k0(X0),true,q2(X1,X0,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f3012])).
% 2.95/0.81 fof(f3757,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,q2(X0,b,b),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f396,f3041])).
% 2.95/0.81 fof(f3760,plain,(
% 2.95/0.81 ![X0]: (q2(X0,b,b)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f3757])).
% 2.95/0.81 fof(f3788,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,k2(X0,X0),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f810,f529])).
% 2.95/0.81 fof(f3803,plain,(
% 2.95/0.81 ![X0]: (k2(X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f3788])).
% 2.95/0.81 fof(f4491,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(s1(X0),true,ifeq(true,true,s1(X1),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f381,f526])).
% 2.95/0.81 fof(f4504,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(s1(X0),true,s1(X1),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f4491])).
% 2.95/0.81 fof(f4512,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,s1(X0),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f1079,f4504])).
% 2.95/0.81 fof(f4528,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(true,true,ifeq(p0(X0,X0),true,ifeq(m0(X1,X2,X3),true,l2(X3,X3),true),true),true)=true)),
% 2.95/0.81 inference(backward_demodulation,[status(thm)],[f4530,f532])).
% 2.95/0.81 fof(f4530,plain,(
% 2.95/0.81 ![X0]: (s1(X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f4512])).
% 2.95/0.81 fof(f4543,plain,(
% 2.95/0.81 ![X0,X1,X2,X3]: (ifeq(p0(X0,X0),true,ifeq(m0(X1,X2,X3),true,l2(X3,X3),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f4528])).
% 2.95/0.81 fof(f5313,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(a,X0,X0),true,ifeq(p1(X0,X0,X0),true,ifeq(true,true,q2(X0,a,X0),true),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f2141,f581])).
% 2.95/0.81 fof(f5361,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(a,X0,X0),true,ifeq(true,true,ifeq(true,true,q2(X0,a,X0),true),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f3018,f5313])).
% 2.95/0.81 fof(f5362,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(a,X0,X0),true,ifeq(true,true,q2(X0,a,X0),true),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f5361])).
% 2.95/0.81 fof(f5363,plain,(
% 2.95/0.81 ![X0]: (ifeq(q2(a,X0,X0),true,q2(X0,a,X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f5362])).
% 2.95/0.81 fof(f5906,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(true,true,ifeq(k2(X0,X1),true,p3(d,X0,X1),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f3040,f638])).
% 2.95/0.81 fof(f5910,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(k2(X0,X1),true,p3(d,X0,X1),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f5906])).
% 2.95/0.81 fof(f6727,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,p3(d,X0,X0),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f3803,f5910])).
% 2.95/0.81 fof(f6731,plain,(
% 2.95/0.81 ![X0]: (p3(d,X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f6727])).
% 2.95/0.81 fof(f7470,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(true,true,ifeq(l1(X0,X1),true,s4(X0),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f6731,f694])).
% 2.95/0.81 fof(f7490,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(l1(X0,X1),true,s4(X0),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f7470])).
% 2.95/0.81 fof(f7509,plain,(
% 2.95/0.81 ifeq(true,true,s4(d),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f903,f7490])).
% 2.95/0.81 fof(f7522,plain,(
% 2.95/0.81 s4(d)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f7509])).
% 2.95/0.81 fof(f7632,plain,(
% 2.95/0.81 ifeq(true,true,ifeq(m4(e,e),true,m5(d,d),true),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f7522,f700])).
% 2.95/0.81 fof(f7641,plain,(
% 2.95/0.81 ifeq(m4(e,e),true,m5(d,d),true)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f7632])).
% 2.95/0.81 fof(f7642,plain,(
% 2.95/0.81 ifeq(m4(e,e),true,sF0_fnc,true)=true),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f727,f7641])).
% 2.95/0.81 fof(f8968,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(p0(X0,X0),true,ifeq(true,true,l2(X1,X1),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f383,f4543])).
% 2.95/0.81 fof(f8983,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(p0(X0,X0),true,l2(X1,X1),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f8968])).
% 2.95/0.81 fof(f9003,plain,(
% 2.95/0.81 ![X0]: (ifeq(true,true,l2(X0,X0),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f378,f8983])).
% 2.95/0.81 fof(f9035,plain,(
% 2.95/0.81 ![X0]: (l2(X0,X0)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f9003])).
% 2.95/0.81 fof(f9069,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(s3(a,X0),true,ifeq(true,true,m4(X0,X1),true),true)=true)),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f9035,f675])).
% 2.95/0.81 fof(f9076,plain,(
% 2.95/0.81 ![X0,X1]: (ifeq(s3(a,X0),true,m4(X0,X1),true)=true)),
% 2.95/0.81 inference(forward_demodulation,[status(thm)],[f364,f9069])).
% 2.95/0.81 fof(f11170,plain,(
% 2.95/0.81 ifeq(true,true,q2(b,a,b),true)=true),
% 2.95/0.81 inference(paramodulation,[status(thm)],[f3760,f5363])).
% 2.95/0.81 fof(f11174,plain,(
% 2.95/0.83 q2(b,a,b)=true),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11170])).
% 2.95/0.83 fof(f11199,plain,(
% 2.95/0.83 ifeq(true,true,s2(a),true)=true),
% 2.95/0.83 inference(paramodulation,[status(thm)],[f11174,f1080])).
% 2.95/0.83 fof(f11203,plain,(
% 2.95/0.83 ![X0,X1]: (ifeq(s2(a),true,ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true),true)=true)),
% 2.95/0.83 inference(paramodulation,[status(thm)],[f11174,f670])).
% 2.95/0.83 fof(f11210,plain,(
% 2.95/0.83 s2(a)=true),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11199])).
% 2.95/0.83 fof(f11212,plain,(
% 2.95/0.83 ![X0,X1]: (ifeq(true,true,ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true),true)=true)),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f11210,f11203])).
% 2.95/0.83 fof(f11213,plain,(
% 2.95/0.83 ![X0,X1]: (ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true)=true)),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11212])).
% 2.95/0.83 fof(f11214,plain,(
% 2.95/0.83 ![X0,X1]: (ifeq(m0(b,X0,X1),true,s3(a,X1),true)=true)),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11213])).
% 2.95/0.83 fof(f11362,plain,(
% 2.95/0.83 ![X0]: (ifeq(true,true,s3(a,X0),true)=true)),
% 2.95/0.83 inference(paramodulation,[status(thm)],[f383,f11214])).
% 2.95/0.83 fof(f11367,plain,(
% 2.95/0.83 ![X0,X1]: (ifeq(true,true,m4(X0,X1),true)=true)),
% 2.95/0.83 inference(backward_demodulation,[status(thm)],[f11373,f9076])).
% 2.95/0.83 fof(f11373,plain,(
% 2.95/0.83 ![X0]: (s3(a,X0)=true)),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11362])).
% 2.95/0.83 fof(f11380,plain,(
% 2.95/0.83 ifeq(true,true,sF0_fnc,true)=true),
% 2.95/0.83 inference(backward_demodulation,[status(thm)],[f11394,f7642])).
% 2.95/0.83 fof(f11394,plain,(
% 2.95/0.83 ![X0,X1]: (m4(X0,X1)=true)),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11367])).
% 2.95/0.83 fof(f11402,plain,(
% 2.95/0.83 sF0_fnc=true),
% 2.95/0.83 inference(forward_demodulation,[status(thm)],[f364,f11380])).
% 2.95/0.83 fof(f11403,plain,(
% 2.95/0.83 $false),
% 2.95/0.83 inference(forward_subsumption_resolution,[status(thm)],[f11402,f728])).
% 2.95/0.83 % SZS output end CNFRefutation for theBenchmark.p
% 2.95/0.83 % Elapsed time: 0.461731 seconds
% 2.95/0.83 % CPU time: 3.375049 seconds
% 2.95/0.83 % Total memory used: 103.860 MB
% 2.95/0.83 % Net memory used: 100.731 MB
%------------------------------------------------------------------------------