%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL042-1 : TPTP v9.3.1. Released v1.0.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:49 AM UTC 2026
% Result : Unsatisfiable 50.32s 7.80s
% Output : CNFRefutation 50.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 7
% Syntax : Number of formulae : 39 ( 25 unt; 0 def)
% Number of atoms : 55 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 18 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 104 ( 8 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(condensed_detachment,axiom,
! [VAR_0,VAR_1] :
( is_a_theorem(VAR_1)
| ~ is_a_theorem(VAR_0)
| ~ is_a_theorem(implies(VAR_0,VAR_1)) ),
file('theBenchmark.p',condensed_detachment) ).
cnf(c_1,plain,
( is_a_theorem(B)
| ~ is_a_theorem(A)
| ~ is_a_theorem(implies(A,B)) ),
inference(clausify,[status(thm)],[condensed_detachment]) ).
fof(cn_3,axiom,
! [VAR_0,VAR_1] : is_a_theorem(implies(VAR_0,implies(not(VAR_0),VAR_1))),
file('theBenchmark.p',cn_3) ).
cnf(c_2,plain,
is_a_theorem(implies(A,implies(not(A),B))),
inference(clausify,[status(thm)],[cn_3]) ).
fof(cn_18,axiom,
! [VAR_0,VAR_1] : is_a_theorem(implies(VAR_0,implies(VAR_1,VAR_0))),
file('theBenchmark.p',cn_18) ).
cnf(c_3,plain,
is_a_theorem(implies(A,implies(B,A))),
inference(clausify,[status(thm)],[cn_18]) ).
fof(cn_21,axiom,
! [VAR_0,VAR_1,VAR_2] : is_a_theorem(implies(implies(VAR_0,implies(VAR_1,VAR_2)),implies(VAR_1,implies(VAR_0,VAR_2)))),
file('theBenchmark.p',cn_21) ).
cnf(c_4,plain,
is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))),
inference(clausify,[status(thm)],[cn_21]) ).
fof(cn_22,axiom,
! [VAR_0,VAR_1,VAR_2] : is_a_theorem(implies(implies(VAR_0,VAR_1),implies(implies(VAR_2,VAR_0),implies(VAR_2,VAR_1)))),
file('theBenchmark.p',cn_22) ).
cnf(c_5,plain,
is_a_theorem(implies(implies(A,B),implies(implies(C,A),implies(C,B)))),
inference(clausify,[status(thm)],[cn_22]) ).
fof(cn_54,axiom,
! [VAR_0,VAR_1] : is_a_theorem(implies(implies(VAR_0,VAR_1),implies(implies(not(VAR_0),VAR_1),VAR_1))),
file('theBenchmark.p',cn_54) ).
cnf(c_6,plain,
is_a_theorem(implies(implies(A,B),implies(implies(not(A),B),B))),
inference(clausify,[status(thm)],[cn_54]) ).
fof(prove_cn_35,axiom,
~ is_a_theorem(implies(implies(a,implies(b,c)),implies(implies(a,b),implies(a,c)))),
file('theBenchmark.p',prove_cn_35) ).
cnf(c_7,plain,
~ is_a_theorem(implies(implies(a,implies(b,c)),implies(implies(a,b),implies(a,c)))),
inference(clausify,[status(thm)],[prove_cn_35]) ).
cnf(c_21265,plain,
( is_a_theorem(implies(B,implies(A,C)))
| ~ is_a_theorem(implies(A,implies(B,C))) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_16,plain,
is_a_theorem(implies(not(A),implies(A,B))),
inference(resolve,[status(thm)],[c_21265,c_2]) ).
cnf(c_21266,plain,
( is_a_theorem(implies(implies(C,A),implies(C,B)))
| ~ is_a_theorem(implies(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_17,plain,
is_a_theorem(implies(implies(A,implies(B,C)),implies(A,implies(implies(D,B),implies(D,C))))),
inference(resolve,[status(thm)],[c_21266,c_5]) ).
cnf(c_21267,plain,
( is_a_theorem(implies(B,implies(A,C)))
| ~ is_a_theorem(implies(A,implies(B,C))) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_18,plain,
is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))),
inference(resolve,[status(thm)],[c_21267,c_5]) ).
cnf(c_21268,plain,
( is_a_theorem(implies(implies(C,A),implies(C,B)))
| ~ is_a_theorem(implies(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_5]) ).
cnf(c_22,plain,
is_a_theorem(implies(implies(A,B),implies(A,implies(C,B)))),
inference(resolve,[status(thm)],[c_21268,c_3]) ).
cnf(c_21269,plain,
( is_a_theorem(implies(B,implies(A,C)))
| ~ is_a_theorem(implies(A,implies(B,C))) ),
inference(resolve,[status(thm)],[c_1,c_4]) ).
cnf(c_162,plain,
is_a_theorem(implies(A,implies(implies(A,B),implies(C,B)))),
inference(resolve,[status(thm)],[c_21269,c_22]) ).
cnf(c_21270,plain,
( is_a_theorem(implies(A,implies(implies(D,B),implies(D,C))))
| ~ is_a_theorem(implies(A,implies(B,C))) ),
inference(resolve,[status(thm)],[c_1,c_17]) ).
cnf(c_194,plain,
is_a_theorem(implies(not(A),implies(implies(B,A),implies(B,C)))),
inference(resolve,[status(thm)],[c_21270,c_16]) ).
cnf(c_21271,plain,
( is_a_theorem(implies(implies(B,C),implies(A,C)))
| ~ is_a_theorem(implies(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_18]) ).
cnf(c_219,plain,
is_a_theorem(implies(implies(implies(A,implies(B,C)),D),implies(implies(A,C),D))),
inference(resolve,[status(thm)],[c_21271,c_22]) ).
cnf(c_21272,plain,
( is_a_theorem(implies(implies(B,C),implies(A,C)))
| ~ is_a_theorem(implies(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_18]) ).
cnf(c_228,plain,
is_a_theorem(implies(implies(implies(A,implies(B,C)),D),implies(implies(B,implies(A,C)),D))),
inference(resolve,[status(thm)],[c_21272,c_4]) ).
cnf(c_21273,plain,
( is_a_theorem(implies(implies(not(A),B),B))
| ~ is_a_theorem(implies(A,B)) ),
inference(resolve,[status(thm)],[c_1,c_6]) ).
cnf(c_247,plain,
is_a_theorem(implies(implies(not(A),implies(implies(A,B),implies(C,B))),implies(implies(A,B),implies(C,B)))),
inference(resolve,[status(thm)],[c_21273,c_162]) ).
cnf(c_21274,plain,
( is_a_theorem(implies(implies(A,C),D))
| ~ is_a_theorem(implies(implies(A,implies(B,C)),D)) ),
inference(resolve,[status(thm)],[c_1,c_219]) ).
cnf(c_20993,plain,
is_a_theorem(implies(implies(not(A),implies(B,C)),implies(implies(A,C),implies(B,C)))),
inference(resolve,[status(thm)],[c_21274,c_247]) ).
cnf(c_21275,plain,
( is_a_theorem(implies(implies(A,C),implies(B,C)))
| ~ is_a_theorem(implies(not(A),implies(B,C))) ),
inference(resolve,[status(thm)],[c_1,c_20993]) ).
cnf(c_21177,plain,
is_a_theorem(implies(implies(A,implies(B,C)),implies(implies(B,A),implies(B,C)))),
inference(resolve,[status(thm)],[c_21275,c_194]) ).
cnf(c_21276,plain,
( is_a_theorem(implies(implies(B,implies(A,C)),D))
| ~ is_a_theorem(implies(implies(A,implies(B,C)),D)) ),
inference(resolve,[status(thm)],[c_1,c_228]) ).
cnf(c_21263,plain,
is_a_theorem(implies(implies(A,implies(B,C)),implies(implies(A,B),implies(A,C)))),
inference(resolve,[status(thm)],[c_21276,c_21177]) ).
cnf(c_21264,plain,
$false,
inference(resolve,[status(thm)],[c_21263,c_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL042-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.57 % Computer : n016.cluster.edu
% 0.14/0.57 % Model : x86_64 x86_64
% 0.14/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.57 % Memory : 8046.5625MB
% 0.14/0.57 % OS : Linux 6.8.0-71-generic
% 0.14/0.57 % CPULimit : 300
% 0.14/0.57 % WCLimit : 300
% 0.14/0.57 % DateTime : Fri Sep 25 21:50:45 UTC 2026
% 0.14/0.57 % CPUTime :
% 0.14/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/0.58 % Process 3378795 was started by sandbox2 on n016,
% 0.14/0.58 % Fri Sep 25 21:50:45 2026
% 0.14/0.58 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.58
% 0.14/0.58 % From the command line: assign(max_seconds, 300).
% 50.32/7.80
% 50.32/7.80 % given #500 (T,wt=37): 4731 is_a_theorem(implies(not(implies(A,not(B))),not(not(implies(C,B))))). [hyper(1,a,1395,a,b,1710,a)].
% 50.32/7.80
% 50.32/7.80 % SZS status Unsatisfiable for theBenchmark
% 50.32/7.80
% 50.32/7.80 % Proof 1 at 5.09 (+ 2.10) seconds.
% 50.32/7.80 % Length of proof is 20.
% 50.32/7.80 % Level of proof is 7.
% 50.32/7.80 % Maximum clause weight is 44.000.
% 50.32/7.80 % Given clauses 572.
% 50.32/7.80
% 50.32/7.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------