%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL096-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 : n016.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:58 AM UTC 2026
% Result : Unsatisfiable 30.96s 4.42s
% Output : CNFRefutation 30.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 6
% Syntax : Number of formulae : 75 ( 75 unt; 0 def)
% Number of atoms : 75 ( 74 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-4 aty)
% Number of variables : 256 ( 1 sgn 19 !; 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(equivalent(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(equivalent(A,B)),true,ifeq(is_a_theorem(A),true,is_a_theorem(B),true),true) = true,
inference(clausify,[status(thm)],[condensed_detachment]) ).
fof(lg_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(VAR_0,VAR_1),equivalent(VAR_0,VAR_2)),equivalent(VAR_1,VAR_2)),VAR_3),VAR_3)) = true,
file('theBenchmark.p',lg_2) ).
cnf(c_3,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(B,C)),D),D)) = true,
inference(clausify,[status(thm)],[lg_2]) ).
fof(lg_3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(VAR_0,VAR_1),equivalent(VAR_0,VAR_2)),VAR_3),equivalent(equivalent(VAR_1,VAR_2),VAR_3)),VAR_4),VAR_4)) = true,
file('theBenchmark.p',lg_3) ).
cnf(c_4,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),D),equivalent(equivalent(B,C),D)),E),E)) = true,
inference(clausify,[status(thm)],[lg_3]) ).
fof(lg_4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(VAR_0,VAR_1),VAR_2),VAR_3),equivalent(equivalent(equivalent(VAR_0,VAR_4),VAR_2),equivalent(equivalent(VAR_1,VAR_4),VAR_3)))) = true,
file('theBenchmark.p',lg_4) ).
cnf(c_5,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),C),D),equivalent(equivalent(equivalent(A,E),C),equivalent(equivalent(B,E),D)))) = true,
inference(clausify,[status(thm)],[lg_4]) ).
fof(prove_lg_1,axiom,
is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(equivalent(b,b),a)),c),c)) != true,
file('theBenchmark.p',prove_lg_1) ).
cnf(c_6,plain,
is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(equivalent(b,b),a)),c),c)) != true,
inference(clausify,[status(thm)],[prove_lg_1]) ).
cnf(c_2668,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(B,C)),D)),true,is_a_theorem(D),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_7,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(B,C)),D)),true,is_a_theorem(D),true) = true,
inference(paramod,[status(thm)],[c_1,c_2668]) ).
cnf(c_2669,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),D),equivalent(equivalent(B,C),D)),E)),true,is_a_theorem(E),true),true) = true,
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_8,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),D),equivalent(equivalent(B,C),D)),E)),true,is_a_theorem(E),true) = true,
inference(paramod,[status(thm)],[c_1,c_2669]) ).
cnf(c_2670,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(A,B),C),D)),true,is_a_theorem(equivalent(equivalent(equivalent(A,E),C),equivalent(equivalent(B,E),D))),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_9,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(A,B),C),D)),true,is_a_theorem(equivalent(equivalent(equivalent(A,E),C),equivalent(equivalent(B,E),D))),true) = true,
inference(paramod,[status(thm)],[c_1,c_2670]) ).
cnf(c_2671,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(equivalent(D,B),equivalent(D,C)))),true) = true,
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_10,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(equivalent(D,B),equivalent(D,C)))) = true,
inference(paramod,[status(thm)],[c_1,c_2671]) ).
cnf(c_2672,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,B),equivalent(A,B))),true) = true,
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_11,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(A,B))) = true,
inference(paramod,[status(thm)],[c_1,c_2672]) ).
cnf(c_2673,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,B),C),equivalent(equivalent(D,B),equivalent(equivalent(A,D),C)))),true) = true,
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_12,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),C),equivalent(equivalent(D,B),equivalent(equivalent(A,D),C)))) = true,
inference(paramod,[status(thm)],[c_1,c_2673]) ).
cnf(c_2674,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),D),E),equivalent(equivalent(equivalent(B,C),D),E))),true) = true,
inference(paramod,[status(thm)],[c_3,c_9]) ).
cnf(c_13,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),D),E),equivalent(equivalent(equivalent(B,C),D),E))) = true,
inference(paramod,[status(thm)],[c_1,c_2674]) ).
cnf(c_2675,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(B,C))),true) = true,
inference(paramod,[status(thm)],[c_11,c_7]) ).
cnf(c_18,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(A,C)),equivalent(B,C))) = true,
inference(paramod,[status(thm)],[c_1,c_2675]) ).
cnf(c_2676,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(A,B),equivalent(A,C))),true,is_a_theorem(equivalent(B,C)),true),true) = true,
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_21,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,B),equivalent(A,C))),true,is_a_theorem(equivalent(B,C)),true) = true,
inference(paramod,[status(thm)],[c_1,c_2676]) ).
cnf(c_2677,plain,
ifeq(true,true,is_a_theorem(equivalent(A,equivalent(equivalent(B,B),A))),true) = true,
inference(paramod,[status(thm)],[c_5,c_21]) ).
cnf(c_23,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(B,B),A))) = true,
inference(paramod,[status(thm)],[c_1,c_2677]) ).
cnf(c_2678,plain,
ifeq(true,true,is_a_theorem(equivalent(A,A)),true) = true,
inference(paramod,[status(thm)],[c_11,c_21]) ).
cnf(c_24,plain,
is_a_theorem(equivalent(A,A)) = true,
inference(paramod,[status(thm)],[c_1,c_2678]) ).
cnf(c_2679,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,A),B)),true,ifeq(true,true,is_a_theorem(B),true),true) = true,
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_27,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,A),B)),true,is_a_theorem(B),true) = true,
inference(paramod,[status(thm)],[c_1,c_2679]) ).
cnf(c_2680,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(A,B),equivalent(A,C))),true,is_a_theorem(equivalent(equivalent(D,B),equivalent(D,C))),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_30,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,B),equivalent(A,C))),true,is_a_theorem(equivalent(equivalent(D,B),equivalent(D,C))),true) = true,
inference(paramod,[status(thm)],[c_1,c_2680]) ).
cnf(c_2681,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(A,B),C)),true,is_a_theorem(equivalent(equivalent(D,B),equivalent(equivalent(A,D),C))),true),true) = true,
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_34,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,B),C)),true,is_a_theorem(equivalent(equivalent(D,B),equivalent(equivalent(A,D),C))),true) = true,
inference(paramod,[status(thm)],[c_1,c_2681]) ).
cnf(c_2682,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(equivalent(equivalent(B,D),A),equivalent(D,C)))),true) = true,
inference(paramod,[status(thm)],[c_12,c_7]) ).
cnf(c_36,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(equivalent(equivalent(B,D),A),equivalent(D,C)))) = true,
inference(paramod,[status(thm)],[c_1,c_2682]) ).
cnf(c_2683,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,A),D)),equivalent(equivalent(C,B),D))),true) = true,
inference(paramod,[status(thm)],[c_13,c_7]) ).
cnf(c_40,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(C,A),D)),equivalent(equivalent(C,B),D))) = true,
inference(paramod,[status(thm)],[c_1,c_2683]) ).
cnf(c_2684,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(C,A),equivalent(C,B)))),true) = true,
inference(paramod,[status(thm)],[c_12,c_27]) ).
cnf(c_43,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(C,A),equivalent(C,B)))) = true,
inference(paramod,[status(thm)],[c_1,c_2684]) ).
cnf(c_2685,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,B),A)),C)),true,ifeq(true,true,is_a_theorem(C),true),true) = true,
inference(paramod,[status(thm)],[c_23,c_2]) ).
cnf(c_46,plain,
ifeq(is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,B),A)),C)),true,is_a_theorem(C),true) = true,
inference(paramod,[status(thm)],[c_1,c_2685]) ).
cnf(c_2686,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(B,D))),equivalent(A,equivalent(C,D)))),true) = true,
inference(paramod,[status(thm)],[c_43,c_7]) ).
cnf(c_72,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(B,D))),equivalent(A,equivalent(C,D)))) = true,
inference(paramod,[status(thm)],[c_1,c_2686]) ).
cnf(c_2687,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),B),C),equivalent(B,C))),true) = true,
inference(paramod,[status(thm)],[c_36,c_46]) ).
cnf(c_226,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),B),C),equivalent(B,C))) = true,
inference(paramod,[status(thm)],[c_1,c_2687]) ).
cnf(c_2688,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,B),C)),equivalent(A,C))),true) = true,
inference(paramod,[status(thm)],[c_40,c_30]) ).
cnf(c_310,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,B),C)),equivalent(A,C))) = true,
inference(paramod,[status(thm)],[c_1,c_2688]) ).
cnf(c_2689,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),D)),equivalent(equivalent(equivalent(C,E),A),equivalent(equivalent(B,E),D)))),true) = true,
inference(paramod,[status(thm)],[c_40,c_34]) ).
cnf(c_313,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),D)),equivalent(equivalent(equivalent(C,E),A),equivalent(equivalent(B,E),D)))) = true,
inference(paramod,[status(thm)],[c_1,c_2689]) ).
cnf(c_2690,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,B),C))),true,is_a_theorem(equivalent(A,C)),true),true) = true,
inference(paramod,[status(thm)],[c_310,c_2]) ).
cnf(c_403,plain,
ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,B),C))),true,is_a_theorem(equivalent(A,C)),true) = true,
inference(paramod,[status(thm)],[c_1,c_2690]) ).
cnf(c_2691,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(B,A),C)),C)),true) = true,
inference(paramod,[status(thm)],[c_40,c_403]) ).
cnf(c_420,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(equivalent(B,A),C)),C)) = true,
inference(paramod,[status(thm)],[c_1,c_2691]) ).
cnf(c_2692,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),D)),equivalent(equivalent(equivalent(C,B),A),D))),true) = true,
inference(paramod,[status(thm)],[c_420,c_34]) ).
cnf(c_574,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),D)),equivalent(equivalent(equivalent(C,B),A),D))) = true,
inference(paramod,[status(thm)],[c_1,c_2692]) ).
cnf(c_2693,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(B,D)))),true,is_a_theorem(equivalent(A,equivalent(C,D))),true),true) = true,
inference(paramod,[status(thm)],[c_72,c_2]) ).
cnf(c_638,plain,
ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(B,D)))),true,is_a_theorem(equivalent(A,equivalent(C,D))),true) = true,
inference(paramod,[status(thm)],[c_1,c_2693]) ).
cnf(c_2694,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(B,C)),equivalent(B,D)),equivalent(C,D))),true) = true,
inference(paramod,[status(thm)],[c_226,c_638]) ).
cnf(c_761,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,A),equivalent(B,C)),equivalent(B,D)),equivalent(C,D))) = true,
inference(paramod,[status(thm)],[c_1,c_2694]) ).
cnf(c_2695,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,C),D))),true,is_a_theorem(equivalent(equivalent(equivalent(C,B),A),D)),true),true) = true,
inference(paramod,[status(thm)],[c_574,c_2]) ).
cnf(c_1819,plain,
ifeq(is_a_theorem(equivalent(A,equivalent(equivalent(B,C),D))),true,is_a_theorem(equivalent(equivalent(equivalent(C,B),A),D)),true) = true,
inference(paramod,[status(thm)],[c_1,c_2695]) ).
cnf(c_2696,plain,
ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(B,C)),equivalent(B,D))),true,is_a_theorem(equivalent(C,D)),true),true) = true,
inference(paramod,[status(thm)],[c_761,c_2]) ).
cnf(c_2296,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(A,A),equivalent(B,C)),equivalent(B,D))),true,is_a_theorem(equivalent(C,D)),true) = true,
inference(paramod,[status(thm)],[c_1,c_2696]) ).
cnf(c_2697,plain,
ifeq(true,true,is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,B),C),C),A))),true) = true,
inference(paramod,[status(thm)],[c_313,c_2296]) ).
cnf(c_2645,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,B),C),C),A))) = true,
inference(paramod,[status(thm)],[c_1,c_2697]) ).
cnf(c_2698,plain,
ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,B),A)),C),C)),true) = true,
inference(paramod,[status(thm)],[c_2645,c_1819]) ).
cnf(c_2666,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,B),A)),C),C)) = true,
inference(paramod,[status(thm)],[c_1,c_2698]) ).
cnf(c_2667,plain,
$false,
inference(resolve,[status(thm)],[c_2666,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL096-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n016.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 21:55:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 3383687 was started by sandbox2 on n016,
% 0.11/0.37 % Fri Sep 25 21:55:45 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 30.96/4.42
% 30.96/4.42 % SZS status Unsatisfiable for theBenchmark
% 30.96/4.42
% 30.96/4.42 % Proof 1 at 2.82 (+ 0.89) seconds.
% 30.96/4.42 % Length of proof is 38.
% 30.96/4.42 % Level of proof is 14.
% 30.96/4.42 % Maximum clause weight is 102.000.
% 30.96/4.42 % Given clauses 469.
% 30.96/4.42
% 30.96/4.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------