%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : REL045-2 : TPTP v9.3.1. Released v4.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 08:25:06 AM UTC 2026
% Result : Unsatisfiable 2.08s 0.75s
% Output : CNFRefutation 2.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 15
% Syntax : Number of formulae : 153 ( 153 unt; 0 def)
% Number of atoms : 153 ( 152 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 204 ( 14 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(maddux1_join_commutativity_1,axiom,
! [VAR_0,VAR_1] : join(VAR_0,VAR_1) = join(VAR_1,VAR_0),
file('theBenchmark.p',maddux1_join_commutativity_1) ).
cnf(c_1,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[maddux1_join_commutativity_1]) ).
fof(maddux2_join_associativity_2,axiom,
! [VAR_0,VAR_1,VAR_2] : join(VAR_0,join(VAR_1,VAR_2)) = join(join(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',maddux2_join_associativity_2) ).
cnf(c_2,plain,
join(A,join(B,C)) = join(join(A,B),C),
inference(clausify,[status(thm)],[maddux2_join_associativity_2]) ).
cnf(c_3,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_2]) ).
fof(maddux3_a_kind_of_de_Morgan_3,axiom,
! [VAR_0,VAR_1] : VAR_0 = join(complement(join(complement(VAR_0),complement(VAR_1))),complement(join(complement(VAR_0),VAR_1))),
file('theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
cnf(c_4,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(clausify,[status(thm)],[maddux3_a_kind_of_de_Morgan_3]) ).
cnf(c_710,plain,
A = join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_5,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_710]) ).
fof(maddux4_definiton_of_meet_4,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,VAR_1) = complement(join(complement(VAR_0),complement(VAR_1))),
file('theBenchmark.p',maddux4_definiton_of_meet_4) ).
cnf(c_6,plain,
meet(A,B) = complement(join(complement(A),complement(B))),
inference(clausify,[status(thm)],[maddux4_definiton_of_meet_4]) ).
fof(composition_associativity_5,axiom,
! [VAR_0,VAR_1,VAR_2] : composition(VAR_0,composition(VAR_1,VAR_2)) = composition(composition(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',composition_associativity_5) ).
cnf(c_7,plain,
composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(clausify,[status(thm)],[composition_associativity_5]) ).
cnf(c_8,plain,
composition(composition(A,B),C) = composition(A,composition(B,C)),
inference(copy,[status(thm)],[c_7]) ).
fof(composition_identity_6,axiom,
! [VAR_0] : composition(VAR_0,one) = VAR_0,
file('theBenchmark.p',composition_identity_6) ).
cnf(c_9,plain,
composition(A,one) = A,
inference(clausify,[status(thm)],[composition_identity_6]) ).
fof(composition_distributivity_7,axiom,
! [VAR_0,VAR_1,VAR_2] : composition(join(VAR_0,VAR_1),VAR_2) = join(composition(VAR_0,VAR_2),composition(VAR_1,VAR_2)),
file('theBenchmark.p',composition_distributivity_7) ).
cnf(c_10,plain,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(clausify,[status(thm)],[composition_distributivity_7]) ).
fof(converse_idempotence_8,axiom,
! [VAR_0] : converse(converse(VAR_0)) = VAR_0,
file('theBenchmark.p',converse_idempotence_8) ).
cnf(c_11,plain,
converse(converse(A)) = A,
inference(clausify,[status(thm)],[converse_idempotence_8]) ).
fof(converse_additivity_9,axiom,
! [VAR_0,VAR_1] : converse(join(VAR_0,VAR_1)) = join(converse(VAR_0),converse(VAR_1)),
file('theBenchmark.p',converse_additivity_9) ).
cnf(c_12,plain,
converse(join(A,B)) = join(converse(A),converse(B)),
inference(clausify,[status(thm)],[converse_additivity_9]) ).
fof(converse_multiplicativity_10,axiom,
! [VAR_0,VAR_1] : converse(composition(VAR_0,VAR_1)) = composition(converse(VAR_1),converse(VAR_0)),
file('theBenchmark.p',converse_multiplicativity_10) ).
cnf(c_13,plain,
converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(clausify,[status(thm)],[converse_multiplicativity_10]) ).
fof(converse_cancellativity_11,axiom,
! [VAR_0,VAR_1] : join(composition(converse(VAR_0),complement(composition(VAR_0,VAR_1))),complement(VAR_1)) = complement(VAR_1),
file('theBenchmark.p',converse_cancellativity_11) ).
cnf(c_14,plain,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(clausify,[status(thm)],[converse_cancellativity_11]) ).
cnf(c_15,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_14]) ).
fof(def_top_12,axiom,
! [VAR_0] : top = join(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_top_12) ).
cnf(c_16,plain,
top = join(A,complement(A)),
inference(clausify,[status(thm)],[def_top_12]) ).
cnf(c_17,plain,
join(A,complement(A)) = top,
inference(copy,[status(thm)],[c_16]) ).
fof(def_zero_13,axiom,
! [VAR_0] : zero = meet(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_zero_13) ).
cnf(c_18,plain,
zero = meet(A,complement(A)),
inference(clausify,[status(thm)],[def_zero_13]) ).
cnf(c_711,plain,
zero = complement(join(complement(A),complement(complement(A)))),
inference(paramod,[status(thm)],[c_6,c_18]) ).
cnf(c_712,plain,
zero = complement(top),
inference(paramod,[status(thm)],[c_17,c_711]) ).
cnf(c_19,plain,
complement(top) = zero,
inference(copy,[status(thm)],[c_712]) ).
fof(dedekind_law_14,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2)))) = composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2))),
file('theBenchmark.p',dedekind_law_14) ).
cnf(c_20,plain,
join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(clausify,[status(thm)],[dedekind_law_14]) ).
cnf(c_713,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_20]) ).
cnf(c_714,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_713]) ).
cnf(c_715,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_714]) ).
cnf(c_716,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(B))))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_715]) ).
cnf(c_21,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C))))),
inference(paramod,[status(thm)],[c_6,c_716]) ).
fof(goals_17,axiom,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1),
file('theBenchmark.p',goals_17) ).
cnf(c_26,plain,
join(sk1,composition(composition(sk1,converse(sk1)),sk1)) != composition(composition(sk1,converse(sk1)),sk1),
inference(clausify,[status(thm)],[goals_17]) ).
cnf(c_717,plain,
join(sk1,composition(sk1,composition(converse(sk1),sk1))) != composition(composition(sk1,converse(sk1)),sk1),
inference(paramod,[status(thm)],[c_8,c_26]) ).
cnf(c_27,plain,
join(sk1,composition(sk1,composition(converse(sk1),sk1))) != composition(sk1,composition(converse(sk1),sk1)),
inference(paramod,[status(thm)],[c_8,c_717]) ).
cnf(c_31,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_718,plain,
join(A,B) = join(complement(join(complement(A),C)),join(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_32,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_718]) ).
cnf(c_719,plain,
converse(A) = composition(converse(one),converse(A)),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_38,plain,
composition(converse(one),converse(A)) = converse(A),
inference(copy,[status(thm)],[c_719]) ).
cnf(c_720,plain,
join(complement(A),composition(converse(composition(B,C)),complement(composition(B,composition(C,A))))) = complement(A),
inference(paramod,[status(thm)],[c_8,c_15]) ).
cnf(c_721,plain,
join(complement(A),composition(composition(converse(C),converse(B)),complement(composition(B,composition(C,A))))) = complement(A),
inference(paramod,[status(thm)],[c_13,c_720]) ).
cnf(c_42,plain,
join(complement(A),composition(converse(B),composition(converse(C),complement(composition(C,composition(B,A)))))) = complement(A),
inference(paramod,[status(thm)],[c_8,c_721]) ).
cnf(c_722,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_17,c_5]) ).
cnf(c_50,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_19,c_722]) ).
cnf(c_723,plain,
join(complement(join(complement(A),complement(A))),complement(top)) = A,
inference(paramod,[status(thm)],[c_17,c_5]) ).
cnf(c_724,plain,
join(complement(join(complement(A),complement(A))),zero) = A,
inference(paramod,[status(thm)],[c_19,c_723]) ).
cnf(c_51,plain,
join(zero,complement(join(complement(A),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_724]) ).
cnf(c_725,plain,
converse(top) = join(converse(A),converse(complement(A))),
inference(paramod,[status(thm)],[c_17,c_12]) ).
cnf(c_53,plain,
join(converse(A),converse(complement(A))) = converse(top),
inference(copy,[status(thm)],[c_725]) ).
cnf(c_726,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = complement(top),
inference(paramod,[status(thm)],[c_19,c_15]) ).
cnf(c_56,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = zero,
inference(paramod,[status(thm)],[c_19,c_726]) ).
cnf(c_58,plain,
join(complement(join(complement(A),complement(composition(B,C)))),composition(complement(join(complement(B),complement(composition(A,converse(C))))),complement(join(complement(C),complement(composition(converse(B),A)))))) = composition(complement(join(complement(B),complement(composition(A,converse(C))))),complement(join(complement(C),complement(composition(converse(B),A))))),
inference(paramod,[status(thm)],[c_1,c_21]) ).
cnf(c_727,plain,
composition(converse(one),A) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_38]) ).
cnf(c_125,plain,
composition(converse(one),A) = A,
inference(paramod,[status(thm)],[c_11,c_727]) ).
cnf(c_728,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_125,c_9]) ).
cnf(c_134,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_728]) ).
cnf(c_138,plain,
join(complement(A),complement(composition(one,A))) = complement(A),
inference(paramod,[status(thm)],[c_125,c_15]) ).
cnf(c_156,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_134,c_125]) ).
cnf(c_161,plain,
join(complement(A),complement(A)) = complement(A),
inference(paramod,[status(thm)],[c_156,c_138]) ).
cnf(c_162,plain,
join(zero,complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_161,c_51]) ).
cnf(c_729,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_17,c_31]) ).
cnf(c_730,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_1,c_729]) ).
cnf(c_731,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_19,c_730]) ).
cnf(c_204,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_731]) ).
cnf(c_212,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_204,c_50]) ).
cnf(c_225,plain,
join(zero,A) = A,
inference(paramod,[status(thm)],[c_212,c_162]) ).
cnf(c_238,plain,
composition(converse(A),complement(composition(A,top))) = zero,
inference(paramod,[status(thm)],[c_225,c_56]) ).
cnf(c_732,plain,
join(complement(join(A,B)),complement(join(complement(complement(A)),complement(B)))) = complement(A),
inference(paramod,[status(thm)],[c_212,c_5]) ).
cnf(c_240,plain,
join(complement(join(A,B)),complement(join(A,complement(B)))) = complement(A),
inference(paramod,[status(thm)],[c_212,c_732]) ).
cnf(c_733,plain,
join(A,complement(complement(A))) = complement(complement(A)),
inference(paramod,[status(thm)],[c_212,c_161]) ).
cnf(c_734,plain,
join(A,A) = complement(complement(A)),
inference(paramod,[status(thm)],[c_212,c_733]) ).
cnf(c_251,plain,
join(A,A) = A,
inference(paramod,[status(thm)],[c_212,c_734]) ).
cnf(c_735,plain,
join(A,B) = join(A,join(A,B)),
inference(paramod,[status(thm)],[c_251,c_3]) ).
cnf(c_263,plain,
join(A,join(A,B)) = join(A,B),
inference(copy,[status(thm)],[c_735]) ).
cnf(c_736,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_251,c_32]) ).
cnf(c_737,plain,
complement(complement(A)) = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_240,c_736]) ).
cnf(c_738,plain,
A = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_212,c_737]) ).
cnf(c_285,plain,
join(A,complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_738]) ).
cnf(c_739,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),A)) = A,
inference(paramod,[status(thm)],[c_251,c_32]) ).
cnf(c_740,plain,
join(complement(join(complement(A),B)),join(A,complement(join(complement(A),complement(B))))) = A,
inference(paramod,[status(thm)],[c_1,c_739]) ).
cnf(c_741,plain,
join(complement(join(complement(A),B)),A) = A,
inference(paramod,[status(thm)],[c_285,c_740]) ).
cnf(c_286,plain,
join(A,complement(join(complement(A),B))) = A,
inference(paramod,[status(thm)],[c_1,c_741]) ).
cnf(c_330,plain,
join(one,converse(complement(one))) = converse(top),
inference(paramod,[status(thm)],[c_134,c_53]) ).
cnf(c_742,plain,
join(A,top) = join(A,complement(A)),
inference(paramod,[status(thm)],[c_17,c_263]) ).
cnf(c_366,plain,
join(A,top) = top,
inference(paramod,[status(thm)],[c_17,c_742]) ).
cnf(c_743,plain,
join(converse(A),converse(top)) = join(converse(A),converse(complement(A))),
inference(paramod,[status(thm)],[c_53,c_263]) ).
cnf(c_367,plain,
join(converse(A),converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_53,c_743]) ).
cnf(c_744,plain,
join(one,converse(top)) = join(one,converse(complement(one))),
inference(paramod,[status(thm)],[c_330,c_263]) ).
cnf(c_368,plain,
join(one,converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_330,c_744]) ).
cnf(c_745,plain,
top = join(top,A),
inference(paramod,[status(thm)],[c_366,c_1]) ).
cnf(c_370,plain,
join(top,A) = top,
inference(copy,[status(thm)],[c_745]) ).
cnf(c_746,plain,
composition(converse(top),A) = join(composition(one,A),composition(converse(top),A)),
inference(paramod,[status(thm)],[c_368,c_10]) ).
cnf(c_747,plain,
composition(converse(top),A) = join(A,composition(converse(top),A)),
inference(paramod,[status(thm)],[c_156,c_746]) ).
cnf(c_398,plain,
join(A,composition(converse(top),A)) = composition(converse(top),A),
inference(copy,[status(thm)],[c_747]) ).
cnf(c_402,plain,
join(A,converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_11,c_367]) ).
cnf(c_407,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_402,c_370]) ).
cnf(c_748,plain,
join(A,composition(top,A)) = composition(converse(top),A),
inference(paramod,[status(thm)],[c_407,c_398]) ).
cnf(c_412,plain,
join(A,composition(top,A)) = composition(top,A),
inference(paramod,[status(thm)],[c_407,c_748]) ).
cnf(c_426,plain,
composition(top,complement(composition(top,top))) = zero,
inference(paramod,[status(thm)],[c_407,c_238]) ).
cnf(c_749,plain,
composition(join(top,A),complement(composition(top,top))) = join(zero,composition(A,complement(composition(top,top)))),
inference(paramod,[status(thm)],[c_426,c_10]) ).
cnf(c_750,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(A,complement(composition(top,top)))),
inference(paramod,[status(thm)],[c_370,c_749]) ).
cnf(c_751,plain,
zero = join(zero,composition(A,complement(composition(top,top)))),
inference(paramod,[status(thm)],[c_426,c_750]) ).
cnf(c_752,plain,
zero = composition(A,complement(composition(top,top))),
inference(paramod,[status(thm)],[c_225,c_751]) ).
cnf(c_472,plain,
composition(A,complement(composition(top,top))) = zero,
inference(copy,[status(thm)],[c_752]) ).
cnf(c_753,plain,
zero = complement(composition(top,top)),
inference(paramod,[status(thm)],[c_472,c_156]) ).
cnf(c_484,plain,
complement(composition(top,top)) = zero,
inference(copy,[status(thm)],[c_753]) ).
cnf(c_754,plain,
join(composition(top,top),zero) = top,
inference(paramod,[status(thm)],[c_484,c_17]) ).
cnf(c_755,plain,
join(zero,composition(top,top)) = top,
inference(paramod,[status(thm)],[c_1,c_754]) ).
cnf(c_500,plain,
composition(top,top) = top,
inference(paramod,[status(thm)],[c_225,c_755]) ).
cnf(c_756,plain,
composition(top,A) = composition(top,composition(top,A)),
inference(paramod,[status(thm)],[c_500,c_8]) ).
cnf(c_504,plain,
composition(top,composition(top,A)) = composition(top,A),
inference(copy,[status(thm)],[c_756]) ).
cnf(c_579,plain,
join(A,complement(composition(top,complement(A)))) = A,
inference(paramod,[status(thm)],[c_412,c_286]) ).
cnf(c_757,plain,
join(complement(composition(top,A)),composition(converse(top),complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_504,c_15]) ).
cnf(c_758,plain,
join(complement(composition(top,A)),composition(top,complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_407,c_757]) ).
cnf(c_598,plain,
composition(top,complement(composition(top,A))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_412,c_758]) ).
cnf(c_759,plain,
join(complement(A),composition(converse(top),composition(converse(top),complement(composition(top,A))))) = complement(A),
inference(paramod,[status(thm)],[c_504,c_42]) ).
cnf(c_760,plain,
join(complement(A),composition(top,composition(converse(top),complement(composition(top,A))))) = complement(A),
inference(paramod,[status(thm)],[c_407,c_759]) ).
cnf(c_761,plain,
join(complement(A),composition(top,composition(top,complement(composition(top,A))))) = complement(A),
inference(paramod,[status(thm)],[c_407,c_760]) ).
cnf(c_762,plain,
join(complement(A),composition(top,complement(composition(top,A)))) = complement(A),
inference(paramod,[status(thm)],[c_598,c_761]) ).
cnf(c_603,plain,
join(complement(A),complement(composition(top,A))) = complement(A),
inference(paramod,[status(thm)],[c_598,c_762]) ).
cnf(c_763,plain,
join(complement(complement(A)),composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_579,c_58]) ).
cnf(c_764,plain,
join(A,composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_763]) ).
cnf(c_765,plain,
join(A,composition(complement(join(zero,complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_19,c_764]) ).
cnf(c_766,plain,
join(A,composition(complement(join(zero,complement(composition(A,converse(A))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_765]) ).
cnf(c_767,plain,
join(A,composition(complement(complement(composition(A,converse(A)))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_225,c_766]) ).
cnf(c_768,plain,
join(A,composition(composition(A,converse(A)),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_767]) ).
cnf(c_769,plain,
join(A,composition(composition(A,converse(A)),complement(join(complement(A),complement(composition(converse(top),A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_768]) ).
cnf(c_770,plain,
join(A,composition(composition(A,converse(A)),complement(join(complement(A),complement(composition(top,A)))))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_407,c_769]) ).
cnf(c_771,plain,
join(A,composition(composition(A,converse(A)),complement(complement(A)))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_603,c_770]) ).
cnf(c_772,plain,
join(A,composition(composition(A,converse(A)),A)) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_771]) ).
cnf(c_773,plain,
join(A,composition(A,composition(converse(A),A))) = composition(complement(join(complement(top),complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_8,c_772]) ).
cnf(c_774,plain,
join(A,composition(A,composition(converse(A),A))) = composition(complement(join(zero,complement(composition(A,converse(complement(complement(A))))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_19,c_773]) ).
cnf(c_775,plain,
join(A,composition(A,composition(converse(A),A))) = composition(complement(join(zero,complement(composition(A,converse(A))))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_774]) ).
cnf(c_776,plain,
join(A,composition(A,composition(converse(A),A))) = composition(complement(complement(composition(A,converse(A)))),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_225,c_775]) ).
cnf(c_777,plain,
join(A,composition(A,composition(converse(A),A))) = composition(composition(A,converse(A)),complement(join(complement(complement(complement(A))),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_776]) ).
cnf(c_778,plain,
join(A,composition(A,composition(converse(A),A))) = composition(composition(A,converse(A)),complement(join(complement(A),complement(composition(converse(top),A))))),
inference(paramod,[status(thm)],[c_212,c_777]) ).
cnf(c_779,plain,
join(A,composition(A,composition(converse(A),A))) = composition(composition(A,converse(A)),complement(join(complement(A),complement(composition(top,A))))),
inference(paramod,[status(thm)],[c_407,c_778]) ).
cnf(c_780,plain,
join(A,composition(A,composition(converse(A),A))) = composition(composition(A,converse(A)),complement(complement(A))),
inference(paramod,[status(thm)],[c_603,c_779]) ).
cnf(c_781,plain,
join(A,composition(A,composition(converse(A),A))) = composition(composition(A,converse(A)),A),
inference(paramod,[status(thm)],[c_212,c_780]) ).
cnf(c_708,plain,
join(A,composition(A,composition(converse(A),A))) = composition(A,composition(converse(A),A)),
inference(paramod,[status(thm)],[c_8,c_781]) ).
cnf(c_709,plain,
$false,
inference(resolve,[status(thm)],[c_708,c_27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL045-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n015.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 05:44:58 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 3258584 was started by sandbox on n015,
% 0.18/0.45 % Sat Sep 26 05:44:58 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 2.08/0.75
% 2.08/0.75 % SZS status Unsatisfiable for theBenchmark
% 2.08/0.75
% 2.08/0.75 % Proof 1 at 0.20 (+ 0.07) seconds.
% 2.08/0.75 % Length of proof is 66.
% 2.08/0.75 % Level of proof is 19.
% 2.08/0.75 % Maximum clause weight is 48.000.
% 2.08/0.75 % Given clauses 93.
% 2.08/0.75
% 2.08/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------