%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL050-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 07:57:50 AM UTC 2026
% Result : Unsatisfiable 12.29s 1.99s
% Output : CNFRefutation 12.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 6
% Syntax : Number of formulae : 87 ( 87 unt; 0 def)
% Number of atoms : 87 ( 86 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 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 : 222 ( 56 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(condensed_detachment,axiom,
! [VAR_0,VAR_1] : ifeq(is_a_theorem(implies(VAR_0,VAR_1)),true,ifeq(is_a_theorem(VAR_0),true,is_a_theorem(VAR_1),true),true) = true,
file('theBenchmark.p',condensed_detachment) ).
cnf(c_2,plain,
ifeq(is_a_theorem(implies(A,B)),true,ifeq(is_a_theorem(A),true,is_a_theorem(B),true),true) = true,
inference(clausify,[status(thm)],[condensed_detachment]) ).
fof(cn_1,axiom,
! [VAR_0,VAR_1,VAR_2] : is_a_theorem(implies(implies(VAR_0,VAR_1),implies(implies(VAR_1,VAR_2),implies(VAR_0,VAR_2)))) = true,
file('theBenchmark.p',cn_1) ).
cnf(c_3,plain,
is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))) = true,
inference(clausify,[status(thm)],[cn_1]) ).
fof(cn_2,axiom,
! [VAR_0] : is_a_theorem(implies(implies(not(VAR_0),VAR_0),VAR_0)) = true,
file('theBenchmark.p',cn_2) ).
cnf(c_4,plain,
is_a_theorem(implies(implies(not(A),A),A)) = true,
inference(clausify,[status(thm)],[cn_2]) ).
fof(cn_3,axiom,
! [VAR_0,VAR_1] : is_a_theorem(implies(VAR_0,implies(not(VAR_0),VAR_1))) = true,
file('theBenchmark.p',cn_3) ).
cnf(c_5,plain,
is_a_theorem(implies(A,implies(not(A),B))) = true,
inference(clausify,[status(thm)],[cn_3]) ).
fof(prove_cn_21,axiom,
is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))) != true,
file('theBenchmark.p',prove_cn_21) ).
cnf(c_6,plain,
is_a_theorem(implies(implies(a,implies(b,c)),implies(b,implies(a,c)))) != true,
inference(clausify,[status(thm)],[prove_cn_21]) ).
cnf(c_4458,plain,
ifeq(true,true,ifeq(is_a_theorem(implies(A,B)),true,is_a_theorem(implies(implies(B,C),implies(A,C))),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_7,plain,
ifeq(is_a_theorem(implies(A,B)),true,is_a_theorem(implies(implies(B,C),implies(A,C))),true) = true,
inference(paramod,[status(thm)],[c_1,c_4458]) ).
cnf(c_4459,plain,
ifeq(true,true,ifeq(is_a_theorem(implies(not(A),A)),true,is_a_theorem(A),true),true) = true,
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_10,plain,
ifeq(is_a_theorem(implies(not(A),A)),true,is_a_theorem(A),true) = true,
inference(paramod,[status(thm)],[c_1,c_4459]) ).
cnf(c_4460,plain,
ifeq(is_a_theorem(implies(implies(implies(not(A),A),A),B)),true,ifeq(true,true,is_a_theorem(B),true),true) = true,
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_11,plain,
ifeq(is_a_theorem(implies(implies(implies(not(A),A),A),B)),true,is_a_theorem(B),true) = true,
inference(paramod,[status(thm)],[c_1,c_4460]) ).
cnf(c_4461,plain,
ifeq(true,true,ifeq(is_a_theorem(A),true,is_a_theorem(implies(not(A),B)),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_13,plain,
ifeq(is_a_theorem(A),true,is_a_theorem(implies(not(A),B)),true) = true,
inference(paramod,[status(thm)],[c_1,c_4461]) ).
cnf(c_4462,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(implies(A,B),implies(C,B)),D),implies(implies(C,A),D))),true) = true,
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_16,plain,
is_a_theorem(implies(implies(implies(implies(A,B),implies(C,B)),D),implies(implies(C,A),D))) = true,
inference(paramod,[status(thm)],[c_1,c_4462]) ).
cnf(c_4463,plain,
ifeq(true,true,is_a_theorem(implies(implies(A,B),implies(implies(not(A),A),B))),true) = true,
inference(paramod,[status(thm)],[c_4,c_7]) ).
cnf(c_18,plain,
is_a_theorem(implies(implies(A,B),implies(implies(not(A),A),B))) = true,
inference(paramod,[status(thm)],[c_1,c_4463]) ).
cnf(c_4464,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(not(A),B),C),implies(A,C))),true) = true,
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_19,plain,
is_a_theorem(implies(implies(implies(not(A),B),C),implies(A,C))) = true,
inference(paramod,[status(thm)],[c_1,c_4464]) ).
cnf(c_4465,plain,
ifeq(is_a_theorem(implies(implies(implies(A,B),implies(implies(not(A),A),B)),C)),true,ifeq(true,true,is_a_theorem(C),true),true) = true,
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_37,plain,
ifeq(is_a_theorem(implies(implies(implies(A,B),implies(implies(not(A),A),B)),C)),true,is_a_theorem(C),true) = true,
inference(paramod,[status(thm)],[c_1,c_4465]) ).
cnf(c_4466,plain,
ifeq(true,true,ifeq(is_a_theorem(implies(implies(not(A),B),C)),true,is_a_theorem(implies(A,C)),true),true) = true,
inference(paramod,[status(thm)],[c_19,c_2]) ).
cnf(c_41,plain,
ifeq(is_a_theorem(implies(implies(not(A),B),C)),true,is_a_theorem(implies(A,C)),true) = true,
inference(paramod,[status(thm)],[c_1,c_4466]) ).
cnf(c_4467,plain,
ifeq(is_a_theorem(implies(implies(implies(implies(not(A),B),C),implies(A,C)),D)),true,ifeq(true,true,is_a_theorem(D),true),true) = true,
inference(paramod,[status(thm)],[c_19,c_2]) ).
cnf(c_42,plain,
ifeq(is_a_theorem(implies(implies(implies(implies(not(A),B),C),implies(A,C)),D)),true,is_a_theorem(D),true) = true,
inference(paramod,[status(thm)],[c_1,c_4467]) ).
cnf(c_4468,plain,
ifeq(true,true,is_a_theorem(implies(A,A)),true) = true,
inference(paramod,[status(thm)],[c_19,c_11]) ).
cnf(c_52,plain,
is_a_theorem(implies(A,A)) = true,
inference(paramod,[status(thm)],[c_1,c_4468]) ).
cnf(c_4469,plain,
ifeq(true,true,is_a_theorem(implies(not(implies(A,A)),B)),true) = true,
inference(paramod,[status(thm)],[c_52,c_13]) ).
cnf(c_55,plain,
is_a_theorem(implies(not(implies(A,A)),B)) = true,
inference(paramod,[status(thm)],[c_1,c_4469]) ).
cnf(c_4470,plain,
ifeq(true,true,is_a_theorem(implies(implies(A,B),implies(not(implies(C,C)),B))),true) = true,
inference(paramod,[status(thm)],[c_55,c_7]) ).
cnf(c_58,plain,
is_a_theorem(implies(implies(A,B),implies(not(implies(C,C)),B))) = true,
inference(paramod,[status(thm)],[c_1,c_4470]) ).
cnf(c_4471,plain,
ifeq(true,true,ifeq(is_a_theorem(implies(implies(implies(A,B),implies(C,B)),D)),true,is_a_theorem(implies(implies(C,A),D)),true),true) = true,
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_75,plain,
ifeq(is_a_theorem(implies(implies(implies(A,B),implies(C,B)),D)),true,is_a_theorem(implies(implies(C,A),D)),true) = true,
inference(paramod,[status(thm)],[c_1,c_4471]) ).
cnf(c_4472,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(not(implies(B,B)),C))),true) = true,
inference(paramod,[status(thm)],[c_58,c_41]) ).
cnf(c_170,plain,
is_a_theorem(implies(A,implies(not(implies(B,B)),C))) = true,
inference(paramod,[status(thm)],[c_1,c_4472]) ).
cnf(c_4473,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(not(implies(A,A)),B),C),implies(D,C))),true) = true,
inference(paramod,[status(thm)],[c_170,c_7]) ).
cnf(c_174,plain,
is_a_theorem(implies(implies(implies(not(implies(A,A)),B),C),implies(D,C))) = true,
inference(paramod,[status(thm)],[c_1,c_4473]) ).
cnf(c_4474,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(B,B))),true) = true,
inference(paramod,[status(thm)],[c_174,c_11]) ).
cnf(c_218,plain,
is_a_theorem(implies(A,implies(B,B))) = true,
inference(paramod,[status(thm)],[c_1,c_4474]) ).
cnf(c_4475,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(A,A),B),implies(C,B))),true) = true,
inference(paramod,[status(thm)],[c_218,c_7]) ).
cnf(c_224,plain,
is_a_theorem(implies(implies(implies(A,A),B),implies(C,B))) = true,
inference(paramod,[status(thm)],[c_1,c_4475]) ).
cnf(c_4476,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(implies(not(B),B),B))),true) = true,
inference(paramod,[status(thm)],[c_224,c_37]) ).
cnf(c_238,plain,
is_a_theorem(implies(A,implies(implies(not(B),B),B))) = true,
inference(paramod,[status(thm)],[c_1,c_4476]) ).
cnf(c_4477,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(A),A),A),B),implies(C,B))),true) = true,
inference(paramod,[status(thm)],[c_238,c_7]) ).
cnf(c_246,plain,
is_a_theorem(implies(implies(implies(implies(not(A),A),A),B),implies(C,B))) = true,
inference(paramod,[status(thm)],[c_1,c_4477]) ).
cnf(c_4478,plain,
ifeq(true,true,is_a_theorem(implies(implies(A,implies(not(B),B)),implies(C,implies(A,B)))),true) = true,
inference(paramod,[status(thm)],[c_246,c_75]) ).
cnf(c_636,plain,
is_a_theorem(implies(implies(A,implies(not(B),B)),implies(C,implies(A,B)))) = true,
inference(paramod,[status(thm)],[c_1,c_4478]) ).
cnf(c_4479,plain,
ifeq(true,true,is_a_theorem(implies(implies(not(A),B),implies(C,implies(implies(B,A),A)))),true) = true,
inference(paramod,[status(thm)],[c_636,c_75]) ).
cnf(c_677,plain,
is_a_theorem(implies(implies(not(A),B),implies(C,implies(implies(B,A),A)))) = true,
inference(paramod,[status(thm)],[c_1,c_4479]) ).
cnf(c_4480,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(B,implies(implies(C,A),A)))),true) = true,
inference(paramod,[status(thm)],[c_677,c_41]) ).
cnf(c_780,plain,
is_a_theorem(implies(A,implies(B,implies(implies(C,A),A)))) = true,
inference(paramod,[status(thm)],[c_1,c_4480]) ).
cnf(c_4481,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(A,implies(implies(B,C),C)),D),implies(C,D))),true) = true,
inference(paramod,[status(thm)],[c_780,c_7]) ).
cnf(c_788,plain,
is_a_theorem(implies(implies(implies(A,implies(implies(B,C),C)),D),implies(C,D))) = true,
inference(paramod,[status(thm)],[c_1,c_4481]) ).
cnf(c_4482,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(implies(B,A),A))),true) = true,
inference(paramod,[status(thm)],[c_788,c_11]) ).
cnf(c_1584,plain,
is_a_theorem(implies(A,implies(implies(B,A),A))) = true,
inference(paramod,[status(thm)],[c_1,c_4482]) ).
cnf(c_4483,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(implies(A,B),B),C),implies(B,C))),true) = true,
inference(paramod,[status(thm)],[c_1584,c_7]) ).
cnf(c_1596,plain,
is_a_theorem(implies(implies(implies(implies(A,B),B),C),implies(B,C))) = true,
inference(paramod,[status(thm)],[c_1,c_4483]) ).
cnf(c_4484,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(B,A))),true) = true,
inference(paramod,[status(thm)],[c_1596,c_42]) ).
cnf(c_1654,plain,
is_a_theorem(implies(A,implies(B,A))) = true,
inference(paramod,[status(thm)],[c_1,c_4484]) ).
cnf(c_4485,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(A,B),C),implies(B,C))),true) = true,
inference(paramod,[status(thm)],[c_1654,c_7]) ).
cnf(c_1663,plain,
is_a_theorem(implies(implies(implies(A,B),C),implies(B,C))) = true,
inference(paramod,[status(thm)],[c_1,c_4485]) ).
cnf(c_4486,plain,
ifeq(true,true,ifeq(is_a_theorem(implies(implies(A,B),C)),true,is_a_theorem(implies(B,C)),true),true) = true,
inference(paramod,[status(thm)],[c_1663,c_2]) ).
cnf(c_1704,plain,
ifeq(is_a_theorem(implies(implies(A,B),C)),true,is_a_theorem(implies(B,C)),true) = true,
inference(paramod,[status(thm)],[c_1,c_4486]) ).
cnf(c_4487,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(B,implies(implies(A,C),C)))),true) = true,
inference(paramod,[status(thm)],[c_677,c_1704]) ).
cnf(c_2437,plain,
is_a_theorem(implies(A,implies(B,implies(implies(A,C),C)))) = true,
inference(paramod,[status(thm)],[c_1,c_4487]) ).
cnf(c_4488,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(implies(implies(implies(not(B),B),B),C),C))),true) = true,
inference(paramod,[status(thm)],[c_2437,c_11]) ).
cnf(c_2475,plain,
is_a_theorem(implies(A,implies(implies(implies(implies(not(B),B),B),C),C))) = true,
inference(paramod,[status(thm)],[c_1,c_4488]) ).
cnf(c_4489,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(implies(not(A),A),A),B),B)),true) = true,
inference(paramod,[status(thm)],[c_2475,c_10]) ).
cnf(c_3917,plain,
is_a_theorem(implies(implies(implies(implies(not(A),A),A),B),B)) = true,
inference(paramod,[status(thm)],[c_1,c_4489]) ).
cnf(c_4490,plain,
ifeq(true,true,is_a_theorem(implies(implies(A,implies(not(B),B)),implies(A,B))),true) = true,
inference(paramod,[status(thm)],[c_3917,c_75]) ).
cnf(c_3935,plain,
is_a_theorem(implies(implies(A,implies(not(B),B)),implies(A,B))) = true,
inference(paramod,[status(thm)],[c_1,c_4490]) ).
cnf(c_4491,plain,
ifeq(true,true,is_a_theorem(implies(implies(not(A),B),implies(implies(B,A),A))),true) = true,
inference(paramod,[status(thm)],[c_3935,c_75]) ).
cnf(c_3946,plain,
is_a_theorem(implies(implies(not(A),B),implies(implies(B,A),A))) = true,
inference(paramod,[status(thm)],[c_1,c_4491]) ).
cnf(c_4492,plain,
ifeq(true,true,is_a_theorem(implies(A,implies(implies(A,B),B))),true) = true,
inference(paramod,[status(thm)],[c_3946,c_1704]) ).
cnf(c_3965,plain,
is_a_theorem(implies(A,implies(implies(A,B),B))) = true,
inference(paramod,[status(thm)],[c_1,c_4492]) ).
cnf(c_4493,plain,
ifeq(true,true,is_a_theorem(implies(implies(implies(implies(A,B),B),C),implies(A,C))),true) = true,
inference(paramod,[status(thm)],[c_3965,c_7]) ).
cnf(c_3971,plain,
is_a_theorem(implies(implies(implies(implies(A,B),B),C),implies(A,C))) = true,
inference(paramod,[status(thm)],[c_1,c_4493]) ).
cnf(c_4494,plain,
ifeq(true,true,is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))),true) = true,
inference(paramod,[status(thm)],[c_3971,c_75]) ).
cnf(c_4456,plain,
is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))) = true,
inference(paramod,[status(thm)],[c_1,c_4494]) ).
cnf(c_4457,plain,
$false,
inference(resolve,[status(thm)],[c_4456,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL050-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n012.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 : Fri Sep 25 21:45:50 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 3126554 was started by sandbox2 on n012,
% 0.07/0.35 % Fri Sep 25 21:45:50 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.07/0.35
% 0.07/0.35 % From the command line: assign(max_seconds, 300).
% 12.29/1.99
% 12.29/1.99 % SZS status Unsatisfiable for theBenchmark
% 12.29/1.99
% 12.29/1.99 % Proof 1 at 1.16 (+ 0.46) seconds.
% 12.29/1.99 % Length of proof is 44.
% 12.29/1.99 % Level of proof is 29.
% 12.29/1.99 % Maximum clause weight is 21.000.
% 12.29/1.99 % Given clauses 389.
% 12.29/1.99
% 12.29/1.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------