%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT005-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 : n010.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:31 AM UTC 2026
% Result : Unsatisfiable 6.52s 1.22s
% Output : CNFRefutation 6.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 19
% Syntax : Number of formulae : 89 ( 44 unt; 0 def)
% Number of atoms : 181 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 188 ( 96 ~; 92 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 152 ( 2 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(join_0_and_x,axiom,
! [VAR_0] : join(n0,VAR_0,VAR_0),
file('theBenchmark.p',join_0_and_x) ).
cnf(c_3,plain,
join(n0,A,A),
inference(clausify,[status(thm)],[join_0_and_x]) ).
fof(meet_0_and_x,axiom,
! [VAR_0] : meet(n0,VAR_0,n0),
file('theBenchmark.p',meet_0_and_x) ).
cnf(c_4,plain,
meet(n0,A,n0),
inference(clausify,[status(thm)],[meet_0_and_x]) ).
fof(meet_x_and_x,axiom,
! [VAR_0] : meet(VAR_0,VAR_0,VAR_0),
file('theBenchmark.p',meet_x_and_x) ).
cnf(c_5,plain,
meet(A,A,A),
inference(clausify,[status(thm)],[meet_x_and_x]) ).
fof(meet_1_and_x,axiom,
! [VAR_0] : meet(n1,VAR_0,VAR_0),
file('theBenchmark.p',meet_1_and_x) ).
cnf(c_6,plain,
meet(n1,A,A),
inference(clausify,[status(thm)],[meet_1_and_x]) ).
fof(commutativity_of_join,axiom,
! [VAR_0,VAR_1,VAR_2] :
( join(VAR_1,VAR_0,VAR_2)
| ~ join(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_join) ).
cnf(c_8,plain,
( join(B,A,C)
| ~ join(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_join]) ).
fof(absorbtion2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( meet(VAR_0,VAR_2,VAR_0)
| ~ join(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',absorbtion2) ).
cnf(c_10,plain,
( meet(A,C,A)
| ~ join(A,B,C) ),
inference(clausify,[status(thm)],[absorbtion2]) ).
fof(associativity_of_meet1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( meet(VAR_2,VAR_3,VAR_5)
| ~ meet(VAR_0,VAR_4,VAR_5)
| ~ meet(VAR_1,VAR_3,VAR_4)
| ~ meet(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity_of_meet1) ).
cnf(c_11,plain,
( meet(C,D,F)
| ~ meet(A,E,F)
| ~ meet(B,D,E)
| ~ meet(A,B,C) ),
inference(clausify,[status(thm)],[associativity_of_meet1]) ).
fof(associativity_of_meet2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( meet(VAR_0,VAR_4,VAR_5)
| ~ meet(VAR_2,VAR_3,VAR_5)
| ~ meet(VAR_1,VAR_3,VAR_4)
| ~ meet(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity_of_meet2) ).
cnf(c_12,plain,
( meet(A,E,F)
| ~ meet(C,D,F)
| ~ meet(B,D,E)
| ~ meet(A,B,C) ),
inference(clausify,[status(thm)],[associativity_of_meet2]) ).
fof(modularity2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( meet(VAR_1,VAR_3,VAR_5)
| ~ join(VAR_0,VAR_4,VAR_5)
| ~ meet(VAR_2,VAR_1,VAR_4)
| ~ join(VAR_0,VAR_2,VAR_3)
| ~ meet(VAR_0,VAR_1,VAR_0) ),
file('theBenchmark.p',modularity2) ).
cnf(c_16,plain,
( meet(B,D,F)
| ~ join(A,E,F)
| ~ meet(C,B,E)
| ~ join(A,C,D)
| ~ meet(A,B,A) ),
inference(clausify,[status(thm)],[modularity2]) ).
fof(modularity3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( join(VAR_1,VAR_4,VAR_5)
| ~ meet(VAR_0,VAR_3,VAR_5)
| ~ meet(VAR_0,VAR_2,VAR_4)
| ~ join(VAR_2,VAR_1,VAR_3)
| ~ meet(VAR_0,VAR_1,VAR_1) ),
file('theBenchmark.p',modularity3) ).
cnf(c_17,plain,
( join(B,E,F)
| ~ meet(A,D,F)
| ~ meet(A,C,E)
| ~ join(C,B,D)
| ~ meet(A,B,B) ),
inference(clausify,[status(thm)],[modularity3]) ).
fof(meet_a_and_b,axiom,
meet(a,b,c),
file('theBenchmark.p',meet_a_and_b) ).
cnf(c_19,plain,
meet(a,b,c),
inference(clausify,[status(thm)],[meet_a_and_b]) ).
fof(meet_c_and_r2,axiom,
meet(c,r2,n0),
file('theBenchmark.p',meet_c_and_r2) ).
cnf(c_21,plain,
meet(c,r2,n0),
inference(clausify,[status(thm)],[meet_c_and_r2]) ).
fof(meet_r2_and_b,axiom,
meet(r2,b,e),
file('theBenchmark.p',meet_r2_and_b) ).
cnf(c_22,plain,
meet(r2,b,e),
inference(clausify,[status(thm)],[meet_r2_and_b]) ).
fof(join_a_and_b,axiom,
join(a,b,c2),
file('theBenchmark.p',join_a_and_b) ).
cnf(c_23,plain,
join(a,b,c2),
inference(clausify,[status(thm)],[join_a_and_b]) ).
fof(meet_c2_and_r1,axiom,
meet(c2,r1,n0),
file('theBenchmark.p',meet_c2_and_r1) ).
cnf(c_25,plain,
meet(c2,r1,n0),
inference(clausify,[status(thm)],[meet_c2_and_r1]) ).
fof(meet_r2_and_a,axiom,
meet(r2,a,d),
file('theBenchmark.p',meet_r2_and_a) ).
cnf(c_26,plain,
meet(r2,a,d),
inference(clausify,[status(thm)],[meet_r2_and_a]) ).
fof(join_r1_and_e,axiom,
join(r1,e,a2),
file('theBenchmark.p',join_r1_and_e) ).
cnf(c_27,plain,
join(r1,e,a2),
inference(clausify,[status(thm)],[join_r1_and_e]) ).
fof(join_r1_and_d,axiom,
join(r1,d,b2),
file('theBenchmark.p',join_r1_and_d) ).
cnf(c_28,plain,
join(r1,d,b2),
inference(clausify,[status(thm)],[join_r1_and_d]) ).
fof(meet_a2_and_b2,axiom,
~ meet(a2,b2,r1),
file('theBenchmark.p',meet_a2_and_b2) ).
cnf(c_29,plain,
~ meet(a2,b2,r1),
inference(clausify,[status(thm)],[meet_a2_and_b2]) ).
cnf(c_32,plain,
join(A,n0,A),
inference(resolve,[status(thm)],[c_8,c_3]) ).
cnf(c_2034,plain,
( meet(C,B,E)
| ~ join(n0,D,E)
| ~ meet(A,C,D)
| ~ join(n0,A,B) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_2035,plain,
( meet(B,A,D)
| ~ join(n0,C,D)
| ~ meet(A,B,C) ),
inference(resolve,[status(thm)],[c_2034,c_3]) ).
cnf(c_2036,plain,
( meet(r2,c,A)
| ~ join(n0,n0,A) ),
inference(resolve,[status(thm)],[c_2035,c_21]) ).
cnf(c_39,plain,
meet(r2,c,n0),
inference(resolve,[status(thm)],[c_2036,c_3]) ).
cnf(c_2037,plain,
( meet(C,B,E)
| ~ join(n0,D,E)
| ~ meet(A,C,D)
| ~ join(n0,A,B) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_2038,plain,
( meet(B,A,D)
| ~ join(n0,C,D)
| ~ meet(A,B,C) ),
inference(resolve,[status(thm)],[c_2037,c_3]) ).
cnf(c_2039,plain,
( meet(b,r2,A)
| ~ join(n0,e,A) ),
inference(resolve,[status(thm)],[c_2038,c_22]) ).
cnf(c_40,plain,
meet(b,r2,e),
inference(resolve,[status(thm)],[c_2039,c_3]) ).
cnf(c_2040,plain,
( meet(e,A,C)
| ~ meet(r2,B,C)
| ~ meet(b,A,B) ),
inference(resolve,[status(thm)],[c_11,c_22]) ).
cnf(c_2041,plain,
( meet(e,b,A)
| ~ meet(r2,b,A) ),
inference(resolve,[status(thm)],[c_2040,c_5]) ).
cnf(c_43,plain,
meet(e,b,e),
inference(resolve,[status(thm)],[c_2041,c_22]) ).
cnf(c_2042,plain,
( join(B,D,E)
| ~ meet(n1,C,E)
| ~ meet(n1,A,D)
| ~ join(A,B,C) ),
inference(resolve,[status(thm)],[c_17,c_6]) ).
cnf(c_2043,plain,
( join(b,A,B)
| ~ meet(n1,c2,B)
| ~ meet(n1,a,A) ),
inference(resolve,[status(thm)],[c_2042,c_23]) ).
cnf(c_2044,plain,
( join(b,a,A)
| ~ meet(n1,c2,A) ),
inference(resolve,[status(thm)],[c_2043,c_6]) ).
cnf(c_45,plain,
join(b,a,c2),
inference(resolve,[status(thm)],[c_2044,c_6]) ).
cnf(c_48,plain,
meet(a,c2,a),
inference(resolve,[status(thm)],[c_10,c_23]) ).
cnf(c_2045,plain,
( meet(C,B,E)
| ~ join(n0,D,E)
| ~ meet(A,C,D)
| ~ join(n0,A,B) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_2046,plain,
( meet(B,A,D)
| ~ join(n0,C,D)
| ~ meet(A,B,C) ),
inference(resolve,[status(thm)],[c_2045,c_3]) ).
cnf(c_2047,plain,
( meet(r1,c2,A)
| ~ join(n0,n0,A) ),
inference(resolve,[status(thm)],[c_2046,c_25]) ).
cnf(c_50,plain,
meet(r1,c2,n0),
inference(resolve,[status(thm)],[c_2047,c_3]) ).
cnf(c_2048,plain,
( join(B,D,E)
| ~ meet(n1,C,E)
| ~ meet(n1,A,D)
| ~ join(A,B,C) ),
inference(resolve,[status(thm)],[c_17,c_6]) ).
cnf(c_2049,plain,
( join(e,A,B)
| ~ meet(n1,a2,B)
| ~ meet(n1,r1,A) ),
inference(resolve,[status(thm)],[c_2048,c_27]) ).
cnf(c_2050,plain,
( join(e,r1,A)
| ~ meet(n1,a2,A) ),
inference(resolve,[status(thm)],[c_2049,c_6]) ).
cnf(c_56,plain,
join(e,r1,a2),
inference(resolve,[status(thm)],[c_2050,c_6]) ).
cnf(c_60,plain,
meet(r1,a2,r1),
inference(resolve,[status(thm)],[c_10,c_27]) ).
cnf(c_2051,plain,
( meet(d,A,C)
| ~ meet(r2,B,C)
| ~ meet(a,A,B) ),
inference(resolve,[status(thm)],[c_11,c_26]) ).
cnf(c_2052,plain,
( meet(d,b,A)
| ~ meet(r2,c,A) ),
inference(resolve,[status(thm)],[c_2051,c_19]) ).
cnf(c_170,plain,
meet(d,b,n0),
inference(resolve,[status(thm)],[c_2052,c_39]) ).
cnf(c_221,plain,
meet(b,c2,b),
inference(resolve,[status(thm)],[c_10,c_45]) ).
cnf(c_2053,plain,
( meet(d,A,C)
| ~ meet(r2,B,C)
| ~ meet(a,A,B) ),
inference(resolve,[status(thm)],[c_11,c_26]) ).
cnf(c_2054,plain,
( meet(d,c2,A)
| ~ meet(r2,a,A) ),
inference(resolve,[status(thm)],[c_2053,c_48]) ).
cnf(c_263,plain,
meet(d,c2,d),
inference(resolve,[status(thm)],[c_2054,c_26]) ).
cnf(c_2055,plain,
( meet(a2,B,D)
| ~ join(r1,C,D)
| ~ meet(A,a2,C)
| ~ join(r1,A,B) ),
inference(resolve,[status(thm)],[c_16,c_60]) ).
cnf(c_2056,plain,
( meet(a2,b2,B)
| ~ join(r1,A,B)
| ~ meet(d,a2,A) ),
inference(resolve,[status(thm)],[c_2055,c_28]) ).
cnf(c_2057,plain,
( meet(a2,b2,r1)
| ~ meet(d,a2,n0) ),
inference(resolve,[status(thm)],[c_2056,c_32]) ).
cnf(c_368,plain,
~ meet(d,a2,n0),
inference(resolve,[status(thm)],[c_2057,c_29]) ).
cnf(c_2058,plain,
( meet(d,B,C)
| ~ meet(n0,A,C)
| ~ meet(b,A,B) ),
inference(resolve,[status(thm)],[c_12,c_170]) ).
cnf(c_2059,plain,
( meet(d,e,A)
| ~ meet(n0,r2,A) ),
inference(resolve,[status(thm)],[c_2058,c_40]) ).
cnf(c_616,plain,
meet(d,e,n0),
inference(resolve,[status(thm)],[c_2059,c_4]) ).
cnf(c_2060,plain,
( meet(e,A,C)
| ~ meet(e,B,C)
| ~ meet(b,A,B) ),
inference(resolve,[status(thm)],[c_11,c_43]) ).
cnf(c_2061,plain,
( meet(e,c2,A)
| ~ meet(e,b,A) ),
inference(resolve,[status(thm)],[c_2060,c_221]) ).
cnf(c_880,plain,
meet(e,c2,e),
inference(resolve,[status(thm)],[c_2061,c_43]) ).
cnf(c_2062,plain,
( meet(d,A,C)
| ~ meet(d,B,C)
| ~ meet(c2,A,B) ),
inference(resolve,[status(thm)],[c_11,c_263]) ).
cnf(c_2063,plain,
( meet(d,A,n0)
| ~ meet(c2,A,e) ),
inference(resolve,[status(thm)],[c_2062,c_616]) ).
cnf(c_1899,plain,
~ meet(c2,a2,e),
inference(resolve,[status(thm)],[c_2063,c_368]) ).
cnf(c_2064,plain,
( meet(c2,B,D)
| ~ join(e,C,D)
| ~ meet(A,c2,C)
| ~ join(e,A,B) ),
inference(resolve,[status(thm)],[c_16,c_880]) ).
cnf(c_2065,plain,
( meet(c2,a2,B)
| ~ join(e,A,B)
| ~ meet(r1,c2,A) ),
inference(resolve,[status(thm)],[c_2064,c_56]) ).
cnf(c_2066,plain,
( meet(c2,a2,A)
| ~ join(e,n0,A) ),
inference(resolve,[status(thm)],[c_2065,c_50]) ).
cnf(c_2032,plain,
meet(c2,a2,e),
inference(resolve,[status(thm)],[c_2066,c_32]) ).
cnf(c_2033,plain,
$false,
inference(resolve,[status(thm)],[c_2032,c_1899]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT005-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 : n010.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:54:59 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 1514922 was started by sandbox2 on n010,
% 0.10/0.37 % Fri Sep 25 19:54:59 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).
% 6.52/1.22
% 6.52/1.22 % SZS status Unsatisfiable for theBenchmark
% 6.52/1.22
% 6.52/1.22 % Proof 1 at 0.66 (+ 0.14) seconds.
% 6.52/1.22 % Length of proof is 37.
% 6.52/1.22 % Level of proof is 5.
% 6.52/1.22 % Maximum clause weight is 20.000.
% 6.52/1.22 % Given clauses 217.
% 6.52/1.22
% 6.52/1.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------