%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:15:19 PM UTC 2026
% Result : Unsatisfiable 1.45s 0.67s
% Output : CNFRefutation 1.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 29
% Syntax : Number of formulae : 132 ( 132 unt; 1 def)
% Number of atoms : 132 ( 131 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 7 con; 0-4 aty)
% Number of variables : 188 ( 188 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
s0(b) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] : p0(b,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X] : q0(X,d) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,Y] : m0(X,d,Y) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
l0(a) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
k0(b) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
n0(c,d) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
n0(b,a) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [H,G] : ifeq(n0(H,G),true,l1(G,G),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [D,E] : ifeq(l0(D),true,ifeq(p0(b,E),true,ifeq(s0(b),true,n1(D,E,D),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [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,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [C,B] : ifeq(p0(C,B),true,p1(B,B,B),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
! [C,D,B] : ifeq(m0(C,D,B),true,q1(B,B,B),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [I] : ifeq(p0(I,I),true,s1(I),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,axiom,
! [H,F,G] : ifeq(s1(H),true,ifeq(q0(F,G),true,s1(F),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,axiom,
! [A,J] : ifeq(q1(A,J,J),true,k2(J,J),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [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,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,axiom,
! [E,F] : ifeq(p1(E,E,E),true,ifeq(k0(F),true,q2(E,F,F),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,axiom,
! [I] : ifeq(p1(I,I,I),true,q2(I,I,I),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,axiom,
! [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,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,axiom,
! [H] : ifeq(q2(b,H,b),true,ifeq(s1(b),true,s2(H),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,axiom,
! [F,C,D,E] : ifeq(q2(F,d,C),true,ifeq(k2(D,E),true,p3(C,D,E),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,axiom,
! [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,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,axiom,
! [E,G,F] : ifeq(s3(a,E),true,ifeq(l2(G,F),true,m4(E,F),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,axiom,
! [B,C,D,A] : ifeq(p3(B,C,D),true,ifeq(l1(A,C),true,s4(A),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f337,axiom,
! [B] : ifeq(s4(B),true,ifeq(m4(e,e),true,m5(B,B),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f363,negated_conjecture,
m5(d,d) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f364,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f369,plain,
s0(b) = true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f378,plain,
! [X0] : p0(b,X0) = true,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f381,plain,
! [X0] : q0(X0,d) = true,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f383,plain,
! [X0,X1] : m0(X0,d,X1) = true,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f384,plain,
l0(a) = true,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f396,plain,
k0(b) = true,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f398,plain,
n0(c,d) = true,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f401,plain,
n0(b,a) = true,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f404,plain,
! [X0,X1] : ifeq(n0(X0,X1),true,l1(X1,X1),true) = true,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f451,plain,
! [X0,X1] : ifeq(l0(X0),true,ifeq(p0(b,X1),true,ifeq(s0(b),true,n1(X0,X1,X0),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f455,plain,
! [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,
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f485,plain,
! [X0,X1] : ifeq(p0(X0,X1),true,p1(X1,X1,X1),true) = true,
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f510,plain,
! [X0,X1,X2] : ifeq(m0(X0,X1,X2),true,q1(X2,X2,X2),true) = true,
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f525,plain,
! [X0] : ifeq(p0(X0,X0),true,s1(X0),true) = true,
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f526,plain,
! [X0,X1,X2] : ifeq(s1(X0),true,ifeq(q0(X1,X2),true,s1(X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f529,plain,
! [X0,X1] : ifeq(q1(X0,X1,X1),true,k2(X1,X1),true) = true,
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f532,plain,
! [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,
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f576,plain,
! [X0,X1] : ifeq(p1(X0,X0,X0),true,ifeq(k0(X1),true,q2(X0,X1,X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f580,plain,
! [X0] : ifeq(p1(X0,X0,X0),true,q2(X0,X0,X0),true) = true,
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f581,plain,
! [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,
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f588,plain,
! [X0] : ifeq(q2(b,X0,b),true,ifeq(s1(b),true,s2(X0),true),true) = true,
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f638,plain,
! [X0,X1,X2,X3] : ifeq(q2(X0,d,X1),true,ifeq(k2(X2,X3),true,p3(X1,X2,X3),true),true) = true,
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f670,plain,
! [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,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f675,plain,
! [X0,X1,X2] : ifeq(s3(a,X0),true,ifeq(l2(X1,X2),true,m4(X0,X2),true),true) = true,
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f694,plain,
! [X0,X1,X2,X3] : ifeq(p3(X0,X1,X2),true,ifeq(l1(X3,X1),true,s4(X3),true),true) = true,
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f700,plain,
! [X0] : ifeq(s4(X0),true,ifeq(m4(e,e),true,m5(X0,X0),true),true) = true,
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f726,plain,
m5(d,d) != true,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f727,definition,
sF0_fnc = m5(d,d),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f728,plain,
sF0_fnc != true,
inference(definition_folding,[],[f726,f727]) ).
fof(f732,plain,
ifeq(s4(d),true,ifeq(m4(e,e),true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f727,f700]) ).
fof(f766,plain,
ifeq(true,true,s1(b),true) = true,
inference(paramodulation,[status(thm)],[f378,f525]) ).
fof(f767,plain,
s1(b) = true,
inference(forward_demodulation,[status(thm)],[f364,f766]) ).
fof(f770,plain,
ifeq(true,true,l1(a,a),true) = true,
inference(paramodulation,[status(thm)],[f401,f404]) ).
fof(f771,plain,
ifeq(true,true,l1(d,d),true) = true,
inference(paramodulation,[status(thm)],[f398,f404]) ).
fof(f778,plain,
l1(a,a) = true,
inference(forward_demodulation,[status(thm)],[f364,f770]) ).
fof(f779,plain,
l1(d,d) = true,
inference(forward_demodulation,[status(thm)],[f364,f771]) ).
fof(f1576,plain,
! [X0] : ifeq(true,true,p1(X0,X0,X0),true) = true,
inference(paramodulation,[status(thm)],[f378,f485]) ).
fof(f1584,plain,
! [X0] : p1(X0,X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f1576]) ).
fof(f2200,plain,
! [X0,X1] : ifeq(l0(X0),true,ifeq(true,true,ifeq(s0(b),true,n1(X0,X1,X0),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f378,f451]) ).
fof(f2201,plain,
! [X0,X1] : ifeq(l0(X0),true,ifeq(s0(b),true,n1(X0,X1,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f2200]) ).
fof(f2202,plain,
! [X0,X1] : ifeq(l0(X0),true,ifeq(true,true,n1(X0,X1,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f369,f2201]) ).
fof(f2203,plain,
! [X0,X1] : ifeq(l0(X0),true,n1(X0,X1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f2202]) ).
fof(f2205,plain,
! [X0] : ifeq(true,true,n1(a,X0,a),true) = true,
inference(paramodulation,[status(thm)],[f384,f2203]) ).
fof(f2215,plain,
! [X0] : n1(a,X0,a) = true,
inference(forward_demodulation,[status(thm)],[f364,f2205]) ).
fof(f2555,plain,
! [X0] : ifeq(n1(a,X0,a),true,ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true),true) = true,
inference(paramodulation,[status(thm)],[f778,f455]) ).
fof(f2588,plain,
! [X0] : ifeq(true,true,ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f2215,f2555]) ).
fof(f2589,plain,
! [X0] : ifeq(l0(a),true,ifeq(true,true,n1(a,X0,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f2588]) ).
fof(f2590,plain,
! [X0] : ifeq(true,true,ifeq(true,true,n1(a,X0,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f384,f2589]) ).
fof(f2591,plain,
! [X0] : ifeq(true,true,n1(a,X0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f2590]) ).
fof(f2592,plain,
! [X0] : n1(a,X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f2591]) ).
fof(f2868,plain,
! [X0] : ifeq(true,true,q1(X0,X0,X0),true) = true,
inference(paramodulation,[status(thm)],[f383,f510]) ).
fof(f2881,plain,
! [X0] : q1(X0,X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f2868]) ).
fof(f2897,plain,
! [X0] : ifeq(true,true,k2(X0,X0),true) = true,
inference(paramodulation,[status(thm)],[f2881,f529]) ).
fof(f2899,plain,
! [X0] : k2(X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f2897]) ).
fof(f3305,plain,
! [X0] : ifeq(true,true,q2(X0,X0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f1584,f580]) ).
fof(f3311,plain,
! [X0] : q2(X0,X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f3305]) ).
fof(f5324,plain,
! [X0,X1] : ifeq(s1(X0),true,ifeq(true,true,s1(X1),true),true) = true,
inference(paramodulation,[status(thm)],[f381,f526]) ).
fof(f5334,plain,
! [X0,X1] : ifeq(s1(X0),true,s1(X1),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f5324]) ).
fof(f5424,plain,
! [X0] : ifeq(true,true,s1(X0),true) = true,
inference(paramodulation,[status(thm)],[f767,f5334]) ).
fof(f5426,plain,
! [X0] : s1(X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f5424]) ).
fof(f5449,plain,
! [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,
inference(forward_demodulation,[status(thm)],[f5426,f532]) ).
fof(f5450,plain,
! [X0,X1,X2,X3] : ifeq(p0(X0,X0),true,ifeq(m0(X1,X2,X3),true,l2(X3,X3),true),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f5449]) ).
fof(f5459,plain,
! [X0,X1] : ifeq(p0(X0,X0),true,ifeq(true,true,l2(X1,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f383,f5450]) ).
fof(f5468,plain,
! [X0,X1] : ifeq(p0(X0,X0),true,l2(X1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f5459]) ).
fof(f5578,plain,
! [X0] : ifeq(true,true,l2(X0,X0),true) = true,
inference(paramodulation,[status(thm)],[f378,f5468]) ).
fof(f5581,plain,
! [X0] : l2(X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f5578]) ).
fof(f6802,plain,
! [X0,X1] : ifeq(true,true,ifeq(k0(X0),true,q2(X1,X0,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f1584,f576]) ).
fof(f6803,plain,
! [X0,X1] : ifeq(k0(X0),true,q2(X1,X0,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f6802]) ).
fof(f6804,plain,
! [X0] : ifeq(true,true,q2(X0,b,b),true) = true,
inference(paramodulation,[status(thm)],[f396,f6803]) ).
fof(f6807,plain,
! [X0] : q2(X0,b,b) = true,
inference(forward_demodulation,[status(thm)],[f364,f6804]) ).
fof(f6867,plain,
! [X0] : ifeq(q2(a,X0,X0),true,ifeq(p1(X0,X0,X0),true,ifeq(true,true,q2(X0,a,X0),true),true),true) = true,
inference(paramodulation,[status(thm)],[f2592,f581]) ).
fof(f6916,plain,
! [X0] : ifeq(q2(a,X0,X0),true,ifeq(true,true,ifeq(true,true,q2(X0,a,X0),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f1584,f6867]) ).
fof(f6917,plain,
! [X0] : ifeq(q2(a,X0,X0),true,ifeq(true,true,q2(X0,a,X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f6916]) ).
fof(f6918,plain,
! [X0] : ifeq(q2(a,X0,X0),true,q2(X0,a,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f6917]) ).
fof(f7002,plain,
ifeq(true,true,q2(b,a,b),true) = true,
inference(paramodulation,[status(thm)],[f6807,f6918]) ).
fof(f7006,plain,
q2(b,a,b) = true,
inference(forward_demodulation,[status(thm)],[f364,f7002]) ).
fof(f7178,plain,
! [X0] : ifeq(q2(b,X0,b),true,ifeq(true,true,s2(X0),true),true) = true,
inference(forward_demodulation,[status(thm)],[f5426,f588]) ).
fof(f7179,plain,
! [X0] : ifeq(q2(b,X0,b),true,s2(X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f7178]) ).
fof(f7180,plain,
ifeq(true,true,s2(a),true) = true,
inference(paramodulation,[status(thm)],[f7006,f7179]) ).
fof(f7186,plain,
s2(a) = true,
inference(forward_demodulation,[status(thm)],[f364,f7180]) ).
fof(f8716,plain,
! [X0,X1] : ifeq(true,true,ifeq(k2(X0,X1),true,p3(d,X0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f3311,f638]) ).
fof(f8721,plain,
! [X0,X1] : ifeq(k2(X0,X1),true,p3(d,X0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f8716]) ).
fof(f8863,plain,
! [X0] : ifeq(true,true,p3(d,X0,X0),true) = true,
inference(paramodulation,[status(thm)],[f2899,f8721]) ).
fof(f8866,plain,
! [X0] : p3(d,X0,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f8863]) ).
fof(f10216,plain,
! [X0,X1] : ifeq(s2(a),true,ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true),true) = true,
inference(paramodulation,[status(thm)],[f7006,f670]) ).
fof(f10249,plain,
! [X0,X1] : ifeq(true,true,ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f7186,f10216]) ).
fof(f10250,plain,
! [X0,X1] : ifeq(true,true,ifeq(m0(b,X0,X1),true,s3(a,X1),true),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f10249]) ).
fof(f10251,plain,
! [X0,X1] : ifeq(m0(b,X0,X1),true,s3(a,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f10250]) ).
fof(f10400,plain,
! [X0,X1] : ifeq(s3(a,X0),true,ifeq(true,true,m4(X0,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f5581,f675]) ).
fof(f10403,plain,
! [X0,X1] : ifeq(s3(a,X0),true,m4(X0,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f10400]) ).
fof(f10969,plain,
! [X0,X1] : ifeq(true,true,ifeq(l1(X0,X1),true,s4(X0),true),true) = true,
inference(paramodulation,[status(thm)],[f8866,f694]) ).
fof(f10985,plain,
! [X0,X1] : ifeq(l1(X0,X1),true,s4(X0),true) = true,
inference(forward_demodulation,[status(thm)],[f364,f10969]) ).
fof(f11013,plain,
ifeq(true,true,s4(d),true) = true,
inference(paramodulation,[status(thm)],[f779,f10985]) ).
fof(f11019,plain,
s4(d) = true,
inference(forward_demodulation,[status(thm)],[f364,f11013]) ).
fof(f11061,plain,
ifeq(true,true,ifeq(m4(e,e),true,sF0_fnc,true),true) = true,
inference(backward_demodulation,[status(thm)],[f11019,f732]) ).
fof(f11068,plain,
ifeq(m4(e,e),true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f364,f11061]) ).
fof(f11299,plain,
! [X0] : ifeq(true,true,s3(a,X0),true) = true,
inference(paramodulation,[status(thm)],[f383,f10251]) ).
fof(f11303,plain,
! [X0] : s3(a,X0) = true,
inference(forward_demodulation,[status(thm)],[f364,f11299]) ).
fof(f11307,plain,
! [X0,X1] : ifeq(true,true,m4(X0,X1),true) = true,
inference(backward_demodulation,[status(thm)],[f11303,f10403]) ).
fof(f11310,plain,
! [X0,X1] : m4(X0,X1) = true,
inference(forward_demodulation,[status(thm)],[f364,f11307]) ).
fof(f11316,plain,
ifeq(true,true,sF0_fnc,true) = true,
inference(backward_demodulation,[status(thm)],[f11310,f11068]) ).
fof(f11321,plain,
sF0_fnc = true,
inference(forward_demodulation,[status(thm)],[f364,f11316]) ).
fof(f11322,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11321,f728]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN143-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.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:44:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 1.45/0.67 % Refutation found
% 1.45/0.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.45/0.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.45/0.70 % Elapsed time: 0.332670 seconds
% 1.45/0.70 % CPU time: 2.374652 seconds
% 1.45/0.70 % Total memory used: 95.622 MB
% 1.45/0.70 % Net memory used: 90.873 MB
%------------------------------------------------------------------------------