%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:26 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.44s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 15
% Syntax : Number of formulae : 55 ( 55 unt; 0 def)
% Number of atoms : 55 ( 54 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 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 : 17 ( 17 usr; 5 con; 0-4 aty)
% Number of variables : 76 ( 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
r0(e) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] : p0(b,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
p0(c,b) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,Y] : m0(X,d,Y) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
m0(e,b,c) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
n0(e,e) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [E,C,F,D] : ifeq(p0(E,C),true,ifeq(r0(F),true,ifeq(m0(D,C,E),true,l1(C,D),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A,J] : ifeq(m0(A,A,J),true,m1(J,J,J),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [G,F] : ifeq(m1(G,G,F),true,p2(F,F,F),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,axiom,
! [H,G] : ifeq(l1(H,G),true,q2(G,G,H),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,axiom,
! [E,F,D] : ifeq(p2(E,F,D),true,n3(D),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [I,G,H] : ifeq(q2(I,G,H),true,ifeq(n0(I,G),true,q3(G,H),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f330,axiom,
! [H,I,G,J] : ifeq(q3(H,I),true,ifeq(n3(G),true,ifeq(p0(J,G),true,r4(G),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f363,negated_conjecture,
r4(b) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f364,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f377,plain,
r0(e) = true,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f378,plain,
! [X0] : p0(b,X0) = true,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f382,plain,
p0(c,b) = true,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f383,plain,
! [X0,X1] : m0(X0,d,X1) = true,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f391,plain,
m0(e,b,c) = true,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f394,plain,
n0(e,e) = true,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f405,plain,
! [X0,X1,X2,X3] : ifeq(p0(X0,X1),true,ifeq(r0(X2),true,ifeq(m0(X3,X1,X0),true,l1(X1,X3),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f408,plain,
! [X0,X1] : ifeq(m0(X0,X0,X1),true,m1(X1,X1,X1),true) = true,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f549,plain,
! [X0,X1] : ifeq(m1(X0,X0,X1),true,p2(X1,X1,X1),true) = true,
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f585,plain,
! [X0,X1] : ifeq(l1(X0,X1),true,q2(X1,X1,X0),true) = true,
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f637,plain,
! [X0,X1,X2] : ifeq(p2(X0,X1,X2),true,n3(X2),true) = true,
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f652,plain,
! [X0,X1,X2] : ifeq(q2(X0,X1,X2),true,ifeq(n0(X0,X1),true,q3(X1,X2),true),true) = true,
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f693,plain,
! [X0,X1,X2,X3] : ifeq(q3(X0,X1),true,ifeq(n3(X2),true,ifeq(p0(X3,X2),true,r4(X2),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f726,plain,
r4(b) != true,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f729,plain,
! [X0,X1,X2] : true = ifeq(q3(X0,X1),true,ifeq(n3(X2),true,ifeq(true,true,r4(X2),true),true),true),
inference(paramodulation,[status(thm)],[f378,f693]) ).
fof(f730,plain,
! [X0,X1,X2] : true = ifeq(q3(X0,X1),true,ifeq(n3(X2),true,r4(X2),true),true),
inference(forward_demodulation,[status(thm)],[f364,f729]) ).
fof(f777,plain,
! [X0] : true = ifeq(p0(c,b),true,ifeq(r0(X0),true,ifeq(true,true,l1(b,e),true),true),true),
inference(paramodulation,[status(thm)],[f391,f405]) ).
fof(f789,plain,
! [X0] : true = ifeq(true,true,ifeq(r0(X0),true,ifeq(true,true,l1(b,e),true),true),true),
inference(forward_demodulation,[status(thm)],[f382,f777]) ).
fof(f790,plain,
! [X0] : true = ifeq(r0(X0),true,ifeq(true,true,l1(b,e),true),true),
inference(forward_demodulation,[status(thm)],[f364,f789]) ).
fof(f791,plain,
! [X0] : true = ifeq(r0(X0),true,l1(b,e),true),
inference(forward_demodulation,[status(thm)],[f364,f790]) ).
fof(f833,plain,
! [X0] : true = ifeq(true,true,m1(X0,X0,X0),true),
inference(paramodulation,[status(thm)],[f383,f408]) ).
fof(f837,plain,
! [X0] : true = m1(X0,X0,X0),
inference(forward_demodulation,[status(thm)],[f364,f833]) ).
fof(f4335,plain,
! [X0] : true = ifeq(true,true,p2(X0,X0,X0),true),
inference(paramodulation,[status(thm)],[f837,f549]) ).
fof(f4344,plain,
! [X0] : true = p2(X0,X0,X0),
inference(forward_demodulation,[status(thm)],[f364,f4335]) ).
fof(f4354,plain,
! [X0] : true = ifeq(true,true,n3(X0),true),
inference(paramodulation,[status(thm)],[f4344,f637]) ).
fof(f4365,plain,
! [X0] : true = n3(X0),
inference(forward_demodulation,[status(thm)],[f364,f4354]) ).
fof(f4367,plain,
! [X0,X1,X2] : true = ifeq(q3(X0,X1),true,ifeq(true,true,r4(X2),true),true),
inference(backward_demodulation,[status(thm)],[f4365,f730]) ).
fof(f4369,plain,
! [X0,X1,X2] : true = ifeq(q3(X0,X1),true,r4(X2),true),
inference(forward_demodulation,[status(thm)],[f364,f4367]) ).
fof(f5327,plain,
true = ifeq(true,true,l1(b,e),true),
inference(paramodulation,[status(thm)],[f377,f791]) ).
fof(f5329,plain,
true = l1(b,e),
inference(forward_demodulation,[status(thm)],[f364,f5327]) ).
fof(f5332,plain,
true = ifeq(true,true,q2(e,e,b),true),
inference(paramodulation,[status(thm)],[f5329,f585]) ).
fof(f5338,plain,
true = q2(e,e,b),
inference(forward_demodulation,[status(thm)],[f364,f5332]) ).
fof(f6364,plain,
true = ifeq(true,true,ifeq(n0(e,e),true,q3(e,b),true),true),
inference(paramodulation,[status(thm)],[f5338,f652]) ).
fof(f6378,plain,
true = ifeq(n0(e,e),true,q3(e,b),true),
inference(forward_demodulation,[status(thm)],[f364,f6364]) ).
fof(f6379,plain,
true = ifeq(true,true,q3(e,b),true),
inference(forward_demodulation,[status(thm)],[f394,f6378]) ).
fof(f6380,plain,
true = q3(e,b),
inference(forward_demodulation,[status(thm)],[f364,f6379]) ).
fof(f6407,plain,
! [X0] : true = ifeq(true,true,r4(X0),true),
inference(paramodulation,[status(thm)],[f6380,f4369]) ).
fof(f6411,plain,
! [X0] : true = r4(X0),
inference(forward_demodulation,[status(thm)],[f364,f6407]) ).
fof(f6412,plain,
$false,
inference(resolution,[status(thm)],[f6411,f726]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN193-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n003.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 10:47:01 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.44 % Refutation found
% 0.12/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.46 % Elapsed time: 0.113879 seconds
% 0.12/0.46 % CPU time: 0.651663 seconds
% 0.12/0.46 % Total memory used: 51.636 MB
% 0.12/0.46 % Net memory used: 51.276 MB
%------------------------------------------------------------------------------