%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL400-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:07:37 PM UTC 2026
% Result : Unsatisfiable 85.78s 11.42s
% Output : CNFRefutation 86.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 6
% Syntax : Number of formulae : 118 ( 118 unt; 0 def)
% Number of atoms : 118 ( 117 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-4 aty)
% Number of variables : 318 ( 318 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : ifeq(is_a_theorem(implies(X,Y)),true,ifeq(is_a_theorem(X),true,is_a_theorem(Y),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : is_a_theorem(implies(implies(not(X),X),X)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
is_a_theorem(implies(not(implies(x,y)),x)) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f8,plain,
! [X0,X1] : ifeq(is_a_theorem(implies(X0,X1)),true,ifeq(is_a_theorem(X0),true,is_a_theorem(X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f9,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f10,plain,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f11,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f12,plain,
is_a_theorem(implies(not(implies(x,y)),x)) != true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f18,plain,
! [X0] : ifeq(true,true,ifeq(is_a_theorem(implies(not(X0),X0)),true,is_a_theorem(X0),true),true) = true,
inference(paramodulation,[status(thm)],[f10,f8]) ).
fof(f19,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(implies(implies(X1,X2),implies(X0,X2))),true),true) = true,
inference(paramodulation,[status(thm)],[f9,f8]) ).
fof(f20,plain,
! [X0,X1] : ifeq(true,true,ifeq(is_a_theorem(X0),true,is_a_theorem(implies(not(X0),X1)),true),true) = true,
inference(paramodulation,[status(thm)],[f11,f8]) ).
fof(f21,plain,
! [X0,X1] : ifeq(is_a_theorem(implies(implies(implies(not(X0),X0),X0),X1)),true,ifeq(true,true,is_a_theorem(X1),true),true) = true,
inference(paramodulation,[status(thm)],[f10,f8]) ).
fof(f23,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,implies(not(X0),X1)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true) = true,
inference(paramodulation,[status(thm)],[f11,f8]) ).
fof(f27,plain,
! [X0] : ifeq(is_a_theorem(implies(not(X0),X0)),true,is_a_theorem(X0),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f18]) ).
fof(f28,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(X0,X1)),true,is_a_theorem(implies(implies(X1,X2),implies(X0,X2))),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f19]) ).
fof(f29,plain,
! [X0,X1] : ifeq(is_a_theorem(X0),true,is_a_theorem(implies(not(X0),X1)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f20]) ).
fof(f30,plain,
! [X0,X1] : ifeq(is_a_theorem(implies(implies(implies(not(X0),X0),X0),X1)),true,is_a_theorem(X1),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f21]) ).
fof(f32,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,implies(not(X0),X1)),X2)),true,is_a_theorem(X2),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f23]) ).
fof(f82,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))),true) = true,
inference(paramodulation,[status(thm)],[f10,f28]) ).
fof(f83,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))),true) = true,
inference(paramodulation,[status(thm)],[f9,f28]) ).
fof(f84,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))),true) = true,
inference(paramodulation,[status(thm)],[f11,f28]) ).
fof(f90,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f82]) ).
fof(f91,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))) = true,
inference(forward_demodulation,[status(thm)],[f7,f83]) ).
fof(f92,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f84]) ).
fof(f100,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(implies(not(X0),X0),X1)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true) = true,
inference(paramodulation,[status(thm)],[f90,f8]) ).
fof(f105,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(implies(not(X0),X0),X1)),X2)),true,is_a_theorem(X2),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f100]) ).
fof(f108,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(is_a_theorem(implies(implies(not(X0),X1),X2)),true,is_a_theorem(implies(X0,X2)),true),true) = true,
inference(paramodulation,[status(thm)],[f92,f8]) ).
fof(f113,plain,
! [X0,X1,X2,X3] : ifeq(is_a_theorem(implies(implies(implies(implies(not(X0),X1),X2),implies(X0,X2)),X3)),true,ifeq(true,true,is_a_theorem(X3),true),true) = true,
inference(paramodulation,[status(thm)],[f92,f8]) ).
fof(f115,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(not(X0),X1),X2)),true,is_a_theorem(implies(X0,X2)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f108]) ).
fof(f118,plain,
! [X0,X1,X2,X3] : ifeq(is_a_theorem(implies(implies(implies(implies(not(X0),X1),X2),implies(X0,X2)),X3)),true,is_a_theorem(X3),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f113]) ).
fof(f169,plain,
! [X0] : ifeq(true,true,is_a_theorem(implies(X0,X0)),true) = true,
inference(paramodulation,[status(thm)],[f92,f30]) ).
fof(f183,plain,
! [X0] : is_a_theorem(implies(X0,X0)) = true,
inference(forward_demodulation,[status(thm)],[f7,f169]) ).
fof(f203,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(not(implies(X0,X0)),X1)),true) = true,
inference(paramodulation,[status(thm)],[f183,f29]) ).
fof(f210,plain,
! [X0,X1] : is_a_theorem(implies(not(implies(X0,X0)),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f203]) ).
fof(f223,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1))),true) = true,
inference(paramodulation,[status(thm)],[f210,f28]) ).
fof(f233,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f223]) ).
fof(f1968,plain,
! [X0,X1,X2,X3] : ifeq(true,true,ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3)),true,is_a_theorem(implies(implies(X2,X0),X3)),true),true) = true,
inference(paramodulation,[status(thm)],[f91,f8]) ).
fof(f1991,plain,
! [X0,X1,X2,X3] : ifeq(is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3)),true,is_a_theorem(implies(implies(X2,X0),X3)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f1968]) ).
fof(f2007,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))),true) = true,
inference(paramodulation,[status(thm)],[f233,f115]) ).
fof(f2072,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2007]) ).
fof(f2160,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(not(implies(X0,X0)),X1),X2),implies(X3,X2))),true) = true,
inference(paramodulation,[status(thm)],[f2072,f28]) ).
fof(f2188,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(not(implies(X0,X0)),X1),X2),implies(X3,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2160]) ).
fof(f2715,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X1))),true) = true,
inference(paramodulation,[status(thm)],[f2188,f30]) ).
fof(f2755,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2715]) ).
fof(f2874,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),true) = true,
inference(paramodulation,[status(thm)],[f2755,f28]) ).
fof(f2902,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2874]) ).
fof(f3052,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(implies(X3,X3),X1),X2))),true) = true,
inference(paramodulation,[status(thm)],[f2902,f28]) ).
fof(f3053,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(is_a_theorem(implies(implies(X0,X0),X1)),true,is_a_theorem(implies(X2,X1)),true),true) = true,
inference(paramodulation,[status(thm)],[f2902,f8]) ).
fof(f3075,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(implies(X3,X3),X1),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f3052]) ).
fof(f3076,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,X0),X1)),true,is_a_theorem(implies(X2,X1)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f3053]) ).
fof(f3900,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X0),X1),X1)),true) = true,
inference(paramodulation,[status(thm)],[f3075,f30]) ).
fof(f3935,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f3900]) ).
fof(f4075,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,X2),X0),X1))),true) = true,
inference(paramodulation,[status(thm)],[f3935,f28]) ).
fof(f4103,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,X2),X0),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f4075]) ).
fof(f4417,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))),true) = true,
inference(paramodulation,[status(thm)],[f2902,f105]) ).
fof(f4509,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f4417]) ).
fof(f4620,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),implies(X2,X1))),true) = true,
inference(paramodulation,[status(thm)],[f4509,f28]) ).
fof(f4657,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),implies(X2,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f4620]) ).
fof(f8187,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(implies(X1,X1),X2),X2))),true) = true,
inference(paramodulation,[status(thm)],[f4103,f3076]) ).
fof(f8322,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(implies(implies(X1,X1),X2),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f8187]) ).
fof(f8707,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(implies(X0,X0),X1),X1),X2),implies(X3,X2))),true) = true,
inference(paramodulation,[status(thm)],[f8322,f28]) ).
fof(f8749,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(implies(implies(X0,X0),X1),X1),X2),implies(X3,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f8707]) ).
fof(f13489,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(X0,implies(implies(X1,X1),X2)),implies(X3,implies(X0,X2)))),true) = true,
inference(paramodulation,[status(thm)],[f8749,f1991]) ).
fof(f13491,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X2,implies(X0,X1)))),true) = true,
inference(paramodulation,[status(thm)],[f4657,f1991]) ).
fof(f13643,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(X0,implies(implies(X1,X1),X2)),implies(X3,implies(X0,X2)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f13489]) ).
fof(f13645,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X2,implies(X0,X1)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f13491]) ).
fof(f14052,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(not(X0),X1),implies(X2,implies(implies(X1,X0),X0)))),true) = true,
inference(paramodulation,[status(thm)],[f13645,f1991]) ).
fof(f14148,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(not(X0),X1),implies(X2,implies(implies(X1,X0),X0)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f14052]) ).
fof(f14981,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X0),X0)))),true) = true,
inference(paramodulation,[status(thm)],[f14148,f115]) ).
fof(f15056,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X0),X0)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f14981]) ).
fof(f15232,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),X2)),X3),implies(X2,X3))),true) = true,
inference(paramodulation,[status(thm)],[f15056,f28]) ).
fof(f15274,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),X2)),X3),implies(X2,X3))) = true,
inference(forward_demodulation,[status(thm)],[f7,f15232]) ).
fof(f15899,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,implies(implies(X1,X3),X3)))),true) = true,
inference(paramodulation,[status(thm)],[f13643,f1991]) ).
fof(f16002,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,implies(implies(X1,X3),X3)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f15899]) ).
fof(f22496,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X1,X0),X0))),true) = true,
inference(paramodulation,[status(thm)],[f15274,f30]) ).
fof(f22599,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,X0),X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f22496]) ).
fof(f22941,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2))),true) = true,
inference(paramodulation,[status(thm)],[f22599,f28]) ).
fof(f22990,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X1,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f22941]) ).
fof(f23973,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X0))),true) = true,
inference(paramodulation,[status(thm)],[f22990,f118]) ).
fof(f24073,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f23973]) ).
fof(f24322,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),true) = true,
inference(paramodulation,[status(thm)],[f24073,f28]) ).
fof(f24354,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,implies(X1,X0)),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true) = true,
inference(paramodulation,[status(thm)],[f24073,f8]) ).
fof(f24373,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f24322]) ).
fof(f24380,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,implies(X1,X0)),X2)),true,is_a_theorem(X2),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f24354]) ).
fof(f25279,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(is_a_theorem(implies(implies(X0,X1),X2)),true,is_a_theorem(implies(X1,X2)),true),true) = true,
inference(paramodulation,[status(thm)],[f24373,f8]) ).
fof(f25324,plain,
! [X0,X1,X2] : ifeq(is_a_theorem(implies(implies(X0,X1),X2)),true,is_a_theorem(implies(X1,X2)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f25279]) ).
fof(f38675,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(implies(implies(not(X1),X1),X1),X2),X2))),true) = true,
inference(paramodulation,[status(thm)],[f16002,f105]) ).
fof(f38799,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(implies(implies(implies(not(X1),X1),X1),X2),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f38675]) ).
fof(f41070,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1)),true) = true,
inference(paramodulation,[status(thm)],[f38799,f27]) ).
fof(f41217,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f41070]) ).
fof(f41313,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))),true) = true,
inference(paramodulation,[status(thm)],[f41217,f1991]) ).
fof(f41433,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f41313]) ).
fof(f42626,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))),true) = true,
inference(paramodulation,[status(thm)],[f41433,f1991]) ).
fof(f42756,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f42626]) ).
fof(f69345,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),true) = true,
inference(paramodulation,[status(thm)],[f42756,f25324]) ).
fof(f69790,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f69345]) ).
fof(f70226,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))),true) = true,
inference(paramodulation,[status(thm)],[f69790,f28]) ).
fof(f70306,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),implies(X0,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f70226]) ).
fof(f76516,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(not(X0),implies(X0,X1))),true) = true,
inference(paramodulation,[status(thm)],[f70306,f118]) ).
fof(f76685,plain,
! [X0,X1] : is_a_theorem(implies(not(X0),implies(X0,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f76516]) ).
fof(f76994,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))),true) = true,
inference(paramodulation,[status(thm)],[f76685,f28]) ).
fof(f77046,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f76994]) ).
fof(f78665,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(X0,X1),implies(not(X1),implies(X0,X2)))),true) = true,
inference(paramodulation,[status(thm)],[f77046,f1991]) ).
fof(f78806,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(X1),implies(X0,X2)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f78665]) ).
fof(f88058,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),implies(X1,X2))),true) = true,
inference(paramodulation,[status(thm)],[f78806,f24380]) ).
fof(f88220,plain,
! [X0,X1,X2] : is_a_theorem(implies(not(implies(X0,X1)),implies(X1,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f88058]) ).
fof(f88543,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X3,X0)),X2))),true) = true,
inference(paramodulation,[status(thm)],[f88220,f28]) ).
fof(f88600,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X3,X0)),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f88543]) ).
fof(f153140,plain,
! [X0,X1,X2,X3] : ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),implies(not(implies(X1,X2)),X3))),true) = true,
inference(paramodulation,[status(thm)],[f88600,f32]) ).
fof(f153324,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(not(implies(X0,X1)),implies(not(implies(X1,X2)),X3))) = true,
inference(forward_demodulation,[status(thm)],[f7,f153140]) ).
fof(f159890,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(not(implies(X0,X1)),X0)),true) = true,
inference(paramodulation,[status(thm)],[f153324,f27]) ).
fof(f160058,plain,
! [X0,X1] : is_a_theorem(implies(not(implies(X0,X1)),X0)) = true,
inference(forward_demodulation,[status(thm)],[f7,f159890]) ).
fof(f160073,plain,
true != true,
inference(backward_demodulation,[status(thm)],[f160058,f12]) ).
fof(f160544,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f160073]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL400-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n013.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 00:27:36 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 85.78/11.42 % Refutation found
% 85.78/11.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 85.78/11.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.04/11.64 % Elapsed time: 11.163767 seconds
% 5.04/11.64 % CPU time: 87.570425 seconds
% 5.04/11.64 % Total memory used: 564.560 MB
% 5.04/11.64 % Net memory used: 529.132 MB
%------------------------------------------------------------------------------