%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : LCL416-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% 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 : Mon Sep 7 01:14:35 PM UTC 2026
% Result : Unsatisfiable 246.94s 246.59s
% Output : CNFRefutation 246.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 4
% Syntax : Number of clauses : 52 ( 52 unt; 0 nHn; 3 RR)
% Number of literals : 52 ( 51 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-4 aty)
% Number of variables : 257 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
is_a_theorem(equivalent(a,a)) != true,
file('theBenchmark.p',prove_reflexivity) ).
cnf(c1,axiom,
ifeq(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c2,axiom,
is_a_theorem(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z))) = true,
file('theBenchmark.p',xcb) ).
cnf(c3,axiom,
ifeq(is_a_theorem(equivalent(X,Y)),true,ifeq(is_a_theorem(X),true,is_a_theorem(Y),true),true) = true,
file('theBenchmark.p',condensed_detachment) ).
cnf(c4,plain,
ifeq(is_a_theorem(X),true,is_a_theorem(equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),true) = true,
inference(equational,[status(thm)],[c1,c2,c3]) ).
cnf(c5,plain,
ifeq(is_a_theorem(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W)),true,is_a_theorem(W),true) = true,
inference(equational,[status(thm)],[c1,c2,c3]) ).
cnf(c6,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(V,W)),V)) = true,
inference(equational,[status(thm)],[c1,c2,c5]) ).
cnf(c8,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),V),equivalent(W,V))) = true,
inference(equational,[status(thm)],[c1,c5,c6]) ).
cnf(c10,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(V,W))),true,is_a_theorem(V),true) = true,
inference(equational,[status(thm)],[c1,c3,c6]) ).
cnf(c12,plain,
is_a_theorem(equivalent(X,equivalent(equivalent(equivalent(equivalent(equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W)),X),V),equivalent(U,V)),U))) = true,
inference(equational,[status(thm)],[c1,c5,c8]) ).
cnf(c18,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(V,W)),V),U),equivalent(U2,U)),U2)) = true,
inference(equational,[status(thm)],[c1,c4,c6]) ).
cnf(c20,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(V,W)),V),U),U2),equivalent(U,U2))) = true,
inference(equational,[status(thm)],[c1,c5,c18]) ).
cnf(c23,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),V),equivalent(W,V)),U),equivalent(U2,U)),U2)) = true,
inference(equational,[status(thm)],[c1,c4,c8]) ).
cnf(c39,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(V,W)),V),U),U2)),true,is_a_theorem(equivalent(U,U2)),true) = true,
inference(equational,[status(thm)],[c1,c3,c20]) ).
cnf(c40,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),V),equivalent(W,V)),U),equivalent(U2,U))),true,is_a_theorem(U2),true) = true,
inference(equational,[status(thm)],[c1,c3,c23]) ).
cnf(c41,plain,
ifeq(is_a_theorem(equivalent(equivalent(X,equivalent(equivalent(equivalent(equivalent(equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W)),X),V),equivalent(U,V)),U)),U2)),true,is_a_theorem(U2),true) = true,
inference(equational,[status(thm)],[c1,c3,c12]) ).
cnf(c56,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),equivalent(W,equivalent(equivalent(equivalent(W,V),equivalent(U,V)),U))),U2),equivalent(U3,U2)),U3)) = true,
inference(equational,[status(thm)],[c1,c5,c12]) ).
cnf(c57,plain,
is_a_theorem(equivalent(equivalent(X,equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W))),X)) = true,
inference(equational,[status(thm)],[c1,c39,c56]) ).
cnf(c61,plain,
is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),W),equivalent(equivalent(equivalent(W,V),equivalent(U,V)),U))) = true,
inference(equational,[status(thm)],[c1,c40,c57]) ).
cnf(c62,plain,
is_a_theorem(equivalent(equivalent(X,Y),equivalent(X,Y))) = true,
inference(equational,[status(thm)],[c1,c10,c61]) ).
cnf(c64,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z)),true,is_a_theorem(Z),true) = true,
inference(equational,[status(thm)],[c1,c3,c62]) ).
cnf(c66,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),equivalent(W,Z)),W)) = true,
inference(equational,[status(thm)],[c1,c4,c62]) ).
cnf(c67,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),W),equivalent(Z,W))) = true,
inference(equational,[status(thm)],[c1,c5,c66]) ).
cnf(c68,plain,
is_a_theorem(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),X))) = true,
inference(equational,[status(thm)],[c1,c64,c67]) ).
cnf(c84,plain,
is_a_theorem(equivalent(X,equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),X),W),equivalent(V,W)),V))) = true,
inference(equational,[status(thm)],[c1,c5,c67]) ).
cnf(c90,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),X)),W),equivalent(V,W)),V)) = true,
inference(equational,[status(thm)],[c1,c4,c68]) ).
cnf(c93,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),X)),W),V),equivalent(W,V))) = true,
inference(equational,[status(thm)],[c1,c5,c90]) ).
cnf(c100,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W))),X),V),equivalent(U,V)),U)) = true,
inference(equational,[status(thm)],[c1,c4,c57]) ).
cnf(c111,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W))),X),V),U),equivalent(V,U))) = true,
inference(equational,[status(thm)],[c1,c5,c100]) ).
cnf(c117,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),equivalent(W,Z)),W),V)),true,is_a_theorem(V),true) = true,
inference(equational,[status(thm)],[c1,c3,c66]) ).
cnf(c124,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),W),equivalent(Z,W)),V)),true,is_a_theorem(V),true) = true,
inference(equational,[status(thm)],[c1,c3,c67]) ).
cnf(c127,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),equivalent(W,Z)),W),V),equivalent(U,V)),U)) = true,
inference(equational,[status(thm)],[c1,c4,c66]) ).
cnf(c139,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),W),equivalent(Z,W)),V),equivalent(U,V)),U)) = true,
inference(equational,[status(thm)],[c1,c61,c117]) ).
cnf(c166,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),equivalent(equivalent(Z,W),equivalent(Z,W))),V),equivalent(U,V)),U)) = true,
inference(equational,[status(thm)],[c1,c64,c84]) ).
cnf(c169,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),X)),W),V)),true,is_a_theorem(equivalent(W,V)),true) = true,
inference(equational,[status(thm)],[c1,c3,c93]) ).
cnf(c178,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),equivalent(equivalent(Z,W),equivalent(Z,W))),V),U),equivalent(V,U))) = true,
inference(equational,[status(thm)],[c1,c5,c166]) ).
cnf(c221,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(Y,equivalent(equivalent(equivalent(Y,Z),equivalent(W,Z)),W))),X),V),U)),true,is_a_theorem(equivalent(V,U)),true) = true,
inference(equational,[status(thm)],[c1,c3,c111]) ).
cnf(c222,plain,
is_a_theorem(equivalent(equivalent(X,equivalent(equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),W),equivalent(equivalent(equivalent(W,V),equivalent(U,V)),U))),X)) = true,
inference(equational,[status(thm)],[c1,c139,c221]) ).
cnf(c299,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),equivalent(W,Z)),W),V),equivalent(U,V))),true,is_a_theorem(U),true) = true,
inference(equational,[status(thm)],[c1,c3,c127]) ).
cnf(c309,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),equivalent(equivalent(equivalent(W,V),equivalent(W,V)),U)),U2),equivalent(U,U2))) = true,
inference(equational,[status(thm)],[c1,c41,c66]) ).
cnf(c373,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),equivalent(equivalent(Z,W),equivalent(Z,W))),V),equivalent(U,V))),true,is_a_theorem(U),true) = true,
inference(equational,[status(thm)],[c1,c3,c166]) ).
cnf(c441,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),equivalent(equivalent(Z,W),equivalent(Z,W))),V),U)),true,is_a_theorem(equivalent(V,U)),true) = true,
inference(equational,[status(thm)],[c1,c3,c178]) ).
cnf(c478,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),equivalent(equivalent(equivalent(Z,W),equivalent(Z,W)),V)),equivalent(equivalent(equivalent(V,U),equivalent(U2,U)),U2))) = true,
inference(equational,[status(thm)],[c1,c124,c222]) ).
cnf(c479,plain,
is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(equivalent(Z,W),equivalent(Z,W)),X),Y))) = true,
inference(equational,[status(thm)],[c1,c373,c478]) ).
cnf(c482,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(equivalent(Z,W),equivalent(Z,W)),X),Y)),V),equivalent(U,V)),U)) = true,
inference(equational,[status(thm)],[c1,c4,c479]) ).
cnf(c986,plain,
is_a_theorem(equivalent(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(Y,Z)),equivalent(equivalent(W,V),equivalent(equivalent(equivalent(equivalent(U,U2),equivalent(U,U2)),W),V)))),X)) = true,
inference(equational,[status(thm)],[c1,c169,c482]) ).
cnf(c995,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(equivalent(equivalent(X,Y),equivalent(Z,Y)),Z)),equivalent(equivalent(equivalent(W,V),equivalent(W,V)),U)),U2)),true,is_a_theorem(equivalent(U,U2)),true) = true,
inference(equational,[status(thm)],[c1,c3,c309]) ).
cnf(c1060,plain,
is_a_theorem(equivalent(equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(equivalent(Z,W),equivalent(Z,W)),X),Y)),equivalent(V,equivalent(equivalent(equivalent(V,U),equivalent(U2,U)),U2)))) = true,
inference(equational,[status(thm)],[c1,c986,c995]) ).
cnf(c1061,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Y)),Z),Z)) = true,
inference(equational,[status(thm)],[c1,c299,c1060]) ).
cnf(c1062,plain,
is_a_theorem(equivalent(X,X)) = true,
inference(equational,[status(thm)],[c1,c441,c1061]) ).
cnf(g1,plain,
is_a_theorem(equivalent(a,a)) = true,
inference(equational,[status(thm)],[c1062]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL416-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.02 % Command : run_Leo-III %s %d THM
% 0.08/0.34 % Computer : n006.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 14:23:46 UTC 2026
% 0.08/0.35 % CPUTime :
% 246.94/246.59 % SZS status Unsatisfiable
% 246.94/246.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------