%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL015-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 07:57:45 AM UTC 2026
% Result : Unsatisfiable 156.92s 21.64s
% Output : CNFRefutation 156.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 3
% Syntax : Number of formulae : 99 ( 51 unt; 0 def)
% Number of atoms : 149 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 102 ( 52 ~; 50 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 337 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(condensed_detachment,axiom,
! [VAR_0,VAR_1] :
( is_a_theorem(VAR_1)
| ~ is_a_theorem(VAR_0)
| ~ is_a_theorem(equivalent(VAR_0,VAR_1)) ),
file('theBenchmark.p',condensed_detachment) ).
cnf(c_1,plain,
( is_a_theorem(B)
| ~ is_a_theorem(A)
| ~ is_a_theorem(equivalent(A,B)) ),
inference(clausify,[status(thm)],[condensed_detachment]) ).
fof(yrm,axiom,
! [VAR_0,VAR_1,VAR_2] : is_a_theorem(equivalent(equivalent(VAR_0,VAR_1),equivalent(VAR_2,equivalent(equivalent(VAR_1,VAR_2),VAR_0)))),
file('theBenchmark.p',yrm) ).
cnf(c_2,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(C,equivalent(equivalent(B,C),A)))),
inference(clausify,[status(thm)],[yrm]) ).
fof(prove_wn,axiom,
~ is_a_theorem(equivalent(equivalent(a,equivalent(b,c)),equivalent(c,equivalent(a,b)))),
file('theBenchmark.p',prove_wn) ).
cnf(c_3,plain,
~ is_a_theorem(equivalent(equivalent(a,equivalent(b,c)),equivalent(c,equivalent(a,b)))),
inference(clausify,[status(thm)],[prove_wn]) ).
cnf(c_38663,plain,
( is_a_theorem(equivalent(C,equivalent(equivalent(B,C),A)))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_4,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(equivalent(C,B),D)),A),equivalent(D,C)))),
inference(resolve,[status(thm)],[c_38663,c_2]) ).
cnf(c_38664,plain,
( is_a_theorem(equivalent(equivalent(equivalent(B,equivalent(equivalent(C,B),D)),A),equivalent(D,C)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_5,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(D,equivalent(equivalent(equivalent(E,equivalent(equivalent(F,E),V6)),D),equivalent(V6,F)))),equivalent(C,B))),
inference(resolve,[status(thm)],[c_38664,c_4]) ).
cnf(c_38665,plain,
( is_a_theorem(equivalent(equivalent(equivalent(B,equivalent(equivalent(C,B),D)),A),equivalent(D,C)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_7,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(D,E),equivalent(F,equivalent(equivalent(E,F),D)))),equivalent(C,B))),
inference(resolve,[status(thm)],[c_38665,c_2]) ).
cnf(c_38666,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(D,E),equivalent(F,equivalent(equivalent(E,F),D))))) ),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_13,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(equivalent(equivalent(C,equivalent(equivalent(D,C),E)),B),equivalent(E,D))),A),F)),F)),
inference(resolve,[status(thm)],[c_38666,c_7]) ).
cnf(c_38667,plain,
( is_a_theorem(F)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(equivalent(equivalent(C,equivalent(equivalent(D,C),E)),B),equivalent(E,D))),A),F))) ),
inference(resolve,[status(thm)],[c_1,c_13]) ).
cnf(c_30,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,equivalent(equivalent(equivalent(C,equivalent(equivalent(D,C),E)),B),equivalent(E,D))),equivalent(F,A))),F)),
inference(resolve,[status(thm)],[c_38667,c_2]) ).
cnf(c_38668,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(D,equivalent(equivalent(equivalent(E,equivalent(equivalent(F,E),V6)),D),equivalent(V6,F))))) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_39,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(B,equivalent(C,A))),C),B)),
inference(resolve,[status(thm)],[c_38668,c_2]) ).
cnf(c_38669,plain,
( is_a_theorem(equivalent(equivalent(equivalent(B,equivalent(equivalent(C,B),D)),A),equivalent(D,C)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_42,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(equivalent(D,equivalent(E,equivalent(F,D))),F),E)),equivalent(C,B))),
inference(resolve,[status(thm)],[c_38669,c_39]) ).
cnf(c_38670,plain,
( is_a_theorem(equivalent(C,equivalent(equivalent(B,C),A)))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_43,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(B,A),equivalent(equivalent(C,equivalent(B,equivalent(D,C))),D)))),
inference(resolve,[status(thm)],[c_38670,c_39]) ).
cnf(c_38671,plain,
( is_a_theorem(equivalent(equivalent(B,A),equivalent(equivalent(C,equivalent(B,equivalent(D,C))),D)))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_43]) ).
cnf(c_49,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(C,equivalent(D,B))),D),C)),equivalent(equivalent(E,equivalent(A,equivalent(F,E))),F))),
inference(resolve,[status(thm)],[c_38671,c_39]) ).
cnf(c_38672,plain,
( is_a_theorem(B)
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,A))),C)) ),
inference(resolve,[status(thm)],[c_1,c_39]) ).
cnf(c_114,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,C),equivalent(D,equivalent(equivalent(C,D),B))),equivalent(E,A))),E)),
inference(resolve,[status(thm)],[c_38672,c_42]) ).
cnf(c_38673,plain,
( is_a_theorem(E)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,C),equivalent(D,equivalent(equivalent(C,D),B))),equivalent(E,A)))) ),
inference(resolve,[status(thm)],[c_1,c_114]) ).
cnf(c_136,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(D,equivalent(equivalent(C,D),B)),A)))),
inference(resolve,[status(thm)],[c_38673,c_43]) ).
cnf(c_38674,plain,
( is_a_theorem(B)
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,A))),C)) ),
inference(resolve,[status(thm)],[c_1,c_39]) ).
cnf(c_211,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,equivalent(C,equivalent(D,B))),D),C),equivalent(E,A))),E)),
inference(resolve,[status(thm)],[c_38674,c_49]) ).
cnf(c_38675,plain,
( is_a_theorem(E)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,equivalent(C,equivalent(D,B))),D),C),equivalent(E,A)))) ),
inference(resolve,[status(thm)],[c_1,c_211]) ).
cnf(c_239,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(C,equivalent(D,B))),D),equivalent(C,A)))),
inference(resolve,[status(thm)],[c_38675,c_43]) ).
cnf(c_38676,plain,
( is_a_theorem(F)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,equivalent(equivalent(equivalent(C,equivalent(equivalent(D,C),E)),B),equivalent(E,D))),A),F))) ),
inference(resolve,[status(thm)],[c_1,c_13]) ).
cnf(c_246,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),B),C)),
inference(resolve,[status(thm)],[c_38676,c_239]) ).
cnf(c_38677,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(D,E),equivalent(F,equivalent(equivalent(E,F),D))))) ),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_248,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,equivalent(B,A)))),C)),
inference(resolve,[status(thm)],[c_38677,c_239]) ).
cnf(c_38678,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),B)) ),
inference(resolve,[status(thm)],[c_1,c_246]) ).
cnf(c_300,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(A,B),B))),
inference(resolve,[status(thm)],[c_38678,c_248]) ).
cnf(c_38679,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(equivalent(D,equivalent(E,equivalent(F,D))),F),E))) ),
inference(resolve,[status(thm)],[c_1,c_42]) ).
cnf(c_325,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),B),A)),
inference(resolve,[status(thm)],[c_38679,c_300]) ).
cnf(c_38680,plain,
( is_a_theorem(F)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(B,equivalent(equivalent(equivalent(C,equivalent(equivalent(D,C),E)),B),equivalent(E,D))),equivalent(F,A)))) ),
inference(resolve,[status(thm)],[c_1,c_30]) ).
cnf(c_326,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(C,B))),
inference(resolve,[status(thm)],[c_38680,c_300]) ).
cnf(c_38681,plain,
( is_a_theorem(equivalent(C,equivalent(equivalent(B,C),A)))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_330,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,C),C),A),B))),
inference(resolve,[status(thm)],[c_38681,c_300]) ).
cnf(c_38682,plain,
( is_a_theorem(equivalent(equivalent(A,B),B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_300]) ).
cnf(c_356,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),B),A),C),C)),
inference(resolve,[status(thm)],[c_38682,c_325]) ).
cnf(c_38683,plain,
( is_a_theorem(A)
| ~ is_a_theorem(equivalent(equivalent(A,B),B)) ),
inference(resolve,[status(thm)],[c_1,c_325]) ).
cnf(c_368,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(B,A),B))),
inference(resolve,[status(thm)],[c_38683,c_246]) ).
cnf(c_38684,plain,
( is_a_theorem(equivalent(equivalent(A,B),B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_300]) ).
cnf(c_398,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),B)),C),C)),
inference(resolve,[status(thm)],[c_38684,c_368]) ).
cnf(c_38685,plain,
( is_a_theorem(equivalent(C,equivalent(equivalent(B,C),A)))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_408,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(equivalent(B,C),B),A),C))),
inference(resolve,[status(thm)],[c_38685,c_368]) ).
cnf(c_38686,plain,
( is_a_theorem(equivalent(equivalent(B,A),B))
| ~ is_a_theorem(A) ),
inference(resolve,[status(thm)],[c_1,c_368]) ).
cnf(c_410,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,C),C),B)),A)),
inference(resolve,[status(thm)],[c_38686,c_325]) ).
cnf(c_38687,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(B,A),C))) ),
inference(resolve,[status(thm)],[c_1,c_326]) ).
cnf(c_732,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(C,equivalent(A,equivalent(B,C))))),
inference(resolve,[status(thm)],[c_38687,c_239]) ).
cnf(c_38688,plain,
( is_a_theorem(A)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,C),C),B))) ),
inference(resolve,[status(thm)],[c_1,c_410]) ).
cnf(c_1133,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(B,A)),B)),
inference(resolve,[status(thm)],[c_38688,c_4]) ).
cnf(c_38689,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(D,equivalent(equivalent(equivalent(E,equivalent(equivalent(F,E),V6)),D),equivalent(V6,F))))) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_1157,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),D),equivalent(C,B)),D)),
inference(resolve,[status(thm)],[c_38689,c_1133]) ).
cnf(c_38690,plain,
( is_a_theorem(B)
| ~ is_a_theorem(equivalent(A,equivalent(B,A))) ),
inference(resolve,[status(thm)],[c_1,c_1133]) ).
cnf(c_1160,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),A),B)),
inference(resolve,[status(thm)],[c_38690,c_408]) ).
cnf(c_38691,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),B)),C)) ),
inference(resolve,[status(thm)],[c_1,c_398]) ).
cnf(c_4595,plain,
is_a_theorem(equivalent(A,equivalent(B,equivalent(equivalent(equivalent(C,B),C),A)))),
inference(resolve,[status(thm)],[c_38691,c_732]) ).
cnf(c_38692,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),B),A),C)) ),
inference(resolve,[status(thm)],[c_1,c_356]) ).
cnf(c_4599,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,C),C),equivalent(B,A)))),
inference(resolve,[status(thm)],[c_38692,c_732]) ).
cnf(c_38693,plain,
( is_a_theorem(equivalent(C,equivalent(A,equivalent(B,C))))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_732]) ).
cnf(c_4619,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,C),B),equivalent(C,A)))),
inference(resolve,[status(thm)],[c_38693,c_1160]) ).
cnf(c_38694,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(B,A),C))) ),
inference(resolve,[status(thm)],[c_1,c_326]) ).
cnf(c_15490,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(B,A))),
inference(resolve,[status(thm)],[c_38694,c_4619]) ).
cnf(c_38695,plain,
( is_a_theorem(equivalent(C,equivalent(A,equivalent(B,C))))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_732]) ).
cnf(c_15670,plain,
is_a_theorem(equivalent(A,equivalent(equivalent(B,C),equivalent(equivalent(C,B),A)))),
inference(resolve,[status(thm)],[c_38695,c_15490]) ).
cnf(c_38696,plain,
( is_a_theorem(equivalent(B,A))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_15490]) ).
cnf(c_15710,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),B),equivalent(A,C)),C)),
inference(resolve,[status(thm)],[c_38696,c_4599]) ).
cnf(c_38697,plain,
( is_a_theorem(equivalent(B,A))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_15490]) ).
cnf(c_15711,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(equivalent(B,A),B),C)),C)),
inference(resolve,[status(thm)],[c_38697,c_4595]) ).
cnf(c_38698,plain,
( is_a_theorem(equivalent(B,A))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_15490]) ).
cnf(c_15726,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,A))),equivalent(B,C))),
inference(resolve,[status(thm)],[c_38698,c_732]) ).
cnf(c_38699,plain,
( is_a_theorem(equivalent(B,A))
| ~ is_a_theorem(equivalent(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_15490]) ).
cnf(c_15736,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(A,B),B),C),A),C)),
inference(resolve,[status(thm)],[c_38699,c_330]) ).
cnf(c_38700,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(equivalent(equivalent(A,B),B),equivalent(A,C))) ),
inference(resolve,[status(thm)],[c_1,c_15710]) ).
cnf(c_17762,plain,
is_a_theorem(equivalent(equivalent(A,B),equivalent(equivalent(equivalent(B,A),C),C))),
inference(resolve,[status(thm)],[c_38700,c_15670]) ).
cnf(c_38701,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(B,A),B),C))) ),
inference(resolve,[status(thm)],[c_1,c_15711]) ).
cnf(c_17790,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),equivalent(B,C))),C)),
inference(resolve,[status(thm)],[c_38701,c_136]) ).
cnf(c_38702,plain,
( is_a_theorem(equivalent(B,C))
| ~ is_a_theorem(equivalent(A,equivalent(B,equivalent(C,A)))) ),
inference(resolve,[status(thm)],[c_1,c_15726]) ).
cnf(c_18866,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(C,equivalent(B,A))),C)),
inference(resolve,[status(thm)],[c_38702,c_17762]) ).
cnf(c_38703,plain,
( is_a_theorem(C)
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),B),C),A)) ),
inference(resolve,[status(thm)],[c_1,c_15736]) ).
cnf(c_19083,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),C)),equivalent(A,B))),
inference(resolve,[status(thm)],[c_38703,c_17790]) ).
cnf(c_38704,plain,
( is_a_theorem(equivalent(C,B))
| ~ is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),equivalent(equivalent(D,E),equivalent(F,equivalent(equivalent(E,F),D))))) ),
inference(resolve,[status(thm)],[c_1,c_7]) ).
cnf(c_20364,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,B),C),B),equivalent(C,A))),
inference(resolve,[status(thm)],[c_38704,c_18866]) ).
cnf(c_38705,plain,
( is_a_theorem(equivalent(A,B))
| ~ is_a_theorem(equivalent(A,equivalent(equivalent(B,C),C))) ),
inference(resolve,[status(thm)],[c_1,c_19083]) ).
cnf(c_20610,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(equivalent(B,C),equivalent(C,A))),B)),
inference(resolve,[status(thm)],[c_38705,c_15726]) ).
cnf(c_38706,plain,
( is_a_theorem(equivalent(C,A))
| ~ is_a_theorem(equivalent(equivalent(equivalent(A,B),C),B)) ),
inference(resolve,[status(thm)],[c_1,c_20364]) ).
cnf(c_27940,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),equivalent(B,equivalent(C,A))),C)),
inference(resolve,[status(thm)],[c_38706,c_20610]) ).
cnf(c_38707,plain,
( is_a_theorem(D)
| ~ is_a_theorem(equivalent(equivalent(equivalent(A,equivalent(equivalent(B,A),C)),D),equivalent(C,B))) ),
inference(resolve,[status(thm)],[c_1,c_1157]) ).
cnf(c_38357,plain,
is_a_theorem(equivalent(equivalent(equivalent(A,B),C),equivalent(equivalent(C,A),B))),
inference(resolve,[status(thm)],[c_38707,c_27940]) ).
cnf(c_38708,plain,
( is_a_theorem(equivalent(equivalent(C,A),B))
| ~ is_a_theorem(equivalent(equivalent(A,B),C)) ),
inference(resolve,[status(thm)],[c_1,c_38357]) ).
cnf(c_38661,plain,
is_a_theorem(equivalent(equivalent(A,equivalent(B,C)),equivalent(C,equivalent(A,B)))),
inference(resolve,[status(thm)],[c_38708,c_27940]) ).
cnf(c_38662,plain,
$false,
inference(resolve,[status(thm)],[c_38661,c_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL015-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.58 % Computer : n015.cluster.edu
% 0.12/0.58 % Model : x86_64 x86_64
% 0.12/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.58 % Memory : 8046.5625MB
% 0.12/0.58 % OS : Linux 6.8.0-71-generic
% 0.12/0.58 % CPULimit : 300
% 0.12/0.58 % WCLimit : 300
% 0.12/0.58 % DateTime : Fri Sep 25 21:46:58 UTC 2026
% 0.12/0.58 % CPUTime :
% 0.12/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.58 % Process 2334892 was started by sandbox on n015,
% 0.12/0.58 % Fri Sep 25 21:46:58 2026
% 0.12/0.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.58
% 0.12/0.58 % From the command line: assign(max_seconds, 300).
% 156.92/21.64
% 156.92/21.64 % given #500 (T,wt=12): 19093 is_a_theorem(equivalent(equivalent(A,equivalent(B,equivalent(C,B))),equivalent(A,C))). [hyper(1,a,15721,a,b,17790,a)].
% 156.92/21.64
% 156.92/21.64 % SZS status Unsatisfiable for theBenchmark
% 156.92/21.64
% 156.92/21.64 % Proof 1 at 15.88 (+ 4.80) seconds.
% 156.92/21.64 % Length of proof is 50.
% 156.92/21.64 % Level of proof is 24.
% 156.92/21.64 % Maximum clause weight is 28.000.
% 156.92/21.64 % Given clauses 827.
% 156.92/21.64
% 156.92/21.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------