%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT002-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 : n018.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:49:30 AM UTC 2026
% Result : Unsatisfiable 149.45s 20.55s
% Output : CNFRefutation 149.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 18
% Syntax : Number of formulae : 176 ( 166 unt; 0 def)
% Number of atoms : 188 ( 174 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 30 ( 18 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 402 ( 39 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(idempotence_of_meet,axiom,
! [VAR_0] : meet(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',idempotence_of_meet) ).
cnf(c_1,plain,
meet(A,A) = A,
inference(clausify,[status(thm)],[idempotence_of_meet]) ).
fof(idempotence_of_join,axiom,
! [VAR_0] : join(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',idempotence_of_join) ).
cnf(c_2,plain,
join(A,A) = A,
inference(clausify,[status(thm)],[idempotence_of_join]) ).
fof(absorption1,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,join(VAR_0,VAR_1)) = VAR_0,
file('theBenchmark.p',absorption1) ).
cnf(c_3,plain,
meet(A,join(A,B)) = A,
inference(clausify,[status(thm)],[absorption1]) ).
fof(absorption2,axiom,
! [VAR_0,VAR_1] : join(VAR_0,meet(VAR_0,VAR_1)) = VAR_0,
file('theBenchmark.p',absorption2) ).
cnf(c_4,plain,
join(A,meet(A,B)) = A,
inference(clausify,[status(thm)],[absorption2]) ).
fof(commutativity_of_meet,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,VAR_1) = meet(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_meet) ).
cnf(c_5,plain,
meet(A,B) = meet(B,A),
inference(clausify,[status(thm)],[commutativity_of_meet]) ).
fof(commutativity_of_join,axiom,
! [VAR_0,VAR_1] : join(VAR_0,VAR_1) = join(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_join) ).
cnf(c_6,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[commutativity_of_join]) ).
fof(associativity_of_meet,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(meet(VAR_0,VAR_1),VAR_2) = meet(VAR_0,meet(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_meet) ).
cnf(c_7,plain,
meet(meet(A,B),C) = meet(A,meet(B,C)),
inference(clausify,[status(thm)],[associativity_of_meet]) ).
fof(associativity_of_join,axiom,
! [VAR_0,VAR_1,VAR_2] : join(join(VAR_0,VAR_1),VAR_2) = join(VAR_0,join(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_join) ).
cnf(c_8,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(clausify,[status(thm)],[associativity_of_join]) ).
fof(x_meet_0,axiom,
! [VAR_0] : meet(VAR_0,n0) = n0,
file('theBenchmark.p',x_meet_0) ).
cnf(c_9,plain,
meet(A,n0) = n0,
inference(clausify,[status(thm)],[x_meet_0]) ).
fof(x_join_0,axiom,
! [VAR_0] : join(VAR_0,n0) = VAR_0,
file('theBenchmark.p',x_join_0) ).
cnf(c_10,plain,
join(A,n0) = A,
inference(clausify,[status(thm)],[x_join_0]) ).
fof(x_meet_1,axiom,
! [VAR_0] : meet(VAR_0,n1) = VAR_0,
file('theBenchmark.p',x_meet_1) ).
cnf(c_11,plain,
meet(A,n1) = A,
inference(clausify,[status(thm)],[x_meet_1]) ).
fof(modular,axiom,
! [VAR_0,VAR_1,VAR_2] :
( meet(VAR_1,join(VAR_0,VAR_2)) = join(VAR_0,meet(VAR_2,VAR_1))
| meet(VAR_0,VAR_1) != VAR_0 ),
file('theBenchmark.p',modular) ).
cnf(c_13,plain,
( meet(B,join(A,C)) = join(A,meet(C,B))
| meet(A,B) != A ),
inference(clausify,[status(thm)],[modular]) ).
cnf(c_14,plain,
( join(A,meet(C,B)) = meet(B,join(A,C))
| meet(A,B) != A ),
inference(copy,[status(thm)],[c_13]) ).
fof(complement_meet,axiom,
! [VAR_0,VAR_1] :
( meet(VAR_0,VAR_1) = n0
| ~ complement(VAR_0,VAR_1) ),
file('theBenchmark.p',complement_meet) ).
cnf(c_15,plain,
( meet(A,B) = n0
| ~ complement(A,B) ),
inference(clausify,[status(thm)],[complement_meet]) ).
fof(complement_join,axiom,
! [VAR_0,VAR_1] :
( join(VAR_0,VAR_1) = n1
| ~ complement(VAR_0,VAR_1) ),
file('theBenchmark.p',complement_join) ).
cnf(c_16,plain,
( join(A,B) = n1
| ~ complement(A,B) ),
inference(clausify,[status(thm)],[complement_join]) ).
fof(meet_join_complement,axiom,
! [VAR_0,VAR_1] :
( complement(VAR_0,VAR_1)
| join(VAR_0,VAR_1) != n1
| meet(VAR_0,VAR_1) != n0 ),
file('theBenchmark.p',meet_join_complement) ).
cnf(c_17,plain,
( complement(A,B)
| join(A,B) != n1
| meet(A,B) != n0 ),
inference(clausify,[status(thm)],[meet_join_complement]) ).
fof(complement_of_a_join_b,axiom,
complement(r1,join(a,b)),
file('theBenchmark.p',complement_of_a_join_b) ).
cnf(c_18,plain,
complement(r1,join(a,b)),
inference(clausify,[status(thm)],[complement_of_a_join_b]) ).
fof(complement_of_a_meet_b,axiom,
complement(r2,meet(a,b)),
file('theBenchmark.p',complement_of_a_meet_b) ).
cnf(c_19,plain,
complement(r2,meet(a,b)),
inference(clausify,[status(thm)],[complement_of_a_meet_b]) ).
fof(prove_complememt_exists,axiom,
! [VAR_0] : ~ complement(a,VAR_0),
file('theBenchmark.p',prove_complememt_exists) ).
cnf(c_20,plain,
~ complement(a,A),
inference(clausify,[status(thm)],[prove_complememt_exists]) ).
cnf(c_21,plain,
join(A,meet(B,A)) = A,
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_22,plain,
meet(A,join(B,A)) = A,
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_5871,plain,
meet(A,B) = meet(A,meet(A,B)),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_24,plain,
meet(A,meet(A,B)) = meet(A,B),
inference(copy,[status(thm)],[c_5871]) ).
cnf(c_5872,plain,
meet(A,B) = meet(A,meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_27,plain,
meet(A,meet(join(A,B),C)) = meet(A,C),
inference(copy,[status(thm)],[c_5872]) ).
cnf(c_28,plain,
join(meet(A,B),meet(A,meet(B,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_5873,plain,
meet(meet(A,B),C) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_30,plain,
meet(A,meet(B,C)) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_7,c_5873]) ).
cnf(c_5874,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_33,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_6,c_5874]) ).
cnf(c_34,plain,
meet(join(A,B),join(A,join(B,C))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_3]) ).
cnf(c_5875,plain,
join(A,B) = join(A,join(meet(A,C),B)),
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_36,plain,
join(A,join(meet(A,B),C)) = join(A,C),
inference(copy,[status(thm)],[c_5875]) ).
cnf(c_5876,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_38,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_8,c_5876]) ).
cnf(c_5877,plain,
A = join(n0,A),
inference(paramod,[status(thm)],[c_10,c_6]) ).
cnf(c_40,plain,
join(n0,A) = A,
inference(copy,[status(thm)],[c_5877]) ).
cnf(c_5878,plain,
A = meet(n1,A),
inference(paramod,[status(thm)],[c_11,c_5]) ).
cnf(c_41,plain,
meet(n1,A) = A,
inference(copy,[status(thm)],[c_5878]) ).
cnf(c_43,plain,
join(A,meet(B,join(A,C))) = meet(join(A,C),join(A,B)),
inference(resolve,[status(thm)],[c_14,c_3]) ).
cnf(c_5879,plain,
join(r1,join(a,b)) = n1,
inference(resolve,[status(thm)],[c_18,c_16]) ).
cnf(c_5880,plain,
join(a,join(r1,b)) = n1,
inference(paramod,[status(thm)],[c_38,c_5879]) ).
cnf(c_51,plain,
join(a,join(b,r1)) = n1,
inference(paramod,[status(thm)],[c_6,c_5880]) ).
cnf(c_52,plain,
meet(r1,join(a,b)) = n0,
inference(resolve,[status(thm)],[c_18,c_15]) ).
cnf(c_53,plain,
join(r2,meet(a,b)) = n1,
inference(resolve,[status(thm)],[c_19,c_16]) ).
cnf(c_5881,plain,
meet(r2,meet(a,b)) = n0,
inference(resolve,[status(thm)],[c_19,c_15]) ).
cnf(c_5882,plain,
meet(a,meet(r2,b)) = n0,
inference(paramod,[status(thm)],[c_30,c_5881]) ).
cnf(c_54,plain,
meet(a,meet(b,r2)) = n0,
inference(paramod,[status(thm)],[c_5,c_5882]) ).
cnf(c_60,plain,
join(A,meet(B,join(C,A))) = meet(join(C,A),join(A,B)),
inference(resolve,[status(thm)],[c_22,c_14]) ).
cnf(c_5883,plain,
meet(A,B) = meet(A,meet(join(C,A),B)),
inference(paramod,[status(thm)],[c_22,c_7]) ).
cnf(c_61,plain,
meet(A,meet(join(B,A),C)) = meet(A,C),
inference(copy,[status(thm)],[c_5883]) ).
cnf(c_5884,plain,
meet(meet(A,B),meet(B,C)) = meet(A,meet(B,C)),
inference(paramod,[status(thm)],[c_24,c_7]) ).
cnf(c_5885,plain,
meet(B,meet(meet(A,B),C)) = meet(A,meet(B,C)),
inference(paramod,[status(thm)],[c_30,c_5884]) ).
cnf(c_66,plain,
meet(A,meet(B,meet(A,C))) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_7,c_5885]) ).
cnf(c_72,plain,
meet(A,meet(B,join(A,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_27]) ).
cnf(c_5886,plain,
join(meet(A,B),meet(meet(B,C),A)) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_28]) ).
cnf(c_87,plain,
join(meet(A,B),meet(B,meet(C,A))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_5886]) ).
cnf(c_5887,plain,
meet(A,n0) = meet(r1,meet(A,join(a,b))),
inference(paramod,[status(thm)],[c_52,c_30]) ).
cnf(c_5888,plain,
n0 = meet(r1,meet(A,join(a,b))),
inference(paramod,[status(thm)],[c_9,c_5887]) ).
cnf(c_96,plain,
meet(r1,meet(A,join(a,b))) = n0,
inference(copy,[status(thm)],[c_5888]) ).
cnf(c_5889,plain,
join(A,join(B,join(C,A))) = join(join(B,C),A),
inference(paramod,[status(thm)],[c_8,c_33]) ).
cnf(c_112,plain,
join(A,join(B,join(C,A))) = join(B,join(C,A)),
inference(paramod,[status(thm)],[c_8,c_5889]) ).
cnf(c_161,plain,
join(A,join(B,meet(A,C))) = join(A,B),
inference(paramod,[status(thm)],[c_6,c_36]) ).
cnf(c_5890,plain,
meet(join(meet(A,B),C),join(A,C)) = join(meet(A,B),C),
inference(paramod,[status(thm)],[c_36,c_22]) ).
cnf(c_162,plain,
meet(join(A,B),join(meet(A,C),B)) = join(meet(A,C),B),
inference(paramod,[status(thm)],[c_5,c_5890]) ).
cnf(c_5891,plain,
join(A,join(meet(A,B),join(C,A))) = join(C,A),
inference(paramod,[status(thm)],[c_33,c_36]) ).
cnf(c_165,plain,
join(meet(A,B),join(C,A)) = join(C,A),
inference(paramod,[status(thm)],[c_112,c_5891]) ).
cnf(c_202,plain,
join(A,meet(join(A,B),C)) = meet(join(A,B),join(A,C)),
inference(paramod,[status(thm)],[c_5,c_43]) ).
cnf(c_203,plain,
join(A,meet(B,meet(C,join(A,D)))) = meet(join(A,D),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_7,c_43]) ).
cnf(c_242,plain,
meet(join(meet(A,B),C),join(C,A)) = join(meet(A,B),C),
inference(paramod,[status(thm)],[c_165,c_34]) ).
cnf(c_5892,plain,
join(meet(A,B),meet(C,join(D,A))) = meet(join(meet(A,B),join(D,A)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_165,c_43]) ).
cnf(c_247,plain,
join(meet(A,B),meet(C,join(D,A))) = meet(join(D,A),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_165,c_5892]) ).
cnf(c_5893,plain,
join(meet(A,B),meet(C,A)) = meet(join(A,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_60]) ).
cnf(c_264,plain,
join(meet(A,B),meet(C,A)) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_5893]) ).
cnf(c_265,plain,
join(A,meet(join(B,A),C)) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_5,c_60]) ).
cnf(c_5894,plain,
join(meet(A,B),meet(C,B)) = meet(join(B,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_21,c_60]) ).
cnf(c_270,plain,
join(meet(A,B),meet(C,B)) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_21,c_5894]) ).
cnf(c_5895,plain,
meet(join(A,join(B,meet(A,C))),join(B,meet(A,C))) = join(meet(A,C),join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_33,c_162]) ).
cnf(c_5896,plain,
meet(join(A,B),join(B,meet(A,C))) = join(meet(A,C),join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_161,c_5895]) ).
cnf(c_883,plain,
meet(join(A,B),join(B,meet(A,C))) = join(B,meet(A,C)),
inference(paramod,[status(thm)],[c_33,c_5896]) ).
cnf(c_5897,plain,
join(meet(A,B),meet(join(C,A),D)) = meet(join(meet(A,B),join(C,A)),join(meet(A,B),D)),
inference(paramod,[status(thm)],[c_165,c_202]) ).
cnf(c_998,plain,
join(meet(A,B),meet(join(C,A),D)) = meet(join(C,A),join(meet(A,B),D)),
inference(paramod,[status(thm)],[c_165,c_5897]) ).
cnf(c_5898,plain,
meet(r1,join(meet(b,A),a)) = n0,
inference(paramod,[status(thm)],[c_242,c_96]) ).
cnf(c_1172,plain,
meet(r1,join(a,meet(b,A))) = n0,
inference(paramod,[status(thm)],[c_6,c_5898]) ).
cnf(c_5899,plain,
join(n0,meet(join(a,meet(b,A)),meet(B,r1))) = meet(r1,join(a,meet(b,A))),
inference(paramod,[status(thm)],[c_1172,c_87]) ).
cnf(c_5900,plain,
meet(join(a,meet(b,A)),meet(B,r1)) = meet(r1,join(a,meet(b,A))),
inference(paramod,[status(thm)],[c_40,c_5899]) ).
cnf(c_1188,plain,
meet(join(a,meet(b,A)),meet(B,r1)) = n0,
inference(paramod,[status(thm)],[c_1172,c_5900]) ).
cnf(c_5901,plain,
join(meet(meet(join(A,B),C),D),meet(B,C)) = meet(meet(join(A,B),C),join(meet(meet(join(A,B),C),D),B)),
inference(paramod,[status(thm)],[c_61,c_264]) ).
cnf(c_5902,plain,
join(meet(join(A,B),meet(C,D)),meet(B,C)) = meet(meet(join(A,B),C),join(meet(meet(join(A,B),C),D),B)),
inference(paramod,[status(thm)],[c_7,c_5901]) ).
cnf(c_5903,plain,
join(meet(B,C),meet(join(A,B),meet(C,D))) = meet(meet(join(A,B),C),join(meet(meet(join(A,B),C),D),B)),
inference(paramod,[status(thm)],[c_6,c_5902]) ).
cnf(c_5904,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(meet(join(A,B),C),join(meet(meet(join(A,B),C),D),B)),
inference(paramod,[status(thm)],[c_998,c_5903]) ).
cnf(c_5905,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(meet(join(A,B),C),join(meet(join(A,B),meet(C,D)),B)),
inference(paramod,[status(thm)],[c_7,c_5904]) ).
cnf(c_5906,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(meet(join(A,B),C),join(B,meet(join(A,B),meet(C,D)))),
inference(paramod,[status(thm)],[c_6,c_5905]) ).
cnf(c_5907,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(meet(join(A,B),C),meet(join(A,B),join(B,meet(C,D)))),
inference(paramod,[status(thm)],[c_265,c_5906]) ).
cnf(c_5908,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(join(A,B),meet(meet(join(A,B),C),join(B,meet(C,D)))),
inference(paramod,[status(thm)],[c_30,c_5907]) ).
cnf(c_5909,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(join(A,B),meet(join(A,B),meet(C,join(B,meet(C,D))))),
inference(paramod,[status(thm)],[c_7,c_5908]) ).
cnf(c_1354,plain,
meet(join(A,B),join(meet(B,C),meet(C,D))) = meet(join(A,B),meet(C,join(B,meet(C,D)))),
inference(paramod,[status(thm)],[c_24,c_5909]) ).
cnf(c_5910,plain,
join(meet(A,B),meet(B,C)) = meet(join(B,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_21,c_265]) ).
cnf(c_1582,plain,
join(meet(A,B),meet(B,C)) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_21,c_5910]) ).
cnf(c_1616,plain,
meet(join(A,B),meet(C,join(meet(B,C),D))) = meet(join(A,B),meet(C,join(B,meet(C,D)))),
inference(paramod,[status(thm)],[c_1582,c_1354]) ).
cnf(c_1727,plain,
join(meet(A,B),meet(C,meet(D,B))) = meet(B,join(meet(A,B),meet(C,D))),
inference(paramod,[status(thm)],[c_7,c_270]) ).
cnf(c_5911,plain,
join(meet(A,B),meet(C,meet(join(D,A),B))) = meet(meet(join(D,A),B),join(meet(A,meet(join(D,A),B)),C)),
inference(paramod,[status(thm)],[c_61,c_270]) ).
cnf(c_5912,plain,
meet(B,join(meet(A,B),meet(C,join(D,A)))) = meet(meet(join(D,A),B),join(meet(A,meet(join(D,A),B)),C)),
inference(paramod,[status(thm)],[c_1727,c_5911]) ).
cnf(c_5913,plain,
meet(B,meet(join(D,A),join(meet(A,B),C))) = meet(meet(join(D,A),B),join(meet(A,meet(join(D,A),B)),C)),
inference(paramod,[status(thm)],[c_247,c_5912]) ).
cnf(c_5914,plain,
meet(B,meet(join(D,A),join(meet(A,B),C))) = meet(meet(join(D,A),B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_61,c_5913]) ).
cnf(c_5915,plain,
meet(B,meet(join(D,A),join(meet(A,B),C))) = meet(join(D,A),meet(B,join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_7,c_5914]) ).
cnf(c_1742,plain,
meet(A,meet(join(B,C),join(meet(C,A),D))) = meet(join(B,C),meet(A,join(C,meet(A,D)))),
inference(paramod,[status(thm)],[c_1616,c_5915]) ).
cnf(c_5916,plain,
join(meet(A,B),meet(C,meet(B,join(A,D)))) = meet(meet(B,join(A,D)),join(meet(A,meet(B,join(A,D))),C)),
inference(paramod,[status(thm)],[c_72,c_270]) ).
cnf(c_5917,plain,
join(meet(A,B),meet(C,meet(B,join(A,D)))) = meet(meet(B,join(A,D)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_72,c_5916]) ).
cnf(c_1753,plain,
join(meet(A,B),meet(C,meet(B,join(A,D)))) = meet(B,meet(join(A,D),join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_7,c_5917]) ).
cnf(c_5918,plain,
meet(join(A,meet(B,C)),meet(C,join(meet(A,C),B))) = join(meet(A,C),meet(B,C)),
inference(paramod,[status(thm)],[c_270,c_162]) ).
cnf(c_5919,plain,
meet(C,meet(join(A,meet(B,C)),join(meet(A,C),B))) = join(meet(A,C),meet(B,C)),
inference(paramod,[status(thm)],[c_30,c_5918]) ).
cnf(c_1767,plain,
meet(A,meet(join(B,meet(C,A)),join(meet(B,A),C))) = meet(A,join(meet(B,A),C)),
inference(paramod,[status(thm)],[c_270,c_5919]) ).
cnf(c_5920,plain,
meet(join(meet(A,B),C),join(C,meet(A,meet(B,D)))) = join(C,meet(meet(A,B),D)),
inference(paramod,[status(thm)],[c_7,c_883]) ).
cnf(c_1878,plain,
meet(join(meet(A,B),C),join(C,meet(A,meet(B,D)))) = join(C,meet(A,meet(B,D))),
inference(paramod,[status(thm)],[c_7,c_5920]) ).
cnf(c_5921,plain,
meet(meet(A,join(meet(B,A),C)),join(meet(C,A),meet(meet(B,A),D))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_270,c_883]) ).
cnf(c_5922,plain,
meet(meet(A,join(meet(B,A),C)),join(meet(C,A),meet(B,meet(A,D)))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_7,c_5921]) ).
cnf(c_5923,plain,
meet(A,meet(join(meet(B,A),C),join(meet(C,A),meet(B,meet(A,D))))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_7,c_5922]) ).
cnf(c_5924,plain,
meet(join(meet(B,A),C),meet(A,join(C,meet(A,meet(B,meet(A,D)))))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_1742,c_5923]) ).
cnf(c_5925,plain,
meet(join(meet(B,A),C),meet(A,join(C,meet(B,meet(A,D))))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_66,c_5924]) ).
cnf(c_5926,plain,
meet(A,meet(join(meet(B,A),C),join(C,meet(B,meet(A,D))))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_30,c_5925]) ).
cnf(c_5927,plain,
meet(A,join(C,meet(B,meet(A,D)))) = join(meet(C,A),meet(meet(B,A),D)),
inference(paramod,[status(thm)],[c_1878,c_5926]) ).
cnf(c_5928,plain,
meet(A,join(C,meet(B,meet(A,D)))) = join(meet(C,A),meet(B,meet(A,D))),
inference(paramod,[status(thm)],[c_7,c_5927]) ).
cnf(c_1907,plain,
join(meet(A,B),meet(C,meet(B,D))) = meet(B,join(A,meet(C,meet(B,D)))),
inference(copy,[status(thm)],[c_5928]) ).
cnf(c_5929,plain,
meet(B,join(A,meet(C,meet(B,join(A,D))))) = meet(B,meet(join(A,D),join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_1907,c_1753]) ).
cnf(c_5930,plain,
meet(B,meet(join(A,D),join(A,meet(C,B)))) = meet(B,meet(join(A,D),join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_203,c_5929]) ).
cnf(c_1918,plain,
meet(A,meet(join(B,C),join(meet(B,A),D))) = meet(A,meet(join(B,C),join(B,meet(D,A)))),
inference(copy,[status(thm)],[c_5930]) ).
cnf(c_5931,plain,
meet(A,meet(join(B,meet(C,A)),join(B,meet(C,A)))) = meet(A,join(meet(B,A),C)),
inference(paramod,[status(thm)],[c_1918,c_1767]) ).
cnf(c_5932,plain,
meet(A,join(B,meet(C,A))) = meet(A,join(meet(B,A),C)),
inference(paramod,[status(thm)],[c_1,c_5931]) ).
cnf(c_1920,plain,
meet(A,join(meet(B,A),C)) = meet(A,join(B,meet(C,A))),
inference(copy,[status(thm)],[c_5932]) ).
cnf(c_5933,plain,
meet(b,join(meet(r2,b),a)) = meet(b,n1),
inference(paramod,[status(thm)],[c_53,c_1920]) ).
cnf(c_5934,plain,
meet(b,join(meet(b,r2),a)) = meet(b,n1),
inference(paramod,[status(thm)],[c_5,c_5933]) ).
cnf(c_5935,plain,
meet(b,join(a,meet(b,r2))) = meet(b,n1),
inference(paramod,[status(thm)],[c_6,c_5934]) ).
cnf(c_5936,plain,
meet(b,join(a,meet(b,r2))) = meet(n1,b),
inference(paramod,[status(thm)],[c_5,c_5935]) ).
cnf(c_2570,plain,
meet(b,join(a,meet(b,r2))) = b,
inference(paramod,[status(thm)],[c_41,c_5936]) ).
cnf(c_5937,plain,
join(join(a,meet(b,r2)),b) = join(a,meet(b,r2)),
inference(paramod,[status(thm)],[c_2570,c_21]) ).
cnf(c_5938,plain,
join(b,join(a,meet(b,r2))) = join(a,meet(b,r2)),
inference(paramod,[status(thm)],[c_6,c_5937]) ).
cnf(c_5939,plain,
join(a,join(b,meet(b,r2))) = join(a,meet(b,r2)),
inference(paramod,[status(thm)],[c_38,c_5938]) ).
cnf(c_5940,plain,
join(a,b) = join(a,meet(b,r2)),
inference(paramod,[status(thm)],[c_4,c_5939]) ).
cnf(c_2675,plain,
join(a,meet(b,r2)) = join(a,b),
inference(copy,[status(thm)],[c_5940]) ).
cnf(c_5941,plain,
join(join(a,b),A) = join(a,join(meet(b,r2),A)),
inference(paramod,[status(thm)],[c_2675,c_8]) ).
cnf(c_5942,plain,
join(a,join(b,A)) = join(a,join(meet(b,r2),A)),
inference(paramod,[status(thm)],[c_8,c_5941]) ).
cnf(c_2698,plain,
join(a,join(meet(b,r2),A)) = join(a,join(b,A)),
inference(copy,[status(thm)],[c_5942]) ).
cnf(c_5943,plain,
join(meet(b,A),n0) = meet(join(a,meet(b,A)),join(meet(b,A),meet(B,r1))),
inference(paramod,[status(thm)],[c_1188,c_265]) ).
cnf(c_5944,plain,
join(n0,meet(b,A)) = meet(join(a,meet(b,A)),join(meet(b,A),meet(B,r1))),
inference(paramod,[status(thm)],[c_6,c_5943]) ).
cnf(c_5945,plain,
meet(b,A) = meet(join(a,meet(b,A)),join(meet(b,A),meet(B,r1))),
inference(paramod,[status(thm)],[c_40,c_5944]) ).
cnf(c_4488,plain,
meet(join(a,meet(b,A)),join(meet(b,A),meet(B,r1))) = meet(b,A),
inference(copy,[status(thm)],[c_5945]) ).
cnf(c_5582,plain,
meet(join(a,b),join(meet(b,r2),meet(A,r1))) = meet(b,r2),
inference(paramod,[status(thm)],[c_2675,c_4488]) ).
cnf(c_5593,plain,
meet(join(a,b),join(meet(b,r2),meet(r1,A))) = meet(b,r2),
inference(paramod,[status(thm)],[c_5,c_5582]) ).
cnf(c_5946,plain,
meet(a,meet(b,r2)) = meet(a,join(meet(b,r2),meet(r1,A))),
inference(paramod,[status(thm)],[c_5593,c_27]) ).
cnf(c_5947,plain,
n0 = meet(a,join(meet(b,r2),meet(r1,A))),
inference(paramod,[status(thm)],[c_54,c_5946]) ).
cnf(c_5827,plain,
meet(a,join(meet(b,r2),meet(r1,A))) = n0,
inference(copy,[status(thm)],[c_5947]) ).
cnf(c_5948,plain,
( complement(a,join(meet(b,r2),meet(r1,A)))
| join(a,join(meet(b,r2),meet(r1,A))) != n1 ),
inference(resolve,[status(thm)],[c_17,c_5827]) ).
cnf(c_5949,plain,
join(a,join(meet(b,r2),meet(r1,A))) != n1,
inference(resolve,[status(thm)],[c_5948,c_20]) ).
cnf(c_5838,plain,
join(a,join(b,meet(r1,A))) != n1,
inference(paramod,[status(thm)],[c_2698,c_5949]) ).
cnf(c_5950,plain,
join(a,join(b,r1)) != n1,
inference(paramod,[status(thm)],[c_1,c_5838]) ).
cnf(c_5951,plain,
n1 != n1,
inference(paramod,[status(thm)],[c_51,c_5950]) ).
cnf(c_5870,plain,
$false,
inference(copy,[status(thm)],[c_5951]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 19:55:50 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2708189 was started by sandbox2 on n018,
% 0.10/0.37 % Fri Sep 25 19:55:50 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 149.45/20.55
% 149.45/20.55 % given #500 (T,wt=31): 5827 meet(a,join(meet(b,r2),meet(r1,A))) = n0. [para(5593(a,1),27(a,1,2)),rewrite([54(5)]),flip(a)].
% 149.45/20.55
% 149.45/20.55 % SZS status Unsatisfiable for theBenchmark
% 149.45/20.55
% 149.45/20.55 % Proof 1 at 2.95 (+ 0.76) seconds.
% 149.45/20.55 % Length of proof is 77.
% 149.45/20.55 % Level of proof is 17.
% 149.45/20.55 % Maximum clause weight is 58.000.
% 149.45/20.55 % Given clauses 503.
% 149.45/20.55
% 149.45/20.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------