%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LAT005-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:37:17 PM UTC 2026
% Result : Unsatisfiable 194.20s 85.99s
% Output : CNFRefutation 197.50s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_126)
% Comments :
%------------------------------------------------------------------------------
cnf(modularity2,axiom,
( meet(X2,X4,X6)
| ~ meet(X1,X2,X1)
| ~ join(X1,X3,X4)
| ~ meet(X3,X2,X5)
| ~ join(X1,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modularity2) ).
cnf(modularity1,axiom,
( join(X1,X5,X6)
| ~ meet(X1,X2,X1)
| ~ join(X1,X3,X4)
| ~ meet(X3,X2,X5)
| ~ meet(X2,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modularity1) ).
cnf(associativity_of_meet2,axiom,
( meet(X1,X5,X6)
| ~ meet(X1,X2,X3)
| ~ meet(X2,X4,X5)
| ~ meet(X3,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet2) ).
cnf(associativity_of_meet1,axiom,
( meet(X3,X4,X6)
| ~ meet(X1,X2,X3)
| ~ meet(X2,X4,X5)
| ~ meet(X1,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet1) ).
cnf(associativity_of_join2,axiom,
( join(X1,X5,X6)
| ~ join(X1,X2,X3)
| ~ join(X2,X4,X5)
| ~ join(X3,X4,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join2) ).
cnf(associativity_of_join1,axiom,
( join(X3,X4,X6)
| ~ join(X1,X2,X3)
| ~ join(X2,X4,X5)
| ~ join(X1,X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join1) ).
cnf(absorbtion2,axiom,
( meet(X1,X3,X1)
| ~ join(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorbtion2) ).
cnf(commutativity_of_meet,axiom,
( meet(X2,X1,X3)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
cnf(absorbtion1,axiom,
( join(X1,X3,X1)
| ~ meet(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorbtion1) ).
cnf(commutativity_of_join,axiom,
( join(X2,X1,X3)
| ~ join(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
cnf(meet_a2_and_b2,negated_conjecture,
~ meet(a2,b2,r1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_a2_and_b2) ).
cnf(meet_x_and_x,axiom,
meet(X1,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_x_and_x) ).
cnf(join_x_and_x,axiom,
join(X1,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_x_and_x) ).
cnf(meet_1_and_x,axiom,
meet(n1,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_1_and_x) ).
cnf(join_0_and_x,axiom,
join(n0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_0_and_x) ).
cnf(meet_x_and_1,axiom,
meet(X1,n1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_x_and_1) ).
cnf(join_x_and_0,axiom,
join(X1,n0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_x_and_0) ).
cnf(meet_0_and_x,axiom,
meet(n0,X1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_0_and_x) ).
cnf(join_1_and_x,axiom,
join(n1,X1,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_1_and_x) ).
cnf(meet_x_and_0,axiom,
meet(X1,n0,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_x_and_0) ).
cnf(join_x_and_1,axiom,
join(X1,n1,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_x_and_1) ).
cnf(meet_c2_and_r1,negated_conjecture,
meet(c2,r1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_c2_and_r1) ).
cnf(meet_r2_and_b,negated_conjecture,
meet(r2,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_r2_and_b) ).
cnf(meet_r2_and_a,negated_conjecture,
meet(r2,a,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_r2_and_a) ).
cnf(meet_c_and_r2,negated_conjecture,
meet(c,r2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_c_and_r2) ).
cnf(meet_a_and_b,negated_conjecture,
meet(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_a_and_b) ).
cnf(join_c2_and_r1,negated_conjecture,
join(c2,r1,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_c2_and_r1) ).
cnf(join_c_and_r2,negated_conjecture,
join(c,r2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_c_and_r2) ).
cnf(join_a_and_b,negated_conjecture,
join(a,b,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_a_and_b) ).
cnf(join_r1_and_d,negated_conjecture,
join(r1,d,b2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_r1_and_d) ).
cnf(join_r1_and_e,negated_conjecture,
join(r1,e,a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',join_r1_and_e) ).
cnf(i_0_31,axiom,
( meet(X2,X4,X6)
| ~ meet(X1,X2,X1)
| ~ join(X1,X3,X4)
| ~ meet(X3,X2,X5)
| ~ join(X1,X5,X6) ),
modularity2,
[final] ).
cnf(i_0_32,axiom,
( join(X1,X5,X6)
| ~ meet(X1,X2,X1)
| ~ join(X1,X3,X4)
| ~ meet(X3,X2,X5)
| ~ meet(X2,X4,X6) ),
modularity1,
[final] ).
cnf(i_0_33,axiom,
( meet(X1,X5,X6)
| ~ meet(X1,X2,X3)
| ~ meet(X2,X4,X5)
| ~ meet(X3,X4,X6) ),
associativity_of_meet2,
[final] ).
cnf(i_0_34,axiom,
( meet(X3,X4,X6)
| ~ meet(X1,X2,X3)
| ~ meet(X2,X4,X5)
| ~ meet(X1,X5,X6) ),
associativity_of_meet1,
[final] ).
cnf(i_0_35,axiom,
( join(X1,X5,X6)
| ~ join(X1,X2,X3)
| ~ join(X2,X4,X5)
| ~ join(X3,X4,X6) ),
associativity_of_join2,
[final] ).
cnf(i_0_36,axiom,
( join(X3,X4,X6)
| ~ join(X1,X2,X3)
| ~ join(X2,X4,X5)
| ~ join(X1,X5,X6) ),
associativity_of_join1,
[final] ).
cnf(i_0_37,axiom,
( meet(X1,X3,X1)
| ~ join(X1,X2,X3) ),
absorbtion2,
[final] ).
cnf(i_0_38,axiom,
( meet(X2,X1,X3)
| ~ meet(X1,X2,X3) ),
commutativity_of_meet,
[final] ).
cnf(i_0_39,axiom,
( join(X1,X3,X1)
| ~ meet(X1,X2,X3) ),
absorbtion1,
[final] ).
cnf(i_0_40,axiom,
( join(X2,X1,X3)
| ~ join(X1,X2,X3) ),
commutativity_of_join,
[final] ).
cnf(i_0_41,negated_conjecture,
~ meet(a2,b2,r1),
meet_a2_and_b2,
[final] ).
cnf(i_0_42,axiom,
meet(X1,X1,X1),
meet_x_and_x,
[final] ).
cnf(i_0_43,axiom,
join(X1,X1,X1),
join_x_and_x,
[final] ).
cnf(i_0_44,axiom,
meet(n1,X1,X1),
meet_1_and_x,
[final] ).
cnf(i_0_45,axiom,
join(n0,X1,X1),
join_0_and_x,
[final] ).
cnf(i_0_46,axiom,
meet(X1,n1,X1),
meet_x_and_1,
[final] ).
cnf(i_0_47,axiom,
join(X1,n0,X1),
join_x_and_0,
[final] ).
cnf(i_0_48,axiom,
meet(n0,X1,n0),
meet_0_and_x,
[final] ).
cnf(i_0_49,axiom,
join(n1,X1,n1),
join_1_and_x,
[final] ).
cnf(i_0_50,axiom,
meet(X1,n0,n0),
meet_x_and_0,
[final] ).
cnf(i_0_51,axiom,
join(X1,n1,n1),
join_x_and_1,
[final] ).
cnf(i_0_52,negated_conjecture,
meet(c2,r1,n0),
meet_c2_and_r1,
[final] ).
cnf(i_0_53,negated_conjecture,
meet(r2,b,e),
meet_r2_and_b,
[final] ).
cnf(i_0_54,negated_conjecture,
meet(r2,a,d),
meet_r2_and_a,
[final] ).
cnf(i_0_55,negated_conjecture,
meet(c,r2,n0),
meet_c_and_r2,
[final] ).
cnf(i_0_56,negated_conjecture,
meet(a,b,c),
meet_a_and_b,
[final] ).
cnf(i_0_57,negated_conjecture,
join(c2,r1,n1),
join_c2_and_r1,
[final] ).
cnf(i_0_58,negated_conjecture,
join(c,r2,n1),
join_c_and_r2,
[final] ).
cnf(i_0_59,negated_conjecture,
join(a,b,c2),
join_a_and_b,
[final] ).
cnf(i_0_60,negated_conjecture,
join(r1,d,b2),
join_r1_and_d,
[final] ).
cnf(i_0_61,negated_conjecture,
join(r1,e,a2),
join_r1_and_e,
[final] ).
cnf(i_0_203,plain,
join(d,b2,b2),
inference(scs_inference,[],[i_0_103,i_0_40]) ).
cnf(i_0_205,plain,
meet(e,a,n0),
inference(scs_inference,[],[i_0_126,i_0_103,i_0_40,i_0_38]) ).
cnf(i_0_207,plain,
join(r1,b2,b2),
inference(scs_inference,[],[i_0_60,i_0_126,i_0_103,i_0_43,i_0_40,i_0_38,i_0_35]) ).
cnf(i_0_219,plain,
join(e,a2,a2),
inference(scs_inference,[],[i_0_123,i_0_40]) ).
cnf(i_0_601,plain,
meet(d,r2,d),
inference(scs_inference,[],[i_0_42,i_0_85,i_0_34]) ).
cnf(i_0_604,plain,
meet(r2,d,d),
inference(scs_inference,[],[i_0_42,i_0_85,i_0_34,i_0_38]) ).
cnf(i_0_609,plain,
meet(c,a,c),
inference(scs_inference,[],[i_0_42,i_0_143,i_0_34]) ).
cnf(i_0_612,plain,
meet(a,c,c),
inference(scs_inference,[],[i_0_42,i_0_143,i_0_34,i_0_38]) ).
cnf(i_0_873,plain,
meet(d,e,n0),
inference(scs_inference,[],[i_0_54,i_0_50,i_0_126,i_0_34]) ).
cnf(i_0_876,plain,
meet(e,d,n0),
inference(scs_inference,[],[i_0_54,i_0_50,i_0_126,i_0_34,i_0_38]) ).
cnf(i_0_1631,plain,
join(r2,e,r2),
inference(scs_inference,[],[i_0_66,i_0_39]) ).
cnf(i_0_1658,plain,
join(b,c,b),
inference(scs_inference,[],[i_0_143,i_0_39]) ).
cnf(i_0_1708,plain,
join(a,d,a),
inference(scs_inference,[],[i_0_570,i_0_39]) ).
cnf(i_0_1710,plain,
meet(b,c2,b),
inference(scs_inference,[],[i_0_141,i_0_570,i_0_39,i_0_37]) ).
cnf(i_0_163,plain,
join(b,c2,c2),
inference(scs_inference,[],[i_0_75,i_0_40]) ).
cnf(i_0_165,plain,
meet(b,e,e),
inference(scs_inference,[],[i_0_69,i_0_75,i_0_40,i_0_38]) ).
cnf(i_0_167,plain,
join(a2,r1,a2),
inference(scs_inference,[],[i_0_69,i_0_75,i_0_119,i_0_43,i_0_40,i_0_38,i_0_36]) ).
cnf(i_0_185,plain,
join(c2,a,c2),
inference(scs_inference,[],[i_0_72,i_0_40]) ).
cnf(i_0_187,plain,
meet(e,r2,e),
inference(scs_inference,[],[i_0_66,i_0_72,i_0_40,i_0_38]) ).
cnf(i_0_1603,plain,
join(a,c,a),
inference(scs_inference,[],[i_0_612,i_0_39]) ).
cnf(i_0_1605,plain,
~ meet(b2,a2,r1),
inference(scs_inference,[],[i_0_612,i_0_45,i_0_39,i_0_134]) ).
cnf(i_0_1633,plain,
meet(e,a2,e),
inference(scs_inference,[],[i_0_219,i_0_66,i_0_39,i_0_37]) ).
cnf(i_0_1660,plain,
meet(r1,b2,r1),
inference(scs_inference,[],[i_0_207,i_0_143,i_0_39,i_0_37]) ).
cnf(i_0_1736,plain,
join(r2,d,r2),
inference(scs_inference,[],[i_0_604,i_0_39]) ).
cnf(i_0_1738,plain,
meet(a,c2,a),
inference(scs_inference,[],[i_0_72,i_0_604,i_0_39,i_0_37]) ).
cnf(i_0_231,plain,
join(r1,a2,a2),
inference(scs_inference,[],[i_0_167,i_0_40]) ).
cnf(i_0_1685,plain,
join(b,e,b),
inference(scs_inference,[],[i_0_165,i_0_39]) ).
cnf(i_0_1687,plain,
meet(d,b2,d),
inference(scs_inference,[],[i_0_203,i_0_165,i_0_39,i_0_37]) ).
cnf(i_0_2043,plain,
~ meet(r1,r1,a2),
inference(scs_inference,[],[i_0_1660,i_0_151]) ).
cnf(i_0_1608,plain,
meet(r1,a2,r1),
inference(scs_inference,[],[i_0_231,i_0_612,i_0_45,i_0_39,i_0_134,i_0_37]) ).
cnf(i_0_1610,plain,
join(d,r2,r2),
inference(scs_inference,[],[i_0_231,i_0_612,i_0_601,i_0_45,i_0_51,i_0_44,i_0_46,i_0_39,i_0_134,i_0_37,i_0_32]) ).
cnf(i_0_1615,plain,
~ meet(d,a2,n0),
inference(scs_inference,[],[i_0_231,i_0_612,i_0_601,i_0_45,i_0_51,i_0_44,i_0_46,i_0_39,i_0_134,i_0_37,i_0_32,i_0_213]) ).
cnf(i_0_1616,plain,
~ meet(a2,d,n0),
inference(scs_inference,[],[i_0_231,i_0_612,i_0_601,i_0_45,i_0_51,i_0_44,i_0_46,i_0_39,i_0_134,i_0_37,i_0_32,i_0_213,i_0_38]) ).
cnf(i_0_1618,plain,
meet(e,c,n0),
inference(scs_inference,[],[i_0_231,i_0_612,i_0_205,i_0_601,i_0_45,i_0_51,i_0_48,i_0_44,i_0_46,i_0_39,i_0_134,i_0_37,i_0_32,i_0_213,i_0_38,i_0_33]) ).
cnf(i_0_1630,plain,
~ meet(d,a2,r1),
inference(scs_inference,[],[i_0_1608,i_0_157]) ).
cnf(i_0_1635,plain,
~ meet(a2,r2,c),
inference(scs_inference,[],[i_0_1616,i_0_219,i_0_66,i_0_604,i_0_426,i_0_39,i_0_37,i_0_33]) ).
cnf(i_0_1637,plain,
~ meet(d,a2,c),
inference(scs_inference,[],[i_0_1615,i_0_1616,i_0_219,i_0_101,i_0_66,i_0_604,i_0_426,i_0_39,i_0_37,i_0_33,i_0_34]) ).
cnf(i_0_1639,plain,
join(c2,c,c2),
inference(scs_inference,[],[i_0_1615,i_0_1603,i_0_1616,i_0_219,i_0_185,i_0_101,i_0_66,i_0_604,i_0_426,i_0_39,i_0_37,i_0_33,i_0_34,i_0_36]) ).
cnf(i_0_1641,plain,
meet(c,e,n0),
inference(scs_inference,[],[i_0_1615,i_0_1618,i_0_1603,i_0_1616,i_0_219,i_0_185,i_0_101,i_0_66,i_0_604,i_0_45,i_0_426,i_0_43,i_0_48,i_0_39,i_0_37,i_0_33,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1646,plain,
~ meet(r2,a2,c),
inference(scs_inference,[],[i_0_1615,i_0_1618,i_0_1603,i_0_1616,i_0_219,i_0_185,i_0_101,i_0_66,i_0_604,i_0_45,i_0_426,i_0_43,i_0_48,i_0_39,i_0_37,i_0_33,i_0_34,i_0_36,i_0_31,i_0_38]) ).
cnf(i_0_1651,plain,
join(c,b,b),
inference(scs_inference,[],[i_0_41,i_0_1615,i_0_1618,i_0_1603,i_0_1616,i_0_219,i_0_185,i_0_101,i_0_66,i_0_604,i_0_581,i_0_45,i_0_426,i_0_51,i_0_43,i_0_48,i_0_44,i_0_1649,i_0_46,i_0_39,i_0_37,i_0_33,i_0_34,i_0_36,i_0_31,i_0_38,i_0_1638,i_0_32]) ).
cnf(i_0_1662,plain,
~ meet(a2,d,r1),
inference(scs_inference,[],[i_0_1630,i_0_207,i_0_143,i_0_39,i_0_37,i_0_38]) ).
cnf(i_0_1664,plain,
~ meet(e,n0,a2),
inference(scs_inference,[],[i_0_1630,i_0_207,i_0_1615,i_0_143,i_0_873,i_0_50,i_0_39,i_0_37,i_0_38,i_0_33]) ).
cnf(i_0_1667,plain,
~ join(r1,r1,d),
inference(scs_inference,[],[i_0_1630,i_0_1608,i_0_207,i_0_1615,i_0_143,i_0_873,i_0_43,i_0_50,i_0_39,i_0_37,i_0_38,i_0_33,i_0_31]) ).
cnf(i_0_1670,plain,
~ meet(a2,r1,d),
inference(scs_inference,[],[i_0_1630,i_0_1608,i_0_207,i_0_1615,i_0_143,i_0_873,i_0_43,i_0_1668,i_0_50,i_0_39,i_0_37,i_0_38,i_0_33,i_0_31,i_0_32]) ).
cnf(i_0_1712,plain,
~ meet(a2,d,c),
inference(scs_inference,[],[i_0_1637,i_0_141,i_0_570,i_0_39,i_0_37,i_0_38]) ).
cnf(i_0_1689,plain,
~ meet(n0,e,a2),
inference(scs_inference,[],[i_0_1664,i_0_203,i_0_165,i_0_39,i_0_37,i_0_38]) ).
cnf(i_0_1691,plain,
~ meet(e,c,a2),
inference(scs_inference,[],[i_0_1664,i_0_203,i_0_101,i_0_165,i_0_187,i_0_39,i_0_37,i_0_38,i_0_33]) ).
cnf(i_0_1693,plain,
join(r2,b,n1),
inference(scs_inference,[],[i_0_1664,i_0_1651,i_0_203,i_0_87,i_0_101,i_0_49,i_0_165,i_0_187,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35]) ).
cnf(i_0_1696,plain,
~ meet(n1,r1,a2),
inference(scs_inference,[],[i_0_41,i_0_1664,i_0_1651,i_0_1660,i_0_203,i_0_87,i_0_101,i_0_49,i_0_165,i_0_187,i_0_44,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1699,plain,
join(a2,c2,n1),
inference(scs_inference,[],[i_0_41,i_0_1664,i_0_1651,i_0_1660,i_0_203,i_0_87,i_0_64,i_0_101,i_0_167,i_0_49,i_0_165,i_0_51,i_0_187,i_0_44,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1702,plain,
meet(b2,r1,r1),
inference(scs_inference,[],[i_0_41,i_0_1664,i_0_1651,i_0_1660,i_0_203,i_0_87,i_0_64,i_0_101,i_0_167,i_0_49,i_0_165,i_0_45,i_0_51,i_0_187,i_0_48,i_0_44,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1768,plain,
~ meet(r1,a2,d),
inference(scs_inference,[],[i_0_1670,i_0_38]) ).
cnf(i_0_1714,plain,
~ meet(n0,a2,a2),
inference(scs_inference,[],[i_0_1689,i_0_1637,i_0_1633,i_0_141,i_0_570,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33]) ).
cnf(i_0_1717,plain,
join(r2,c2,n1),
inference(scs_inference,[],[i_0_1689,i_0_1637,i_0_1693,i_0_1633,i_0_141,i_0_49,i_0_570,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35]) ).
cnf(i_0_1720,plain,
~ meet(b2,a2,e),
inference(scs_inference,[],[i_0_1689,i_0_1637,i_0_1687,i_0_1693,i_0_1633,i_0_141,i_0_1615,i_0_873,i_0_49,i_0_570,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1722,plain,
join(b,r2,n1),
inference(scs_inference,[],[i_0_1658,i_0_1689,i_0_1637,i_0_1687,i_0_1693,i_0_1633,i_0_141,i_0_1615,i_0_873,i_0_49,i_0_570,i_0_51,i_0_58,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1725,plain,
meet(b2,d,d),
inference(scs_inference,[],[i_0_1658,i_0_1689,i_0_1637,i_0_1687,i_0_1693,i_0_1633,i_0_141,i_0_1615,i_0_873,i_0_49,i_0_570,i_0_45,i_0_51,i_0_58,i_0_48,i_0_1715,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1729,plain,
join(e,b,b),
inference(scs_inference,[],[i_0_1658,i_0_1689,i_0_1637,i_0_1687,i_0_1693,i_0_1633,i_0_141,i_0_1615,i_0_873,i_0_49,i_0_570,i_0_45,i_0_51,i_0_58,i_0_48,i_0_1715,i_0_39,i_0_37,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_388]) ).
cnf(i_0_1740,plain,
~ meet(c,e,a2),
inference(scs_inference,[],[i_0_1691,i_0_72,i_0_604,i_0_39,i_0_37,i_0_38]) ).
cnf(i_0_1742,plain,
~ meet(r1,b2,a2),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_72,i_0_1660,i_0_604,i_0_39,i_0_37,i_0_38,i_0_33]) ).
cnf(i_0_1744,plain,
~ meet(b2,r1,a2),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_72,i_0_1660,i_0_604,i_0_39,i_0_37,i_0_38,i_0_33,i_0_34]) ).
cnf(i_0_1746,plain,
~ join(n0,r1,d),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_1667,i_0_72,i_0_1660,i_0_604,i_0_45,i_0_43,i_0_39,i_0_37,i_0_38,i_0_33,i_0_34,i_0_36]) ).
cnf(i_0_1750,plain,
~ join(n0,r1,a2),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_1667,i_0_72,i_0_1660,i_0_604,i_0_45,i_0_1747,i_0_43,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1754,plain,
~ join(r1,n0,d),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_1667,i_0_72,i_0_1660,i_0_604,i_0_45,i_0_1747,i_0_43,i_0_48,i_0_39,i_0_37,i_0_38,i_0_33,i_0_34,i_0_36,i_0_31,i_0_40]) ).
cnf(i_0_1789,plain,
~ meet(r1,n1,a2),
inference(scs_inference,[],[i_0_1696,i_0_38]) ).
cnf(i_0_1758,plain,
~ meet(d,b2,r1),
inference(scs_inference,[],[i_0_1605,i_0_1691,i_0_1702,i_0_1725,i_0_1667,i_0_72,i_0_1660,i_0_207,i_0_604,i_0_45,i_0_1747,i_0_1752,i_0_43,i_0_48,i_0_1751,i_0_39,i_0_37,i_0_38,i_0_33,i_0_34,i_0_36,i_0_31,i_0_40,i_0_35,i_0_32]) ).
cnf(i_0_1770,plain,
~ join(r1,n0,a2),
inference(scs_inference,[],[i_0_1670,i_0_1750,i_0_38,i_0_40]) ).
cnf(i_0_1772,plain,
~ meet(r1,a2,a2),
inference(scs_inference,[],[i_0_1670,i_0_1744,i_0_1750,i_0_1608,i_0_1702,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1774,plain,
meet(c,c2,c),
inference(scs_inference,[],[i_0_1670,i_0_1710,i_0_1744,i_0_1750,i_0_1608,i_0_1702,i_0_581,i_0_38,i_0_40,i_0_33,i_0_34]) ).
cnf(i_0_1776,plain,
join(c2,e,c2),
inference(scs_inference,[],[i_0_1685,i_0_1670,i_0_1710,i_0_1744,i_0_1750,i_0_75,i_0_1608,i_0_1702,i_0_581,i_0_38,i_0_40,i_0_33,i_0_34,i_0_36]) ).
cnf(i_0_1778,plain,
~ meet(a2,n0,a2),
inference(scs_inference,[],[i_0_1685,i_0_1670,i_0_1710,i_0_1714,i_0_1744,i_0_1750,i_0_75,i_0_1608,i_0_1702,i_0_581,i_0_45,i_0_50,i_0_38,i_0_40,i_0_33,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1783,plain,
join(c,e,b),
inference(scs_inference,[],[i_0_1685,i_0_1670,i_0_1710,i_0_1714,i_0_1744,i_0_1750,i_0_75,i_0_1608,i_0_1702,i_0_581,i_0_45,i_0_58,i_0_50,i_0_53,i_0_46,i_0_38,i_0_40,i_0_33,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_1788,plain,
~ meet(e,r1,e),
inference(scs_inference,[],[i_0_1772,i_0_606]) ).
cnf(i_0_1791,plain,
~ meet(n0,c2,a2),
inference(scs_inference,[],[i_0_1696,i_0_1774,i_0_1618,i_0_1691,i_0_38,i_0_33]) ).
cnf(i_0_1793,plain,
join(e,c2,c2),
inference(scs_inference,[],[i_0_1696,i_0_1774,i_0_1729,i_0_1618,i_0_1691,i_0_163,i_0_38,i_0_33,i_0_35]) ).
cnf(i_0_1795,plain,
~ meet(b2,d,r1),
inference(scs_inference,[],[i_0_1696,i_0_1758,i_0_1774,i_0_1729,i_0_1618,i_0_1691,i_0_1725,i_0_1687,i_0_163,i_0_38,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1797,plain,
join(c2,d,c2),
inference(scs_inference,[],[i_0_1696,i_0_1758,i_0_1774,i_0_1729,i_0_1708,i_0_1618,i_0_1691,i_0_1725,i_0_1687,i_0_185,i_0_163,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1799,plain,
meet(c2,a,a),
inference(scs_inference,[],[i_0_1738,i_0_1696,i_0_1758,i_0_1774,i_0_1729,i_0_1708,i_0_1618,i_0_1691,i_0_1725,i_0_1687,i_0_185,i_0_163,i_0_45,i_0_48,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1804,plain,
meet(e,c2,e),
inference(scs_inference,[],[i_0_1738,i_0_1696,i_0_1758,i_0_1774,i_0_1729,i_0_1708,i_0_1618,i_0_1691,i_0_1725,i_0_1687,i_0_185,i_0_163,i_0_45,i_0_48,i_0_38,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_37]) ).
cnf(i_0_1889,plain,
~ meet(a2,r1,a2),
inference(scs_inference,[],[i_0_1772,i_0_38]) ).
cnf(i_0_1810,plain,
~ meet(r1,e,e),
inference(scs_inference,[],[i_0_1788,i_0_38]) ).
cnf(i_0_1812,plain,
~ meet(c2,c2,r1),
inference(scs_inference,[],[i_0_1788,i_0_1804,i_0_38,i_0_33]) ).
cnf(i_0_1814,plain,
~ join(r1,r1,a2),
inference(scs_inference,[],[i_0_1788,i_0_1804,i_0_1750,i_0_45,i_0_43,i_0_38,i_0_33,i_0_35]) ).
cnf(i_0_1818,plain,
~ meet(a,n0,a2),
inference(scs_inference,[],[i_0_1788,i_0_1740,i_0_1804,i_0_1641,i_0_1750,i_0_612,i_0_45,i_0_43,i_0_38,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1820,plain,
~ join(c2,e,r1),
inference(scs_inference,[],[i_0_1788,i_0_1776,i_0_1740,i_0_1804,i_0_1641,i_0_1750,i_0_612,i_0_45,i_0_43,i_0_42,i_0_38,i_0_33,i_0_35,i_0_34,i_0_31]) ).
cnf(i_0_1823,plain,
~ join(e,X1,r1),
inference(scs_inference,[],[i_0_1788,i_0_1776,i_0_1740,i_0_1804,i_0_1641,i_0_1750,i_0_612,i_0_45,i_0_43,i_0_42,i_0_38,i_0_33,i_0_35,i_0_34,i_0_31,i_0_37]) ).
cnf(i_0_1825,plain,
~ join(X1,e,r1),
inference(scs_inference,[],[i_0_1788,i_0_1776,i_0_1740,i_0_1804,i_0_1641,i_0_1750,i_0_612,i_0_45,i_0_43,i_0_42,i_0_38,i_0_33,i_0_35,i_0_34,i_0_31,i_0_37,i_0_40]) ).
cnf(i_0_1838,plain,
~ join(n0,a,b),
inference(scs_inference,[],[i_0_1810,i_0_741]) ).
cnf(i_0_1839,plain,
~ join(n0,n0,b),
inference(scs_inference,[],[i_0_1810,i_0_746]) ).
cnf(i_0_1840,plain,
~ join(n0,d,n1),
inference(scs_inference,[],[i_0_1810,i_0_1425]) ).
cnf(i_0_1841,plain,
~ join(n0,d,e),
inference(scs_inference,[],[i_0_1810,i_0_1447]) ).
cnf(i_0_1842,plain,
~ join(n0,a,e),
inference(scs_inference,[],[i_0_1810,i_0_1454]) ).
cnf(i_0_1843,plain,
~ join(d,e,n0),
inference(scs_inference,[],[i_0_1825,i_0_221]) ).
cnf(i_0_1844,plain,
~ join(X1,e,r1),
inference(rename_variables,[],[i_0_1825]) ).
cnf(i_0_1846,plain,
~ meet(a2,b2,e),
inference(scs_inference,[],[i_0_1825,i_0_1720,i_0_221,i_0_38]) ).
cnf(i_0_1848,plain,
~ join(e,d,n0),
inference(scs_inference,[],[i_0_1825,i_0_1720,i_0_221,i_0_38,i_0_40]) ).
cnf(i_0_1850,plain,
~ meet(d,c,a2),
inference(scs_inference,[],[i_0_1825,i_0_1720,i_0_1818,i_0_101,i_0_85,i_0_221,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1852,plain,
join(c,c2,c2),
inference(scs_inference,[],[i_0_1783,i_0_1825,i_0_1720,i_0_1793,i_0_1818,i_0_101,i_0_163,i_0_85,i_0_221,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1854,plain,
~ meet(e,a,a2),
inference(scs_inference,[],[i_0_1783,i_0_1825,i_0_1720,i_0_1791,i_0_1793,i_0_1818,i_0_1738,i_0_101,i_0_163,i_0_205,i_0_85,i_0_221,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1857,plain,
~ join(X1,e,r1),
inference(rename_variables,[],[i_0_1825]) ).
cnf(i_0_1864,plain,
~ join(X1,e,r1),
inference(rename_variables,[],[i_0_1825]) ).
cnf(i_0_1874,plain,
~ join(e,X1,r1),
inference(rename_variables,[],[i_0_1823]) ).
cnf(i_0_1880,plain,
~ join(e,X1,r1),
inference(rename_variables,[],[i_0_1823]) ).
cnf(i_0_1934,plain,
~ join(X1,e,r1),
inference(rename_variables,[],[i_0_1825]) ).
cnf(i_0_2187,plain,
~ join(e,X1,r1),
inference(rename_variables,[],[i_0_1823]) ).
cnf(i_0_2238,plain,
~ join(X1,e,r1),
inference(rename_variables,[],[i_0_1825]) ).
cnf(i_0_1856,plain,
~ join(c2,b,r1),
inference(scs_inference,[],[i_0_1639,i_0_1783,i_0_1825,i_0_1844,i_0_1720,i_0_1791,i_0_1793,i_0_1818,i_0_1738,i_0_101,i_0_163,i_0_205,i_0_85,i_0_221,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1859,plain,
~ join(n0,n0,a2),
inference(scs_inference,[],[i_0_1639,i_0_1783,i_0_1825,i_0_1844,i_0_1720,i_0_1791,i_0_1793,i_0_1818,i_0_1738,i_0_1740,i_0_1618,i_0_101,i_0_163,i_0_205,i_0_85,i_0_45,i_0_48,i_0_221,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1863,plain,
~ meet(c2,b,r1),
inference(scs_inference,[],[i_0_1639,i_0_1783,i_0_1825,i_0_1844,i_0_1857,i_0_1720,i_0_1791,i_0_1793,i_0_1818,i_0_1738,i_0_1740,i_0_1774,i_0_1618,i_0_101,i_0_163,i_0_1804,i_0_205,i_0_85,i_0_45,i_0_48,i_0_221,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_1866,plain,
~ join(n0,a,b),
inference(scs_inference,[],[i_0_1841,i_0_728]) ).
cnf(i_0_1891,plain,
~ join(d,n0,n1),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_38,i_0_40]) ).
cnf(i_0_1893,plain,
~ meet(n0,X1,a2),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_1778,i_0_50,i_0_48,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1896,plain,
~ join(n1,X1,d),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_1778,i_0_49,i_0_51,i_0_50,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1899,plain,
~ meet(r2,c,a2),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_1778,i_0_1791,i_0_1774,i_0_101,i_0_49,i_0_51,i_0_50,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1913,plain,
~ meet(c,d,a2),
inference(scs_inference,[],[i_0_1850,i_0_38]) ).
cnf(i_0_1970,plain,
~ meet(a,e,a2),
inference(scs_inference,[],[i_0_1854,i_0_38]) ).
cnf(i_0_1867,plain,
~ meet(b,c2,r1),
inference(scs_inference,[],[i_0_1863,i_0_38]) ).
cnf(i_0_1869,plain,
~ join(a,n0,b),
inference(scs_inference,[],[i_0_1838,i_0_1863,i_0_38,i_0_40]) ).
cnf(i_0_1871,plain,
~ meet(r1,r2,r2),
inference(scs_inference,[],[i_0_1838,i_0_1863,i_0_1810,i_0_66,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1873,plain,
~ join(a2,c2,r1),
inference(scs_inference,[],[i_0_1838,i_0_1699,i_0_1863,i_0_1823,i_0_1810,i_0_219,i_0_66,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1876,plain,
~ meet(n1,d,r1),
inference(scs_inference,[],[i_0_1838,i_0_1699,i_0_1795,i_0_1863,i_0_1823,i_0_1810,i_0_219,i_0_1725,i_0_66,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1879,plain,
~ join(n0,c2,r1),
inference(scs_inference,[],[i_0_1838,i_0_1699,i_0_1795,i_0_1863,i_0_1823,i_0_1874,i_0_1810,i_0_1793,i_0_219,i_0_1725,i_0_66,i_0_45,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1883,plain,
~ join(d,d,r1),
inference(scs_inference,[],[i_0_1838,i_0_1699,i_0_1795,i_0_1863,i_0_1823,i_0_1874,i_0_1810,i_0_1793,i_0_219,i_0_1725,i_0_1687,i_0_66,i_0_45,i_0_43,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1886,plain,
~ meet(c2,a2,r1),
inference(scs_inference,[],[i_0_1838,i_0_1699,i_0_1795,i_0_1863,i_0_1823,i_0_1874,i_0_1810,i_0_1814,i_0_1793,i_0_219,i_0_1725,i_0_64,i_0_1687,i_0_1608,i_0_66,i_0_45,i_0_43,i_0_44,i_0_46,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_1925,plain,
~ join(n1,X1,d),
inference(rename_variables,[],[i_0_1896]) ).
cnf(i_0_1949,plain,
~ meet(n0,X1,a2),
inference(rename_variables,[],[i_0_1893]) ).
cnf(i_0_1972,plain,
~ join(b,c2,r1),
inference(scs_inference,[],[i_0_1854,i_0_1856,i_0_38,i_0_40]) ).
cnf(i_0_1980,plain,
~ meet(n0,X1,a2),
inference(rename_variables,[],[i_0_1893]) ).
cnf(i_0_2008,plain,
~ join(n1,X1,d),
inference(rename_variables,[],[i_0_1896]) ).
cnf(i_0_2152,plain,
~ join(n1,X1,d),
inference(rename_variables,[],[i_0_1896]) ).
cnf(i_0_2290,plain,
~ meet(n0,X1,a2),
inference(rename_variables,[],[i_0_1893]) ).
cnf(i_0_2610,plain,
~ join(n1,X1,d),
inference(rename_variables,[],[i_0_1896]) ).
cnf(i_0_1901,plain,
~ join(a,c,b),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_1778,i_0_1869,i_0_1791,i_0_1603,i_0_1774,i_0_101,i_0_49,i_0_51,i_0_50,i_0_48,i_0_47,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1904,plain,
~ join(c,c2,r1),
inference(scs_inference,[],[i_0_1840,i_0_1772,i_0_1778,i_0_1812,i_0_1852,i_0_1869,i_0_1791,i_0_1603,i_0_1774,i_0_101,i_0_49,i_0_51,i_0_50,i_0_48,i_0_47,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1907,plain,
~ meet(c2,b,n0),
inference(scs_inference,[],[i_0_1839,i_0_1840,i_0_1772,i_0_1778,i_0_1812,i_0_1852,i_0_1869,i_0_1710,i_0_1791,i_0_1603,i_0_1774,i_0_101,i_0_49,i_0_51,i_0_45,i_0_50,i_0_48,i_0_47,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_1911,plain,
~ meet(r1,n0,b),
inference(scs_inference,[],[i_0_1839,i_0_1840,i_0_1772,i_0_1778,i_0_1812,i_0_1852,i_0_1869,i_0_1710,i_0_1791,i_0_1603,i_0_1774,i_0_101,i_0_49,i_0_51,i_0_45,i_0_50,i_0_48,i_0_47,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_106]) ).
cnf(i_0_1915,plain,
~ join(c2,n0,r1),
inference(scs_inference,[],[i_0_1879,i_0_1850,i_0_38,i_0_40]) ).
cnf(i_0_1917,plain,
meet(r1,a,n0),
inference(scs_inference,[],[i_0_1879,i_0_1799,i_0_1850,i_0_62,i_0_48,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1920,plain,
~ join(n1,d,r1),
inference(scs_inference,[],[i_0_1879,i_0_1799,i_0_1850,i_0_1797,i_0_1873,i_0_1699,i_0_62,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1922,plain,
~ meet(d,n0,a2),
inference(scs_inference,[],[i_0_1879,i_0_1799,i_0_1850,i_0_1797,i_0_1873,i_0_1699,i_0_101,i_0_601,i_0_62,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1924,plain,
~ join(b,r2,d),
inference(scs_inference,[],[i_0_1879,i_0_1631,i_0_1722,i_0_1799,i_0_1850,i_0_1896,i_0_1797,i_0_1873,i_0_1699,i_0_101,i_0_601,i_0_62,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1996,plain,
~ meet(a2,c2,r1),
inference(scs_inference,[],[i_0_1886,i_0_38]) ).
cnf(i_0_2022,plain,
~ meet(r2,r1,r2),
inference(scs_inference,[],[i_0_1871,i_0_38]) ).
cnf(i_0_2045,plain,
~ meet(d,n1,r1),
inference(scs_inference,[],[i_0_1876,i_0_1660,i_0_151,i_0_38]) ).
cnf(i_0_1927,plain,
~ join(c,b,n0),
inference(scs_inference,[],[i_0_1879,i_0_1631,i_0_1722,i_0_1799,i_0_1850,i_0_1896,i_0_1797,i_0_1873,i_0_1907,i_0_1699,i_0_1651,i_0_1710,i_0_1774,i_0_101,i_0_601,i_0_62,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1929,plain,
~ meet(a2,e,d),
inference(scs_inference,[],[i_0_1879,i_0_1841,i_0_1631,i_0_1722,i_0_1799,i_0_1850,i_0_1896,i_0_1797,i_0_1873,i_0_1907,i_0_1699,i_0_1651,i_0_1710,i_0_1633,i_0_1774,i_0_101,i_0_601,i_0_62,i_0_45,i_0_48,i_0_1918,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_1933,plain,
~ meet(r1,X1,e),
inference(scs_inference,[],[i_0_1879,i_0_1841,i_0_1631,i_0_1722,i_0_1799,i_0_1850,i_0_1896,i_0_1797,i_0_1873,i_0_1907,i_0_1699,i_0_1825,i_0_1651,i_0_1710,i_0_1633,i_0_1774,i_0_101,i_0_601,i_0_62,i_0_45,i_0_48,i_0_1918,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_39]) ).
cnf(i_0_1936,plain,
~ join(a2,X1,r1),
inference(scs_inference,[],[i_0_1889,i_0_1879,i_0_1841,i_0_1631,i_0_1722,i_0_1799,i_0_1850,i_0_1896,i_0_1797,i_0_1873,i_0_1907,i_0_1699,i_0_1825,i_0_1651,i_0_1710,i_0_1633,i_0_1774,i_0_101,i_0_601,i_0_62,i_0_45,i_0_48,i_0_1918,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_39,i_0_37]) ).
cnf(i_0_1938,plain,
~ meet(n0,r1,b),
inference(scs_inference,[],[i_0_1911,i_0_38]) ).
cnf(i_0_1940,plain,
~ join(a,n0,e),
inference(scs_inference,[],[i_0_1842,i_0_1911,i_0_38,i_0_40]) ).
cnf(i_0_1942,plain,
~ meet(r1,a,b),
inference(scs_inference,[],[i_0_1842,i_0_1911,i_0_1917,i_0_42,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1945,plain,
~ join(n1,c,r1),
inference(scs_inference,[],[i_0_1842,i_0_1911,i_0_1936,i_0_1917,i_0_1639,i_0_1699,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1946,plain,
~ join(a2,X1,r1),
inference(rename_variables,[],[i_0_1936]) ).
cnf(i_0_1948,plain,
~ meet(r1,a,a2),
inference(scs_inference,[],[i_0_1842,i_0_1911,i_0_1893,i_0_1936,i_0_1917,i_0_1639,i_0_1738,i_0_1699,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1951,plain,
~ join(r1,r1,b2),
inference(scs_inference,[],[i_0_41,i_0_1842,i_0_1911,i_0_1893,i_0_1936,i_0_1917,i_0_1639,i_0_1738,i_0_1699,i_0_1608,i_0_43,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_31]) ).
cnf(i_0_1954,plain,
~ meet(n1,n1,r1),
inference(scs_inference,[],[i_0_41,i_0_1842,i_0_1911,i_0_1893,i_0_1936,i_0_1917,i_0_1920,i_0_1639,i_0_1738,i_0_1699,i_0_1608,i_0_49,i_0_43,i_0_44,i_0_46,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_31,i_0_32]) ).
cnf(i_0_1959,plain,
~ join(d,b2,r1),
inference(scs_inference,[],[i_0_41,i_0_1842,i_0_1911,i_0_1893,i_0_1936,i_0_1917,i_0_1920,i_0_1639,i_0_1738,i_0_1699,i_0_1608,i_0_49,i_0_43,i_0_44,i_0_46,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_31,i_0_32,i_0_154]) ).
cnf(i_0_1961,plain,
~ join(d,n0,r1),
inference(scs_inference,[],[i_0_41,i_0_1842,i_0_1911,i_0_1893,i_0_1936,i_0_1917,i_0_1920,i_0_1639,i_0_1738,i_0_1699,i_0_1608,i_0_49,i_0_43,i_0_44,i_0_46,i_0_42,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_31,i_0_32,i_0_154,i_0_192]) ).
cnf(i_0_1974,plain,
~ meet(n0,c2,e),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1856,i_0_1917,i_0_1738,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_1975,plain,
~ meet(r1,X1,e),
inference(rename_variables,[],[i_0_1933]) ).
cnf(i_0_1977,plain,
~ join(b2,c2,n0),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1856,i_0_1891,i_0_203,i_0_1917,i_0_489,i_0_1738,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_1979,plain,
~ meet(c,n0,a2),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1856,i_0_1891,i_0_1893,i_0_203,i_0_1641,i_0_1917,i_0_489,i_0_1738,i_0_1618,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_1982,plain,
~ join(n0,d,r1),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1856,i_0_1883,i_0_1891,i_0_1893,i_0_203,i_0_1641,i_0_1917,i_0_489,i_0_1738,i_0_1618,i_0_45,i_0_43,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_1987,plain,
~ meet(r1,X1,e),
inference(rename_variables,[],[i_0_1933]) ).
cnf(i_0_2112,plain,
~ meet(e,a2,d),
inference(scs_inference,[],[i_0_1929,i_0_38]) ).
cnf(i_0_2511,plain,
~ meet(r1,X1,e),
inference(rename_variables,[],[i_0_1933]) ).
cnf(i_0_2541,plain,
~ join(a2,X1,r1),
inference(rename_variables,[],[i_0_1936]) ).
cnf(i_0_1966,plain,
~ join(d,a,c),
inference(scs_inference,[],[i_0_1959,i_0_1103]) ).
cnf(i_0_1967,plain,
~ join(d,r2,c),
inference(scs_inference,[],[i_0_1959,i_0_1114]) ).
cnf(i_0_1968,plain,
~ join(d,a,n0),
inference(scs_inference,[],[i_0_1959,i_0_1334]) ).
cnf(i_0_1969,plain,
~ join(d,r2,n0),
inference(scs_inference,[],[i_0_1959,i_0_1346]) ).
cnf(i_0_1986,plain,
~ join(n0,r1,e),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1975,i_0_1856,i_0_1883,i_0_1891,i_0_1893,i_0_203,i_0_1641,i_0_1917,i_0_489,i_0_1738,i_0_1618,i_0_51,i_0_45,i_0_43,i_0_44,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_1992,plain,
~ meet(c2,a,b),
inference(scs_inference,[],[i_0_1854,i_0_1933,i_0_1975,i_0_1856,i_0_1883,i_0_1891,i_0_1901,i_0_1893,i_0_203,i_0_1641,i_0_1917,i_0_1603,i_0_489,i_0_1738,i_0_1618,i_0_1774,i_0_51,i_0_45,i_0_43,i_0_44,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2180,plain,
~ meet(a,r1,a2),
inference(scs_inference,[],[i_0_1948,i_0_38]) ).
cnf(i_0_1994,plain,
~ join(a,r2,b),
inference(scs_inference,[],[i_0_1966,i_0_325]) ).
cnf(i_0_1995,plain,
~ join(d,n1,b),
inference(scs_inference,[],[i_0_1966,i_0_1225]) ).
cnf(i_0_1998,plain,
~ join(a,d,c),
inference(scs_inference,[],[i_0_1966,i_0_1886,i_0_38,i_0_40]) ).
cnf(i_0_2000,plain,
meet(c2,c,c),
inference(scs_inference,[],[i_0_1966,i_0_1886,i_0_1799,i_0_612,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2002,plain,
~ join(b,e,n0),
inference(scs_inference,[],[i_0_1966,i_0_1886,i_0_1927,i_0_1685,i_0_1799,i_0_1651,i_0_612,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_2004,plain,
~ meet(n1,a,b),
inference(scs_inference,[],[i_0_1966,i_0_1886,i_0_1992,i_0_1927,i_0_1685,i_0_1799,i_0_1651,i_0_612,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_2007,plain,
~ join(r2,c2,d),
inference(scs_inference,[],[i_0_1966,i_0_1717,i_0_1886,i_0_1992,i_0_1927,i_0_1685,i_0_1776,i_0_1896,i_0_1799,i_0_1651,i_0_612,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_2010,plain,
~ join(n1,n1,r1),
inference(scs_inference,[],[i_0_1966,i_0_1717,i_0_1886,i_0_1992,i_0_1927,i_0_1954,i_0_1685,i_0_1776,i_0_1896,i_0_1799,i_0_1651,i_0_612,i_0_49,i_0_44,i_0_2005,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_2014,plain,
~ meet(c2,b,a),
inference(scs_inference,[],[i_0_1866,i_0_1966,i_0_1717,i_0_1886,i_0_1992,i_0_1927,i_0_1954,i_0_1685,i_0_1776,i_0_1896,i_0_1799,i_0_1651,i_0_1710,i_0_612,i_0_49,i_0_45,i_0_44,i_0_2005,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2018,plain,
~ join(n0,r1,b2),
inference(scs_inference,[],[i_0_1866,i_0_1966,i_0_1717,i_0_1886,i_0_1992,i_0_1927,i_0_1954,i_0_1685,i_0_1776,i_0_1896,i_0_1799,i_0_1651,i_0_1710,i_0_612,i_0_1608,i_0_49,i_0_45,i_0_44,i_0_2005,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_134]) ).
cnf(i_0_2024,plain,
~ join(r2,d,c),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_38,i_0_40]) ).
cnf(i_0_2026,plain,
~ meet(n0,a,b),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1942,i_0_1799,i_0_62,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2028,plain,
~ join(r2,e,c),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1942,i_0_1631,i_0_1610,i_0_1799,i_0_62,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_2030,plain,
~ meet(n1,n0,a2),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1899,i_0_1942,i_0_1631,i_0_1610,i_0_1799,i_0_101,i_0_62,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_2033,plain,
~ join(r2,b,r1),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1899,i_0_1942,i_0_1945,i_0_1631,i_0_1693,i_0_1658,i_0_1610,i_0_1799,i_0_101,i_0_62,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_2047,plain,
~ join(a,d,n0),
inference(scs_inference,[],[i_0_1968,i_0_1876,i_0_1660,i_0_151,i_0_38,i_0_40]) ).
cnf(i_0_2049,plain,
~ meet(b,n1,r1),
inference(scs_inference,[],[i_0_1968,i_0_1867,i_0_1876,i_0_1660,i_0_1710,i_0_46,i_0_151,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2020,plain,
~ join(a,r2,b),
inference(scs_inference,[],[i_0_1998,i_0_322]) ).
cnf(i_0_2021,plain,
~ join(d,n1,b),
inference(scs_inference,[],[i_0_1998,i_0_1228]) ).
cnf(i_0_2035,plain,
~ join(e,b,a),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1899,i_0_1942,i_0_1945,i_0_2014,i_0_1631,i_0_1693,i_0_1729,i_0_1658,i_0_1610,i_0_1799,i_0_1710,i_0_1804,i_0_101,i_0_62,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_2037,plain,
~ meet(a2,e,r1),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1899,i_0_1942,i_0_1945,i_0_1986,i_0_2014,i_0_1631,i_0_1693,i_0_1729,i_0_1658,i_0_1610,i_0_1633,i_0_1799,i_0_1710,i_0_1804,i_0_101,i_0_62,i_0_45,i_0_44,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2041,plain,
~ join(a2,X1,n0),
inference(scs_inference,[],[i_0_1967,i_0_1871,i_0_1899,i_0_1942,i_0_1945,i_0_1986,i_0_2014,i_0_1631,i_0_1693,i_0_1778,i_0_1729,i_0_1658,i_0_1610,i_0_1633,i_0_1799,i_0_1710,i_0_1804,i_0_101,i_0_62,i_0_45,i_0_44,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_37]) ).
cnf(i_0_2052,plain,
~ join(b2,c2,b),
inference(scs_inference,[],[i_0_1968,i_0_1995,i_0_1867,i_0_1876,i_0_203,i_0_489,i_0_1660,i_0_1710,i_0_46,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_2054,plain,
~ meet(c2,n0,a2),
inference(scs_inference,[],[i_0_1968,i_0_1995,i_0_1867,i_0_1876,i_0_2000,i_0_1740,i_0_203,i_0_1641,i_0_489,i_0_1660,i_0_1710,i_0_46,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_2056,plain,
~ join(n0,r2,n0),
inference(scs_inference,[],[i_0_1968,i_0_1969,i_0_1995,i_0_1867,i_0_1876,i_0_2000,i_0_1740,i_0_203,i_0_1641,i_0_1610,i_0_489,i_0_1660,i_0_1710,i_0_45,i_0_46,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_2059,plain,
~ join(b,b,r1),
inference(scs_inference,[],[i_0_1968,i_0_1969,i_0_1995,i_0_1867,i_0_1876,i_0_2000,i_0_1863,i_0_1740,i_0_203,i_0_1641,i_0_1610,i_0_489,i_0_1660,i_0_1710,i_0_45,i_0_43,i_0_46,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_2062,plain,
~ meet(n1,a2,n0),
inference(scs_inference,[],[i_0_1968,i_0_1969,i_0_1995,i_0_1859,i_0_1867,i_0_1876,i_0_2000,i_0_1863,i_0_1740,i_0_203,i_0_1641,i_0_1610,i_0_489,i_0_1660,i_0_1710,i_0_51,i_0_45,i_0_43,i_0_48,i_0_46,i_0_2050,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2067,plain,
~ meet(n0,X1,r2),
inference(scs_inference,[],[i_0_1968,i_0_1969,i_0_1995,i_0_1859,i_0_1867,i_0_1876,i_0_2000,i_0_1863,i_0_1740,i_0_203,i_0_1641,i_0_1610,i_0_489,i_0_1660,i_0_1710,i_0_51,i_0_45,i_0_43,i_0_48,i_0_46,i_0_2050,i_0_151,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32,i_0_39]) ).
cnf(i_0_2399,plain,
~ meet(a,n1,b),
inference(scs_inference,[],[i_0_2004,i_0_38]) ).
cnf(i_0_2439,plain,
~ meet(n1,b,r1),
inference(scs_inference,[],[i_0_2049,i_0_38]) ).
cnf(i_0_2069,plain,
~ meet(X1,n0,r2),
inference(scs_inference,[],[i_0_2067,i_0_38]) ).
cnf(i_0_2071,plain,
~ join(r2,a,b),
inference(scs_inference,[],[i_0_1994,i_0_2067,i_0_38,i_0_40]) ).
cnf(i_0_2073,plain,
~ meet(a,c2,b),
inference(scs_inference,[],[i_0_1994,i_0_2067,i_0_1992,i_0_1799,i_0_1738,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2075,plain,
~ join(c2,d,r1),
inference(scs_inference,[],[i_0_1994,i_0_1904,i_0_2067,i_0_1992,i_0_1797,i_0_1852,i_0_1799,i_0_1738,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_2077,plain,
~ meet(r1,c,r2),
inference(scs_inference,[],[i_0_1994,i_0_1904,i_0_2067,i_0_1992,i_0_1797,i_0_2000,i_0_1852,i_0_1799,i_0_1738,i_0_62,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_2078,plain,
~ meet(n0,X1,r2),
inference(rename_variables,[],[i_0_2067]) ).
cnf(i_0_2080,plain,
~ join(r2,c2,r1),
inference(scs_inference,[],[i_0_1994,i_0_1904,i_0_2067,i_0_1717,i_0_1992,i_0_1797,i_0_1920,i_0_2000,i_0_1852,i_0_1799,i_0_1738,i_0_62,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_2083,plain,
~ meet(n0,X1,r2),
inference(rename_variables,[],[i_0_2067]) ).
cnf(i_0_2326,plain,
~ join(a2,X1,n0),
inference(rename_variables,[],[i_0_2041]) ).
cnf(i_0_2332,plain,
~ join(a2,X1,n0),
inference(rename_variables,[],[i_0_2041]) ).
cnf(i_0_2374,plain,
~ meet(a2,n1,n0),
inference(scs_inference,[],[i_0_2062,i_0_38]) ).
cnf(i_0_2381,plain,
~ meet(n0,X1,r2),
inference(rename_variables,[],[i_0_2067]) ).
cnf(i_0_2082,plain,
~ join(n0,n0,r2),
inference(scs_inference,[],[i_0_1994,i_0_1904,i_0_2067,i_0_2078,i_0_1717,i_0_1992,i_0_1797,i_0_1920,i_0_2000,i_0_1852,i_0_1799,i_0_1738,i_0_62,i_0_51,i_0_50,i_0_44,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_2088,plain,
~ meet(b2,n1,r1),
inference(scs_inference,[],[i_0_1994,i_0_1904,i_0_2067,i_0_2078,i_0_1951,i_0_1717,i_0_1992,i_0_1797,i_0_1920,i_0_2000,i_0_1852,i_0_207,i_0_1799,i_0_1738,i_0_62,i_0_51,i_0_50,i_0_44,i_0_2086,i_0_46,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2097,plain,
~ meet(X1,n0,r2),
inference(rename_variables,[],[i_0_2069]) ).
cnf(i_0_2247,plain,
~ meet(X1,n0,r2),
inference(rename_variables,[],[i_0_2069]) ).
cnf(i_0_2487,plain,
~ meet(c,r1,r2),
inference(scs_inference,[],[i_0_2077,i_0_38]) ).
cnf(i_0_2092,plain,
~ meet(n1,b2,r1),
inference(scs_inference,[],[i_0_2088,i_0_38]) ).
cnf(i_0_2094,plain,
~ join(b,e,a),
inference(scs_inference,[],[i_0_2035,i_0_2088,i_0_38,i_0_40]) ).
cnf(i_0_2096,plain,
~ meet(r1,a,r2),
inference(scs_inference,[],[i_0_2035,i_0_2088,i_0_2069,i_0_1917,i_0_1702,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2099,plain,
~ join(c2,c,r1),
inference(scs_inference,[],[i_0_2035,i_0_1972,i_0_2088,i_0_2069,i_0_1639,i_0_1917,i_0_1702,i_0_163,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(i_0_2101,plain,
~ meet(b2,r1,d),
inference(scs_inference,[],[i_0_2035,i_0_1972,i_0_2088,i_0_2069,i_0_1768,i_0_1639,i_0_1917,i_0_1702,i_0_163,i_0_1608,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34]) ).
cnf(i_0_2103,plain,
~ join(n0,b,a),
inference(scs_inference,[],[i_0_2035,i_0_1972,i_0_2088,i_0_2069,i_0_1768,i_0_1639,i_0_1729,i_0_1917,i_0_1702,i_0_163,i_0_1608,i_0_45,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36]) ).
cnf(i_0_2106,plain,
~ join(c,a,b),
inference(scs_inference,[],[i_0_2035,i_0_1972,i_0_2088,i_0_2069,i_0_1768,i_0_2073,i_0_1639,i_0_1852,i_0_1729,i_0_1917,i_0_1702,i_0_163,i_0_1799,i_0_1608,i_0_609,i_0_45,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31]) ).
cnf(i_0_2108,plain,
~ meet(a,r1,r2),
inference(scs_inference,[],[i_0_2035,i_0_2056,i_0_1972,i_0_2088,i_0_2069,i_0_1768,i_0_2073,i_0_1639,i_0_1852,i_0_1729,i_0_1917,i_0_1702,i_0_163,i_0_1799,i_0_1608,i_0_609,i_0_45,i_0_2104,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35,i_0_34,i_0_36,i_0_31,i_0_32]) ).
cnf(i_0_2114,plain,
~ join(b,n0,a),
inference(scs_inference,[],[i_0_2103,i_0_1929,i_0_38,i_0_40]) ).
cnf(i_0_2116,plain,
~ meet(n0,X1,d),
inference(scs_inference,[],[i_0_2103,i_0_1929,i_0_1616,i_0_50,i_0_48,i_0_38,i_0_40,i_0_33]) ).
cnf(i_0_2119,plain,
~ join(r2,d,n0),
inference(scs_inference,[],[i_0_2082,i_0_2103,i_0_1929,i_0_1736,i_0_1616,i_0_45,i_0_50,i_0_48,i_0_38,i_0_40,i_0_33,i_0_35]) ).
cnf(c_0_1817,axiom,
( join(X1,X2,X3)
| ~ join(X2,X1,X3) ),
i_0_40 ).
cnf(c_0_1818,plain,
join(c2,d,c2),
i_0_1797 ).
cnf(c_0_1819,axiom,
( meet(X1,X2,X3)
| ~ meet(X4,X1,X4)
| ~ join(X4,X5,X2)
| ~ meet(X5,X1,X6)
| ~ join(X4,X6,X3) ),
i_0_31 ).
cnf(c_0_1820,axiom,
join(X1,n0,X1),
i_0_47 ).
cnf(c_0_1821,axiom,
( meet(X1,X2,X3)
| ~ meet(X2,X1,X3) ),
i_0_38 ).
cnf(c_0_1822,negated_conjecture,
meet(c2,r1,n0),
i_0_52 ).
cnf(c_0_1823,axiom,
( meet(X1,X2,X1)
| ~ join(X1,X3,X2) ),
i_0_37 ).
cnf(c_0_1824,plain,
join(d,c2,c2),
inference(spm,[status(thm)],[c_0_1817,c_0_1818]) ).
cnf(c_0_1825,plain,
( meet(X1,X2,X3)
| ~ join(X3,X4,X2)
| ~ meet(X4,X1,n0)
| ~ meet(X3,X1,X3) ),
inference(spm,[status(thm)],[c_0_1819,c_0_1820]) ).
cnf(c_0_1826,negated_conjecture,
meet(r1,c2,n0),
inference(spm,[status(thm)],[c_0_1821,c_0_1822]) ).
cnf(c_0_1827,negated_conjecture,
join(r1,e,a2),
i_0_61 ).
cnf(c_0_1828,axiom,
( meet(X1,X2,X3)
| ~ meet(X1,X4,X5)
| ~ meet(X4,X6,X2)
| ~ meet(X5,X6,X3) ),
i_0_33 ).
cnf(c_0_1829,plain,
meet(e,d,n0),
i_0_876 ).
cnf(c_0_1830,plain,
meet(d,c2,d),
inference(spm,[status(thm)],[c_0_1823,c_0_1824]) ).
cnf(c_0_1831,negated_conjecture,
( meet(c2,X1,X2)
| ~ join(X2,r1,X1)
| ~ meet(X2,c2,X2) ),
inference(spm,[status(thm)],[c_0_1825,c_0_1826]) ).
cnf(c_0_1832,negated_conjecture,
join(e,r1,a2),
inference(spm,[status(thm)],[c_0_1817,c_0_1827]) ).
cnf(c_0_1833,plain,
meet(e,c2,e),
i_0_1804 ).
cnf(c_0_1834,plain,
( meet(X1,X2,n0)
| ~ meet(X3,d,X2)
| ~ meet(X1,X3,e) ),
inference(spm,[status(thm)],[c_0_1828,c_0_1829]) ).
cnf(c_0_1835,plain,
meet(c2,d,d),
inference(spm,[status(thm)],[c_0_1821,c_0_1830]) ).
cnf(c_0_1836,negated_conjecture,
meet(c2,a2,e),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1831,c_0_1832]),c_0_1833])]) ).
cnf(c_0_1837,plain,
( meet(X1,d,n0)
| ~ meet(X1,c2,e) ),
inference(spm,[status(thm)],[c_0_1834,c_0_1835]) ).
cnf(c_0_1838,negated_conjecture,
meet(a2,c2,e),
inference(spm,[status(thm)],[c_0_1821,c_0_1836]) ).
cnf(c_0_1839,plain,
~ meet(a2,d,n0),
i_0_1616 ).
cnf(c_0_1840,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1837,c_0_1838]),c_0_1839]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LAT005-2 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n025.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Mon May 4 20:45:13 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 194.20/85.99 % Version : CSE_E---1.7
% 194.20/85.99 % Problem : theBenchmark.p
% 194.20/85.99 % SZS status Unsatisfiable for theBenchmark.p
% 194.20/85.99 % SZS output start CNFRefutation
% See solution above
% 197.50/89.22 % Total time : 84.706s
%------------------------------------------------------------------------------