%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL050-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 : n015.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:06:40 PM UTC 2026
% Result : Unsatisfiable 69.94s 9.58s
% Output : CNFRefutation 47.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 6
% Syntax : Number of formulae : 104 ( 104 unt; 0 def)
% Number of atoms : 104 ( 103 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 : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 276 ( 276 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : is_a_theorem(implies(implies(not(X),X),X)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))) != true,
file('/export/starexec/sandbox/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(implies(a,implies(b,c)),implies(b,implies(a,c)))) != true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f20,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(f21,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(f22,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(f23,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(f29,plain,
! [X0] : ifeq(is_a_theorem(implies(not(X0),X0)),true,is_a_theorem(X0),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f20]) ).
fof(f30,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,f21]) ).
fof(f31,plain,
! [X0,X1] : ifeq(is_a_theorem(X0),true,is_a_theorem(implies(not(X0),X1)),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f22]) ).
fof(f32,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,f23]) ).
fof(f35,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,f30]) ).
fof(f36,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,f30]) ).
fof(f37,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,f30]) ).
fof(f41,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f35]) ).
fof(f42,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,f36]) ).
fof(f43,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f37]) ).
fof(f46,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(X0),X0),X1),X2),implies(implies(X0,X1),X2))),true) = true,
inference(paramodulation,[status(thm)],[f41,f30]) ).
fof(f49,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)],[f41,f8]) ).
fof(f51,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X1),X2),implies(implies(X0,X1),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f46]) ).
fof(f53,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,f49]) ).
fof(f56,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)],[f43,f8]) ).
fof(f58,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)],[f43,f8]) ).
fof(f61,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,f56]) ).
fof(f62,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,f58]) ).
fof(f67,plain,
! [X0,X1,X2,X3] : ifeq(is_a_theorem(implies(implies(implies(implies(implies(not(X0),X0),X1),X2),implies(implies(X0,X1),X2)),X3)),true,ifeq(true,true,is_a_theorem(X3),true),true) = true,
inference(paramodulation,[status(thm)],[f51,f8]) ).
fof(f71,plain,
! [X0,X1,X2,X3] : ifeq(is_a_theorem(implies(implies(implies(implies(implies(not(X0),X0),X1),X2),implies(implies(X0,X1),X2)),X3)),true,is_a_theorem(X3),true) = true,
inference(forward_demodulation,[status(thm)],[f7,f67]) ).
fof(f630,plain,
! [X0] : ifeq(true,true,is_a_theorem(implies(X0,X0)),true) = true,
inference(paramodulation,[status(thm)],[f43,f32]) ).
fof(f664,plain,
! [X0] : is_a_theorem(implies(X0,X0)) = true,
inference(forward_demodulation,[status(thm)],[f7,f630]) ).
fof(f724,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)],[f42,f8]) ).
fof(f738,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,f724]) ).
fof(f780,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(not(implies(X0,X0)),X1)),true) = true,
inference(paramodulation,[status(thm)],[f664,f31]) ).
fof(f791,plain,
! [X0,X1] : is_a_theorem(implies(not(implies(X0,X0)),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f780]) ).
fof(f811,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)],[f791,f30]) ).
fof(f825,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(implies(X2,X2)),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f811]) ).
fof(f1633,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))),true) = true,
inference(paramodulation,[status(thm)],[f825,f61]) ).
fof(f1697,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f1633]) ).
fof(f1774,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)],[f1697,f30]) ).
fof(f1800,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,f1774]) ).
fof(f1969,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X1))),true) = true,
inference(paramodulation,[status(thm)],[f1800,f32]) ).
fof(f2004,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f1969]) ).
fof(f2111,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)],[f2004,f30]) ).
fof(f2136,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2111]) ).
fof(f2244,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))),true) = true,
inference(paramodulation,[status(thm)],[f2136,f53]) ).
fof(f2263,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)],[f2136,f30]) ).
fof(f2264,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)],[f2136,f8]) ).
fof(f2279,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(not(X1),X1),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f2244]) ).
fof(f2284,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,f2263]) ).
fof(f2285,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,f2264]) ).
fof(f2360,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)],[f2279,f30]) ).
fof(f2385,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,f2360]) ).
fof(f5307,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(implies(implies(X0,X0),X1),X1)),true) = true,
inference(paramodulation,[status(thm)],[f2284,f32]) ).
fof(f5345,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f5307]) ).
fof(f5388,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)],[f5345,f30]) ).
fof(f5414,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,f5388]) ).
fof(f6173,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)],[f5414,f2285]) ).
fof(f6303,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(implies(implies(X1,X1),X2),X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f6173]) ).
fof(f6443,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)],[f6303,f30]) ).
fof(f6475,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,f6443]) ).
fof(f8326,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)],[f2385,f738]) ).
fof(f8448,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,f8326]) ).
fof(f9721,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)],[f8448,f738]) ).
fof(f9800,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,f9721]) ).
fof(f10375,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)],[f9800,f61]) ).
fof(f10438,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X0),X0)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f10375]) ).
fof(f10594,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)],[f10438,f30]) ).
fof(f10630,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,f10594]) ).
fof(f11913,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)],[f6475,f738]) ).
fof(f11991,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,f11913]) ).
fof(f13766,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X1,X0),X0))),true) = true,
inference(paramodulation,[status(thm)],[f10630,f32]) ).
fof(f13839,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,X0),X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f13766]) ).
fof(f13962,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)],[f13839,f30]) ).
fof(f14001,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,f13962]) ).
fof(f14107,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(X1,X0))),true) = true,
inference(paramodulation,[status(thm)],[f14001,f62]) ).
fof(f14178,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f14107]) ).
fof(f14371,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)],[f14178,f30]) ).
fof(f14414,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))) = true,
inference(forward_demodulation,[status(thm)],[f7,f14371]) ).
fof(f14668,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)],[f14414,f8]) ).
fof(f14718,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,f14668]) ).
fof(f32219,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)],[f11991,f71]) ).
fof(f32375,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,f32219]) ).
fof(f32541,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)],[f32375,f29]) ).
fof(f32671,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),X0),X0),X1),X1)) = true,
inference(forward_demodulation,[status(thm)],[f7,f32541]) ).
fof(f32758,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)],[f32671,f738]) ).
fof(f32859,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f32758]) ).
fof(f32932,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)],[f32859,f738]) ).
fof(f33037,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))) = true,
inference(forward_demodulation,[status(thm)],[f7,f32932]) ).
fof(f49077,plain,
! [X0,X1] : ifeq(true,true,is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),true) = true,
inference(paramodulation,[status(thm)],[f33037,f14718]) ).
fof(f49473,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))) = true,
inference(forward_demodulation,[status(thm)],[f7,f49077]) ).
fof(f50026,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)],[f49473,f30]) ).
fof(f50081,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,f50026]) ).
fof(f54614,plain,
! [X0,X1,X2] : ifeq(true,true,is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),true) = true,
inference(paramodulation,[status(thm)],[f50081,f738]) ).
fof(f54744,plain,
true != true,
inference(backward_demodulation,[status(thm)],[f54745,f12]) ).
fof(f54745,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))) = true,
inference(forward_demodulation,[status(thm)],[f7,f54614]) ).
fof(f54765,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f54744]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL050-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.67 % Computer : n015.cluster.edu
% 0.16/0.67 % Model : x86_64 x86_64
% 0.16/0.67 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.67 % Memory : 8046.5625MB
% 0.16/0.67 % OS : Linux 6.8.0-71-generic
% 0.16/0.67 % CPULimit : 300
% 0.16/0.67 % WCLimit : 300
% 0.16/0.67 % DateTime : Mon Sep 21 00:05:21 UTC 2026
% 0.16/0.67 % CPUTime :
% 0.16/0.68 % Drodi V4.1.1
% 69.94/9.58 % Refutation found
% 69.94/9.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 69.94/9.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 68.07/10.41 % Elapsed time: 9.713954 seconds
% 68.07/10.41 % CPU time: 72.557851 seconds
% 68.07/10.41 % Total memory used: 630.707 MB
% 68.07/10.41 % Net memory used: 589.225 MB
%------------------------------------------------------------------------------