%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT394-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 01:03:05 PM UTC 2026
% Result : Unsatisfiable 61.63s 8.28s
% Output : CNFRefutation 61.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 5
% Syntax : Number of formulae : 85 ( 85 unt; 0 def)
% Number of atoms : 85 ( 84 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 206 ( 206 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : f(f(f(f(A,B),f(B,C)),D),f(B,f(f(B,f(f(A,A),A)),C))) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : or(A,B) = f(f(A,A),f(B,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : and(A,B) = f(f(A,B),f(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : neg(A) = f(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
f(x0,f(x0,x0)) != f(x1,f(x1,x1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f7,plain,
! [X0,X1] : or(X0,X1) = f(f(X0,X0),f(X1,X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f8,plain,
! [X0,X1] : and(X0,X1) = f(f(X0,X1),f(X0,X1)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f9,plain,
! [X0] : neg(X0) = f(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
f(x0,f(x0,x0)) != f(x1,f(x1,x1)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0,X1] : and(X0,X1) = neg(f(X0,X1)),
inference(backward_demodulation,[status(thm)],[f9,f8]) ).
fof(f17,plain,
! [X0,X1] : or(X0,X1) = f(f(X0,X0),neg(X1)),
inference(backward_demodulation,[status(thm)],[f9,f7]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(neg(X0),X0)),X2))) = X1,
inference(backward_demodulation,[status(thm)],[f9,f6]) ).
fof(f19,plain,
f(x0,neg(x0)) != f(x1,f(x1,x1)),
inference(forward_demodulation,[status(thm)],[f9,f10]) ).
fof(f20,plain,
f(x0,neg(x0)) != f(x1,neg(x1)),
inference(forward_demodulation,[status(thm)],[f9,f19]) ).
fof(f21,plain,
! [X0,X1] : or(X0,X1) = f(neg(X0),neg(X1)),
inference(forward_demodulation,[status(thm)],[f9,f17]) ).
fof(f22,plain,
! [X0,X1,X2,X3] : f(X0,f(f(X0,X1),f(f(f(X0,X1),f(neg(f(X2,X0)),f(X2,X0))),X3))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f18,f18]) ).
fof(f23,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(X0,f(f(X0,f(neg(f(f(X2,X0),f(X0,X3))),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))) = X0,
inference(paramodulation,[status(thm)],[f18,f18]) ).
fof(f26,plain,
! [X0,X1,X2,X3,X4] : f(f(f(f(X0,f(f(X1,X2),f(X2,X3))),f(f(f(X1,X2),f(X2,X3)),f(X2,f(f(X2,f(neg(X1),X1)),X3)))),X4),f(f(f(X1,X2),f(X2,X3)),X2)) = f(f(X1,X2),f(X2,X3)),
inference(paramodulation,[status(thm)],[f18,f18]) ).
fof(f27,plain,
! [X0,X1,X2,X3] : f(X0,f(f(X0,X1),f(f(f(X0,X1),f(and(X2,X0),f(X2,X0))),X3))) = f(X0,X1),
inference(forward_demodulation,[status(thm)],[f16,f22]) ).
fof(f28,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))) = X0,
inference(forward_demodulation,[status(thm)],[f16,f23]) ).
fof(f30,plain,
! [X0,X1,X2] : f(f(X0,X1),f(f(f(X0,X1),f(X1,X2)),X1)) = f(f(X0,X1),f(X1,X2)),
inference(paramodulation,[status(thm)],[f18,f26]) ).
fof(f138,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,X2)),X1),f(X1,X1)) = f(f(f(f(X0,X1),f(X1,X2)),X1),f(X1,f(f(X1,f(neg(X0),X0)),X2))),
inference(paramodulation,[status(thm)],[f18,f30]) ).
fof(f168,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,X2)),X1),neg(X1)) = f(f(f(f(X0,X1),f(X1,X2)),X1),f(X1,f(f(X1,f(neg(X0),X0)),X2))),
inference(forward_demodulation,[status(thm)],[f9,f138]) ).
fof(f169,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,X2)),X1),neg(X1)) = X1,
inference(forward_demodulation,[status(thm)],[f18,f168]) ).
fof(f1787,plain,
! [X0,X1] : f(X0,f(f(X0,X1),f(X0,X1))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f28,f27]) ).
fof(f1802,plain,
! [X0,X1,X2] : f(f(X0,X0),f(X0,X0)) = f(f(X0,X0),f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2)))),
inference(paramodulation,[status(thm)],[f28,f30]) ).
fof(f1916,plain,
! [X0,X1] : f(X0,neg(f(X0,X1))) = f(X0,X1),
inference(forward_demodulation,[status(thm)],[f9,f1787]) ).
fof(f1918,plain,
! [X0,X1] : f(X0,and(X0,X1)) = f(X0,X1),
inference(forward_demodulation,[status(thm)],[f16,f1916]) ).
fof(f1953,plain,
! [X0,X1,X2] : neg(f(X0,X0)) = f(f(X0,X0),f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2)))),
inference(forward_demodulation,[status(thm)],[f9,f1802]) ).
fof(f1954,plain,
! [X0,X1,X2] : and(X0,X0) = f(f(X0,X0),f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2)))),
inference(forward_demodulation,[status(thm)],[f16,f1953]) ).
fof(f1979,plain,
! [X0] : and(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f28,f1954]) ).
fof(f2854,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,neg(f(X1,f(neg(X0),X0))))) = X1,
inference(paramodulation,[status(thm)],[f9,f18]) ).
fof(f2867,plain,
! [X0] : f(f(neg(f(X0,X0)),X0),neg(X0)) = X0,
inference(paramodulation,[status(thm)],[f9,f169]) ).
fof(f2914,plain,
! [X0,X1] : f(f(X0,X1),f(f(f(X0,X1),neg(X1)),X1)) = f(f(X0,X1),f(X1,X1)),
inference(paramodulation,[status(thm)],[f9,f30]) ).
fof(f2988,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,and(X1,f(neg(X0),X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f16,f2854]) ).
fof(f2989,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,f(neg(X0),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f1918,f2988]) ).
fof(f3078,plain,
! [X0] : f(f(and(X0,X0),X0),neg(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f16,f2867]) ).
fof(f3079,plain,
! [X0] : f(f(X0,X0),neg(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1979,f3078]) ).
fof(f3080,plain,
! [X0] : f(neg(X0),neg(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f9,f3079]) ).
fof(f3093,plain,
! [X0] : neg(neg(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f9,f3080]) ).
fof(f3252,plain,
! [X0,X1] : f(f(X0,X1),f(f(f(X0,X1),neg(X1)),X1)) = f(f(X0,X1),neg(X1)),
inference(forward_demodulation,[status(thm)],[f9,f2914]) ).
fof(f3354,plain,
! [X0,X1,X2,X3] : and(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))) = neg(X0),
inference(paramodulation,[status(thm)],[f28,f16]) ).
fof(f3357,plain,
! [X0,X1] : neg(and(X0,X1)) = f(X0,X1),
inference(paramodulation,[status(thm)],[f16,f3093]) ).
fof(f5063,plain,
! [X0,X1,X2,X3] : f(X0,f(f(f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))),neg(f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))) = f(f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))),neg(f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))),
inference(paramodulation,[status(thm)],[f28,f3252]) ).
fof(f5254,plain,
! [X0,X1,X2,X3] : f(X0,f(f(X0,neg(f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2))))),f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2))))) = f(f(f(X0,X3),f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2)))),neg(f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2))))),
inference(forward_demodulation,[status(thm)],[f28,f5063]) ).
fof(f5255,plain,
! [X0,X1,X2,X3] : f(X0,X0) = f(f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))),neg(f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))),
inference(forward_demodulation,[status(thm)],[f28,f5254]) ).
fof(f5256,plain,
! [X0,X1,X2,X3] : neg(X0) = f(f(f(X0,X1),f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3)))),neg(f(X0,f(f(X0,f(and(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(neg(X2),X2)),X3))))),
inference(forward_demodulation,[status(thm)],[f9,f5255]) ).
fof(f5257,plain,
! [X0,X1,X2] : neg(X0) = f(X0,neg(f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2))))),
inference(forward_demodulation,[status(thm)],[f28,f5256]) ).
fof(f5258,plain,
! [X0,X1,X2] : neg(X0) = f(X0,and(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2)))),
inference(forward_demodulation,[status(thm)],[f16,f5257]) ).
fof(f5259,plain,
! [X0,X1] : f(f(X0,X1),neg(X0)) = X0,
inference(backward_demodulation,[status(thm)],[f5287,f28]) ).
fof(f5269,plain,
! [X0,X1] : and(f(X0,X1),neg(X0)) = neg(X0),
inference(backward_demodulation,[status(thm)],[f5287,f3354]) ).
fof(f5287,plain,
! [X0,X1,X2] : neg(X0) = f(X0,f(f(X0,f(and(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(neg(X1),X1)),X2))),
inference(forward_demodulation,[status(thm)],[f1918,f5258]) ).
fof(f6794,plain,
! [X0,X1,X2] : or(and(X0,X1),X2) = f(f(X0,X1),neg(X2)),
inference(paramodulation,[status(thm)],[f3357,f21]) ).
fof(f6796,plain,
! [X0,X1] : or(neg(X0),X1) = f(X0,neg(X1)),
inference(paramodulation,[status(thm)],[f3093,f21]) ).
fof(f6799,plain,
! [X0,X1] : or(X0,neg(X1)) = f(neg(X0),X1),
inference(paramodulation,[status(thm)],[f3093,f21]) ).
fof(f6857,plain,
! [X0,X1] : or(and(X0,X1),X0) = X0,
inference(backward_demodulation,[status(thm)],[f6794,f5259]) ).
fof(f6948,plain,
f(x0,neg(x0)) != or(neg(x1),x1),
inference(backward_demodulation,[status(thm)],[f6796,f20]) ).
fof(f6984,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,or(X0,neg(X0))),X2))) = X1,
inference(backward_demodulation,[status(thm)],[f6799,f18]) ).
fof(f7048,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,f(neg(X0),X0)))),X2),f(X1,or(X0,neg(X0)))) = X1,
inference(backward_demodulation,[status(thm)],[f6799,f2989]) ).
fof(f7890,plain,
or(neg(x0),x0) != or(neg(x1),x1),
inference(forward_demodulation,[status(thm)],[f6796,f6948]) ).
fof(f8030,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,or(X0,neg(X0))))),X2),f(X1,or(X0,neg(X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f6799,f7048]) ).
fof(f8423,plain,
! [X0,X1] : and(f(neg(X0),X1),X0) = neg(neg(X0)),
inference(paramodulation,[status(thm)],[f3093,f5269]) ).
fof(f8441,plain,
! [X0,X1] : and(or(X0,neg(X1)),X0) = neg(neg(X0)),
inference(forward_demodulation,[status(thm)],[f6799,f8423]) ).
fof(f8442,plain,
! [X0,X1] : and(or(X0,neg(X1)),X0) = X0,
inference(forward_demodulation,[status(thm)],[f3093,f8441]) ).
fof(f8476,plain,
! [X0,X1] : and(or(X0,X1),X0) = X0,
inference(paramodulation,[status(thm)],[f3093,f8442]) ).
fof(f8721,plain,
! [X0,X1] : or(X0,or(X0,X1)) = or(X0,X1),
inference(paramodulation,[status(thm)],[f8476,f6857]) ).
fof(f8979,plain,
! [X0,X1] : or(neg(X0),neg(X1)) = f(X0,X1),
inference(paramodulation,[status(thm)],[f3093,f6796]) ).
fof(f9330,plain,
! [X0,X1,X2] : or(and(X0,X1),neg(X2)) = f(f(X0,X1),X2),
inference(paramodulation,[status(thm)],[f3357,f6799]) ).
fof(f10417,plain,
! [X0,X1,X2,X3] : or(and(X0,X1),and(X2,X3)) = f(f(X0,X1),f(X2,X3)),
inference(paramodulation,[status(thm)],[f16,f9330]) ).
fof(f10500,plain,
! [X0,X1,X2,X3] : or(and(f(f(X0,X1),f(X1,X2)),X3),and(X1,f(f(X1,or(X0,neg(X0))),X2))) = X1,
inference(backward_demodulation,[status(thm)],[f10417,f6984]) ).
fof(f10626,plain,
! [X0,X1,X2] : or(and(f(f(X0,X1),f(X1,f(X1,or(X0,neg(X0))))),X2),and(X1,or(X0,neg(X0)))) = X1,
inference(backward_demodulation,[status(thm)],[f10417,f8030]) ).
fof(f11031,plain,
! [X0,X1,X2,X3] : or(and(or(and(X0,X1),and(X1,X2)),X3),and(X1,f(f(X1,or(X0,neg(X0))),X2))) = X1,
inference(forward_demodulation,[status(thm)],[f10417,f10500]) ).
fof(f11438,plain,
! [X0,X1,X2] : or(and(or(and(X0,X1),and(X1,f(X1,or(X0,neg(X0))))),X2),and(X1,or(X0,neg(X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f10417,f10626]) ).
fof(f12569,plain,
! [X0,X1,X2,X3] : or(and(or(and(X0,X1),and(X1,X2)),X3),X1) = or(and(or(and(X0,X1),and(X1,X2)),X3),and(X1,f(f(X1,or(X0,neg(X0))),X2))),
inference(paramodulation,[status(thm)],[f11031,f8721]) ).
fof(f12654,plain,
! [X0,X1,X2,X3] : or(and(or(and(X0,X1),and(X1,X2)),X3),X1) = X1,
inference(forward_demodulation,[status(thm)],[f11031,f12569]) ).
fof(f15994,plain,
! [X0,X1] : or(and(X0,X1),X1) = X1,
inference(paramodulation,[status(thm)],[f8476,f12654]) ).
fof(f16421,plain,
! [X0,X1] : and(X0,and(X1,X0)) = and(X1,X0),
inference(paramodulation,[status(thm)],[f15994,f8476]) ).
fof(f20331,plain,
! [X0,X1] : and(X0,or(X1,neg(X1))) = X0,
inference(paramodulation,[status(thm)],[f15994,f11438]) ).
fof(f21182,plain,
! [X0,X1] : and(X0,f(X1,neg(X1))) = X0,
inference(paramodulation,[status(thm)],[f8979,f20331]) ).
fof(f21285,plain,
! [X0,X1] : and(X0,or(neg(X1),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f6796,f21182]) ).
fof(f21841,plain,
! [X0,X1] : and(or(neg(X0),X0),X1) = and(X1,or(neg(X0),X0)),
inference(paramodulation,[status(thm)],[f21285,f16421]) ).
fof(f21885,plain,
! [X0,X1] : and(or(neg(X0),X0),X1) = X1,
inference(forward_demodulation,[status(thm)],[f21285,f21841]) ).
fof(f22102,plain,
! [X0,X1] : or(neg(X0),X0) = or(neg(X1),X1),
inference(paramodulation,[status(thm)],[f21285,f21885]) ).
fof(f22167,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f7890,f22102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT394-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 20 23:58:17 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 61.63/8.28 % Refutation found
% 61.63/8.28 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 61.63/8.28 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 27.99/9.56 % Elapsed time: 8.947445 seconds
% 27.99/9.56 % CPU time: 54.226338 seconds
% 27.99/9.56 % Total memory used: 633.238 MB
% 27.99/9.56 % Net memory used: 608.769 MB
%------------------------------------------------------------------------------