%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYN231-1 : TPTP v9.2.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n009.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 05:36:31 PM UTC 2026
% Result : Unsatisfiable 0.42s 1.61s
% Output : CNFRefutation 1.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN231-1 : TPTP v9.2.1. Released v1.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n009.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 : Tue May 5 08:21:56 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.42/1.61 % Version : CSE_E---1.7
% 0.42/1.61 % Problem : theBenchmark.p
% 0.42/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.42/1.61 % SZS output start CNFRefutation
% 0.42/1.61 cnf(rule_096, axiom, (q1(X1,X1,X1)|~n1(X2,X3,X3)|~p0(X2,X4)|~m1(X1,X3,X2)|~q1(X4,X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_096)).
% 0.42/1.61 cnf(rule_182, axiom, (q2(X1,X2,X1)|~p1(X1,X1,X3)|~n1(X2,X1,X3)|~q2(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_182)).
% 0.42/1.61 cnf(rule_051, axiom, (n1(X1,X1,X1)|~m1(c,X1,X2)|~m0(b,X2,c)|~n1(X2,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_051)).
% 0.42/1.61 cnf(rule_162, axiom, (p2(b,c,c)|~p1(X1,b,b)|~n1(e,e,X1)|~q1(e,c,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_162)).
% 0.42/1.61 cnf(rule_295, axiom, (q4(X1,X2)|~k3(X3,X3,X1)|~q2(X4,X2,X1)|~m3(X4,X5,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_295)).
% 0.42/1.61 cnf(rule_128, axiom, (k2(X1,X1)|~n1(e,d,X1)|~m1(X1,e,X1)|~q1(X1,X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_128)).
% 0.42/1.61 cnf(rule_225, axiom, (m3(X1,X2,X1)|~m0(X3,X3,X2)|~l2(X4,X1)|~m0(X1,X4,X4)|~s2(X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_225)).
% 0.42/1.61 cnf(rule_292, axiom, (p4(X1,X1,X1)|~k3(X2,X3,X3)|~n4(X1,X3)|~p1(X3,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_292)).
% 0.42/1.61 cnf(rule_262, axiom, (r3(X1,X1,X1)|~p1(X2,X3,X1)|~l2(X3,X2)|~r3(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_262)).
% 0.42/1.61 cnf(rule_146, axiom, (p2(X1,X2,X2)|~p1(X1,X3,X4)|~l1(X3,X4)|~p2(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_146)).
% 0.42/1.61 cnf(rule_152, axiom, (p2(X1,X2,X2)|~n1(X3,X2,X3)|~p0(X1,X2)|~p2(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_152)).
% 0.42/1.61 cnf(rule_138, axiom, (n2(a)|~m1(b,a,e)|~k1(c)|~n1(e,a,e)|~q1(c,a,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_138)).
% 0.42/1.61 cnf(rule_187, axiom, (q2(X1,X2,X1)|~r1(X2)|~m0(X3,X4,X1)|~k0(X2)|~q2(X2,X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_187)).
% 0.42/1.61 cnf(rule_024, axiom, (m1(X1,a,X2)|~m0(a,X3,a)|~q0(X1,X2)|~m1(X2,c,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_024)).
% 0.42/1.61 cnf(rule_269, axiom, (r3(a,a,e)|~k2(a,a)|~q2(X1,e,X1)|~m2(b)|~m3(a,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_269)).
% 0.42/1.61 cnf(rule_243, axiom, (p3(X1,d,e)|~l3(b,e)|~p2(d,b,c)|~n3(X1)|~q2(X1,d,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_243)).
% 0.42/1.61 cnf(rule_158, axiom, (p2(X1,X1,X2)|~q1(c,X1,X3)|~s1(c)|~s0(e)|~p2(X1,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_158)).
% 0.42/1.61 cnf(rule_268, axiom, (r3(X1,X1,X2)|~m2(X2)|~m3(X3,b,X1)|~r3(X2,X4,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_268)).
% 0.42/1.61 cnf(rule_185, axiom, (q2(X1,X1,X1)|~n1(X2,d,X3)|~k1(X1)|~q2(X3,X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_185)).
% 0.42/1.61 cnf(rule_200, axiom, (k3(X1,X1,X1)|~p2(X2,X3,e)|~s1(X2)|~k3(X1,X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_200)).
% 0.42/1.61 cnf(rule_290, axiom, (p4(X1,X1,X1)|~m3(X2,X3,X1)|~p4(X1,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_290)).
% 0.42/1.61 cnf(rule_288, axiom, (p4(X1,X2,X2)|~r3(X2,X2,X1)|~p4(X3,X3,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_288)).
% 0.42/1.61 cnf(rule_271, axiom, (r3(X1,X1,X1)|~p3(X2,X1,X3)|~r3(X2,X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_271)).
% 0.42/1.61 cnf(rule_251, axiom, (p3(X1,X2,X2)|~m3(X2,X3,X4)|~p2(X1,X2,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_251)).
% 0.42/1.61 cnf(rule_196, axiom, (k3(X1,X1,X1)|~p2(X2,X3,X2)|~m1(X1,X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_196)).
% 0.42/1.61 cnf(rule_165, axiom, (p2(X1,X1,X1)|~q1(X2,X3,X2)|~p2(X2,X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_165)).
% 0.42/1.61 cnf(rule_169, axiom, (p2(X1,X1,X1)|~q1(X2,X2,X2)|~p1(X1,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_169)).
% 0.42/1.61 cnf(rule_148, axiom, (p2(X1,X1,X1)|~m1(X2,X3,X1)|~p2(X2,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_148)).
% 0.42/1.61 cnf(rule_082, axiom, (p1(X1,X2,X3)|~m0(X3,X1,X4)|~p1(X3,X1,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_082)).
% 0.42/1.61 cnf(rule_062, axiom, (n1(X1,X1,X1)|~m0(X2,X2,X3)|~n1(X2,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_062)).
% 0.42/1.61 cnf(rule_059, axiom, (n1(X1,X1,X2)|~m0(X3,X4,X4)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_059)).
% 0.42/1.61 cnf(rule_016, axiom, (m1(X1,X2,X2)|~m1(X3,X2,X1)|~m1(X3,X4,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_016)).
% 0.42/1.61 cnf(rule_263, axiom, (r3(X1,X1,X1)|~m0(d,X2,X1)|~r3(X1,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_263)).
% 0.42/1.61 cnf(rule_160, axiom, (p2(X1,X1,X1)|~m1(a,a,X2)|~p2(a,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_160)).
% 0.42/1.61 cnf(rule_107, axiom, (q1(e,X1,X1)|~m0(X1,d,X1)|~m0(e,d,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_107)).
% 0.42/1.61 cnf(rule_156, axiom, (p2(X1,e,X2)|~n1(e,X1,a)|~q1(a,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_156)).
% 0.42/1.61 cnf(rule_254, axiom, (p3(e,b,e)|~m3(e,X1,e)|~q2(X1,X1,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_254)).
% 0.42/1.61 cnf(rule_134, axiom, (l2(X1,X1)|~m0(X2,X1,X3)|~m1(X3,X2,X2)|~p0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_134)).
% 0.42/1.61 cnf(rule_111, axiom, (q1(d,d,c)|~m0(c,b,a)|~m1(c,d,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_111)).
% 0.42/1.61 cnf(rule_226, axiom, (m3(X1,X1,X1)|~k2(X2,X3)|~m3(X1,X3,X1)|~n0(X3,a)|~l2(a,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_226)).
% 0.42/1.61 cnf(rule_273, axiom, (s3(X1,X2)|~q2(X3,X1,X3)|~s2(X1)|~m0(X3,X4,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_273)).
% 0.42/1.61 cnf(rule_276, axiom, (k4(e)|~q3(X1,X1)|~q1(a,a,X2)|~r3(X1,e,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_276)).
% 0.42/1.61 cnf(rule_316, axiom, (n5(X1,X1)|~p4(X2,X1,X1)|~s1(X1)|~p4(b,b,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_316)).
% 0.42/1.61 cnf(rule_216, axiom, (l3(X1,X1)|~p1(X1,X1,X2)|~p2(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_216)).
% 0.42/1.61 cnf(rule_319, axiom, (p5(X1,X2,X2)|~l2(X1,X3)|~p5(X1,X3,X1)|~m4(X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_319)).
% 0.42/1.61 cnf(rule_245, axiom, (p3(X1,X1,X1)|~l1(X2,X2)|~l3(X2,X1)|~p3(X3,X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_245)).
% 0.42/1.61 cnf(rule_202, axiom, (k3(X1,X1,X2)|~q0(X3,X2)|~k2(X1,X4)|~k3(X2,X5,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_202)).
% 0.42/1.61 cnf(rule_209, axiom, (k3(X1,X1,X1)|~m2(X2)|~l1(X3,X4)|~s2(X1)|~k3(X3,X4,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_209)).
% 0.42/1.61 cnf(rule_052, axiom, (n1(X1,X1,X1)|~m0(X2,X2,X2)|~k1(X1)|~s0(X1)|~p0(X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_052)).
% 0.42/1.61 cnf(rule_144, axiom, (p2(b,c,a)|~r0(e)|~n1(c,X1,X1)|~p0(b,X1)|~k2(c,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_144)).
% 0.42/1.61 cnf(rule_108, axiom, (q1(X1,X1,X1)|~p0(X2,X3)|~p1(X1,b,b)|~q0(b,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_108)).
% 0.42/1.61 cnf(rule_289, axiom, (p4(X1,X1,X1)|~l4(X1)|~n0(X1,X2)|~p4(X3,X4,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_289)).
% 0.42/1.61 cnf(rule_261, axiom, (r3(X1,X1,X1)|~l1(X2,X3)|~n1(X3,X3,X3)|~r2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_261)).
% 0.42/1.61 cnf(rule_272, axiom, (r3(X1,X2,X3)|~k2(X2,X3)|~r2(X3)|~r3(X3,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_272)).
% 0.42/1.61 cnf(rule_192, axiom, (k3(X1,X2,X1)|~s1(X2)|~p2(X3,X2,X4)|~n0(X1,X4)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_192)).
% 0.42/1.61 cnf(rule_164, axiom, (p2(X1,X1,X1)|~p0(X1,X1)|~r1(X2)|~p2(X3,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_164)).
% 0.42/1.61 cnf(rule_091, axiom, (p1(X1,X1,X1)|~q0(X2,X3)|~k1(X4)|~n1(X2,X1,X5)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_091)).
% 0.42/1.61 cnf(rule_080, axiom, (p1(X1,X1,X1)|~n0(X2,X2)|~l0(X3)|~n1(X2,X4,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_080)).
% 0.42/1.61 cnf(rule_081, axiom, (p1(X1,X1,X1)|~m1(X2,X3,X1)|~q0(X3,X4)|~l0(X5)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_081)).
% 0.42/1.61 cnf(rule_042, axiom, (n1(X1,X1,X1)|~m0(X2,X3,X2)|~k0(X1)|~q0(X4,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_042)).
% 0.42/1.61 cnf(rule_054, axiom, (n1(X1,X2,X2)|~l0(X3)|~l1(X3,X1)|~n1(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_054)).
% 0.42/1.61 cnf(rule_168, axiom, (p2(a,c,b)|~l1(e,c)|~l2(e,b)|~r1(e)|~m1(d,a,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_168)).
% 0.42/1.61 cnf(rule_282, axiom, (n4(d,d)|~k3(c,c,e)|~q1(d,d,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_282)).
% 0.42/1.61 cnf(rule_307, axiom, (n5(X1,X2)|~q4(X3,X4)|~n4(X1,X4)|~p4(X5,X5,X2)|~n5(X5,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_307)).
% 0.42/1.61 cnf(rule_089, axiom, (p1(d,d,X1)|~s0(X1)|~n1(c,d,X1)|~r0(d)|~n0(c,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_089)).
% 0.42/1.61 cnf(rule_270, axiom, (r3(X1,b,X1)|~r0(X1)|~p2(b,X1,b)|~l2(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_270)).
% 0.42/1.61 cnf(rule_101, axiom, (q1(X1,X1,X1)|~k1(X1)|~q0(X1,b)|~p1(b,b,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_101)).
% 0.42/1.61 cnf(rule_178, axiom, (q2(X1,X1,X1)|~q0(X2,X1)|~n1(X2,X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_178)).
% 0.42/1.61 cnf(rule_171, axiom, (p2(X1,X1,X1)|~n1(X2,X2,X2)|~p0(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_171)).
% 0.42/1.61 cnf(rule_033, axiom, (m1(X1,X1,X1)|~q0(X2,X2)|~m1(X3,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_033)).
% 0.42/1.61 cnf(rule_118, axiom, (q1(X1,X1,X1)|~p0(b,d)|~s0(b)|~n1(X2,d,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_118)).
% 0.42/1.61 cnf(rule_241, axiom, (p3(X1,X2,X3)|~q2(X4,d,X1)|~k2(X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_241)).
% 0.42/1.61 cnf(rule_163, axiom, (p2(X1,X1,X1)|~q1(X2,c,X2)|~k2(X1,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_163)).
% 0.42/1.61 cnf(rule_084, axiom, (p1(X1,X1,X1)|~m0(b,X2,b)|~l1(X1,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_084)).
% 0.42/1.61 cnf(rule_247, axiom, (p3(X1,X1,X1)|~n2(X1)|~q2(X2,X3,X1)|~s1(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_247)).
% 0.42/1.61 cnf(rule_228, axiom, (m3(X1,X2,X2)|~n2(X1)|~m2(X2)|~m3(X3,X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_228)).
% 0.42/1.61 cnf(rule_201, axiom, (k3(X1,X1,X2)|~p1(X2,X3,X1)|~m2(X4)|~m2(X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_201)).
% 0.42/1.61 cnf(rule_099, axiom, (q1(X1,X2,X2)|~k0(X3)|~l0(X1)|~q1(X2,X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_099)).
% 0.42/1.61 cnf(rule_028, axiom, (m1(X1,X1,X1)|~l0(X1)|~k0(X1)|~m0(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_028)).
% 0.42/1.61 cnf(rule_166, axiom, (p2(a,X1,d)|~n0(X1,d)|~m1(a,X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_166)).
% 0.42/1.61 cnf(rule_071, axiom, (p1(X1,X2,X1)|~l0(X3)|~p1(X2,X4,X1)|~s0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_071)).
% 0.42/1.61 cnf(rule_230, axiom, (m3(c,b,d)|~l1(d,b)|~m2(d)|~q2(b,c,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_230)).
% 0.42/1.61 cnf(rule_203, axiom, (k3(d,d,d)|~p1(a,d,b)|~r2(a)|~l2(e,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_203)).
% 0.42/1.61 cnf(rule_180, axiom, (q2(d,a,a)|~q2(d,c,a)|~s1(c)|~q0(e,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_180)).
% 0.42/1.61 cnf(rule_055, axiom, (n1(d,e,e)|~p0(d,d)|~n1(e,e,e)|~r0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_055)).
% 0.42/1.61 cnf(rule_060, axiom, (n1(d,d,b)|~q0(b,e)|~m1(d,e,e)|~k0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_060)).
% 0.42/1.61 cnf(rule_193, axiom, (k3(X1,X1,X1)|~s1(X1)|~q2(d,X2,d)|~s2(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_193)).
% 0.42/1.61 cnf(rule_285, axiom, (p4(X1,X1,X2)|~r0(X1)|~r3(X2,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_285)).
% 0.42/1.61 cnf(rule_248, axiom, (p3(X1,X1,X1)|~p2(X2,X1,X1)|~n3(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_248)).
% 0.42/1.61 cnf(rule_250, axiom, (p3(X1,X1,X1)|~k1(X1)|~q2(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_250)).
% 0.42/1.61 cnf(rule_242, axiom, (p3(X1,X2,X3)|~r2(X2)|~k3(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_242)).
% 0.42/1.61 cnf(rule_235, axiom, (m3(X1,X1,X2)|~r2(X2)|~k3(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_235)).
% 0.42/1.61 cnf(rule_213, axiom, (k3(X1,X1,X1)|~r1(X1)|~p2(X2,X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_213)).
% 0.42/1.61 cnf(rule_179, axiom, (q2(X1,X1,X1)|~k1(X2)|~n1(X1,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_179)).
% 0.42/1.61 cnf(rule_177, axiom, (q2(X1,X2,X2)|~k0(X2)|~p1(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_177)).
% 0.42/1.61 cnf(rule_114, axiom, (q1(X1,X1,X1)|~m0(X1,X1,X2)|~k0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_114)).
% 0.42/1.61 cnf(rule_098, axiom, (q1(X1,X1,X1)|~s0(X1)|~m0(X2,X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_098)).
% 0.42/1.61 cnf(rule_113, axiom, (q1(X1,X1,X2)|~r0(X3)|~m1(X1,X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_113)).
% 0.42/1.61 cnf(rule_086, axiom, (p1(X1,X1,X1)|~l0(X1)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_086)).
% 0.42/1.61 cnf(rule_046, axiom, (n1(X1,X1,X1)|~m1(X2,X3,X1)|~k0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_046)).
% 0.42/1.61 cnf(rule_015, axiom, (m1(X1,X2,X2)|~l0(X3)|~m0(X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_015)).
% 0.42/1.61 cnf(rule_143, axiom, (p2(c,e,e)|~l1(c,b)|~q1(e,e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_143)).
% 0.42/1.61 cnf(rule_078, axiom, (p1(d,d,b)|~p0(d,b)|~m0(e,a,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_078)).
% 0.42/1.61 cnf(rule_031, axiom, (m1(c,a,c)|~r0(e)|~m0(a,e,c)|~r0(X1)|~k0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_031)).
% 0.42/1.61 cnf(rule_155, axiom, (p2(X1,X2,X2)|~k1(X3)|~p2(e,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_155)).
% 0.42/1.61 cnf(rule_123, axiom, (q1(X1,X1,X1)|~m0(c,X1,X1)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_123)).
% 0.42/1.61 cnf(rule_064, axiom, (p1(X1,X1,X1)|~m0(X2,X3,b)|~l0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_064)).
% 0.42/1.61 cnf(rule_083, axiom, (p1(X1,b,X2)|~m1(X1,X2,b)|~k0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_083)).
% 0.42/1.61 cnf(rule_040, axiom, (n1(X1,e,e)|~m0(X1,X2,e)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_040)).
% 0.42/1.61 cnf(rule_145, axiom, (p2(e,X1,X2)|~r0(e)|~p1(X1,X2,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_145)).
% 0.42/1.61 cnf(rule_149, axiom, (p2(X1,X1,d)|~r1(a)|~m0(X2,X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_149)).
% 0.42/1.61 cnf(rule_321, axiom, (p5(b,b,b)|~p4(X1,X1,X2)|~k5(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_321)).
% 0.42/1.61 cnf(rule_291, axiom, (p4(X1,X1,X1)|~p3(X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_291)).
% 0.42/1.61 cnf(rule_287, axiom, (p4(X1,X2,X1)|~k3(X1,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_287)).
% 0.42/1.61 cnf(rule_267, axiom, (r3(X1,X2,X1)|~p2(X1,X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_267)).
% 0.42/1.61 cnf(rule_238, axiom, (m3(X1,X1,X1)|~p2(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_238)).
% 0.42/1.61 cnf(rule_205, axiom, (k3(X1,X1,X1)|~p2(X2,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_205)).
% 0.42/1.61 cnf(rule_206, axiom, (k3(X1,X2,X1)|~p2(X2,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_206)).
% 0.42/1.61 cnf(rule_181, axiom, (q2(X1,X1,X1)|~p1(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_181)).
% 0.42/1.61 cnf(rule_154, axiom, (p2(X1,X1,X1)|~q1(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_154)).
% 0.42/1.61 cnf(rule_150, axiom, (p2(X1,X1,X1)|~m1(X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_150)).
% 0.42/1.61 cnf(rule_176, axiom, (p2(X1,X2,X1)|~m1(X2,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_176)).
% 0.42/1.61 cnf(rule_122, axiom, (q1(X1,X1,X1)|~m0(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_122)).
% 0.42/1.61 cnf(rule_121, axiom, (q1(X1,X1,X1)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_121)).
% 0.42/1.61 cnf(rule_110, axiom, (q1(X1,X1,X1)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_110)).
% 0.42/1.61 cnf(rule_006, axiom, (m1(X1,X1,X1)|~m0(X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_006)).
% 0.42/1.61 cnf(rule_025, axiom, (m1(X1,X1,X1)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_025)).
% 0.42/1.61 cnf(rule_014, axiom, (m1(X1,X1,X1)|~m0(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_014)).
% 0.42/1.61 cnf(rule_005, axiom, (m1(X1,X2,X1)|~m0(X2,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_005)).
% 0.42/1.61 cnf(rule_237, axiom, (m3(X1,c,X1)|~s2(c)|~q2(X1,c,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_237)).
% 0.42/1.61 cnf(rule_036, axiom, (n1(X1,X1,X2)|~m0(b,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_036)).
% 0.42/1.61 cnf(rule_184, axiom, (q2(X1,X1,X1)|~q1(X2,c,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_184)).
% 0.42/1.61 cnf(rule_041, axiom, (n1(e,e,X1)|~s0(b)|~m1(b,X1,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_041)).
% 0.42/1.61 cnf(rule_294, axiom, (p4(c,c,X1)|~n3(a)|~m3(X1,c,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_294)).
% 0.42/1.61 cnf(rule_234, axiom, (m3(X1,e,e)|~n2(e)|~p2(X1,e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_234)).
% 0.42/1.61 cnf(rule_141, axiom, (p2(X1,a,X1)|~q1(X1,a,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_141)).
% 0.42/1.61 cnf(rule_039, axiom, (n1(X1,c,X1)|~m0(X2,X1,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_039)).
% 0.42/1.61 cnf(rule_153, axiom, (p2(X1,X1,X1)|~n1(d,d,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_153)).
% 0.42/1.61 cnf(rule_103, axiom, (q1(X1,X1,X1)|~m0(X1,c,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_103)).
% 0.42/1.61 cnf(rule_170, axiom, (p2(X1,e,X1)|~n1(X1,e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_170)).
% 0.42/1.61 cnf(rule_087, axiom, (p1(a,b,a)|~r0(b)|~p1(a,a,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_087)).
% 0.42/1.61 cnf(rule_259, axiom, (q3(X1,X1)|~m0(X2,d,X2)|~k1(X1)|~r2(d)|~q3(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_259)).
% 0.42/1.61 cnf(rule_257, axiom, (q3(X1,X2)|~n1(X3,X1,X2)|~s2(X1)|~q3(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_257)).
% 0.42/1.61 cnf(rule_133, axiom, (l2(X1,X1)|~p0(X2,X2)|~s1(X3)|~m0(X4,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_133)).
% 0.42/1.61 cnf(rule_127, axiom, (k2(X1,X2)|~m1(X3,X2,X1)|~k1(X4)|~k2(X4,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_127)).
% 0.42/1.61 cnf(rule_003, axiom, (l1(X1,X2)|~p0(X3,X1)|~r0(X4)|~m0(X2,X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_003)).
% 0.42/1.61 cnf(rule_229, axiom, (m3(b,b,b)|~q2(a,b,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_229)).
% 0.42/1.61 cnf(rule_172, axiom, (p2(a,a,a)|~p1(e,e,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_172)).
% 0.42/1.61 cnf(rule_161, axiom, (p2(d,b,b)|~p1(d,b,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_161)).
% 0.42/1.61 cnf(rule_077, axiom, (p1(c,e,b)|~m0(b,c,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_077)).
% 0.42/1.61 cnf(rule_308, axiom, (n5(X1,X1)|~m0(X2,X1,X2)|~n5(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_308)).
% 0.42/1.61 cnf(rule_281, axiom, (n4(X1,X2)|~p3(X1,X2,X2)|~n4(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_281)).
% 0.42/1.61 cnf(rule_256, axiom, (q3(X1,X1)|~p2(X2,X1,X1)|~q3(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_256)).
% 0.42/1.61 cnf(rule_255, axiom, (q3(X1,X2)|~q2(X3,X1,X2)|~n0(X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_255)).
% 0.42/1.61 cnf(rule_222, axiom, (l3(X1,X1)|~k3(X2,X1,X1)|~l2(X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_222)).
% 0.42/1.61 cnf(rule_293, axiom, (p4(X1,X1,X1)|~q3(X2,X3)|~n4(X3,X1)|~l3(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_293)).
% 0.42/1.61 cnf(rule_065, axiom, (p1(X1,X1,X1)|~l1(X2,X2)|~p0(X1,X2)|~n0(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_065)).
% 0.42/1.61 cnf(rule_010, axiom, (m1(X1,X1,c)|~n0(X2,X2)|~l1(c,c)|~p0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_010)).
% 0.42/1.61 cnf(rule_104, axiom, (q1(X1,X2,X1)|~l0(X1)|~r0(X3)|~p0(X4,X1)|~q0(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_104)).
% 0.42/1.61 cnf(rule_317, axiom, (n5(d,X1)|~k3(d,X1,a)|~n4(X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_317)).
% 0.42/1.61 cnf(rule_124, axiom, (r1(X1)|~q0(X1,X2)|~s0(d)|~q1(d,X2,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_124)).
% 0.42/1.61 cnf(rule_299, axiom, (s4(X1)|~p3(X2,X3,X4)|~l1(X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_299)).
% 0.42/1.61 cnf(rule_142, axiom, (p2(X1,X1,X1)|~k1(X2)|~k0(X2)|~l2(a,X2)|~k2(X1,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_142)).
% 0.42/1.61 cnf(rule_312, axiom, (n5(b,e)|~r3(d,b,c)|~n4(b,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_312)).
% 0.42/1.61 cnf(rule_297, axiom, (q4(b,b)|~k3(c,e,b)|~l1(b,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_297)).
% 0.42/1.61 cnf(rule_283, axiom, (n4(e,e)|~l3(b,a)|~p3(b,e,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_283)).
% 0.42/1.61 cnf(rule_303, axiom, (m5(X1,X2)|~r0(X1)|~p4(X1,X3,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_303)).
% 0.42/1.61 cnf(rule_284, axiom, (n4(X1,X1)|~k4(X2)|~m3(X1,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_284)).
% 0.42/1.61 cnf(rule_215, axiom, (l3(X1,X2)|~r0(X1)|~p2(X1,X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_215)).
% 0.42/1.61 cnf(rule_109, axiom, (q1(X1,X1,X2)|~p0(X3,X3)|~q0(X2,X1)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_109)).
% 0.42/1.61 cnf(rule_019, axiom, (m1(X1,X2,c)|~r0(c)|~s0(d)|~q0(X2,d)|~p0(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_019)).
% 0.42/1.61 cnf(rule_047, axiom, (n1(X1,d,X2)|~p0(X2,X2)|~r0(X1)|~l1(X2,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_047)).
% 0.42/1.61 cnf(rule_129, axiom, (k2(X1,X1)|~q1(X2,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_129)).
% 0.42/1.61 cnf(rule_252, axiom, (p3(X1,X1,X1)|~q0(X2,X1)|~k2(X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_252)).
% 0.42/1.61 cnf(rule_092, axiom, (q1(X1,X2,X1)|~n0(X3,X2)|~p0(X4,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_092)).
% 0.42/1.61 cnf(rule_058, axiom, (n1(X1,X1,X1)|~l1(X2,X1)|~n0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_058)).
% 0.42/1.61 cnf(rule_044, axiom, (n1(X1,X2,X1)|~p0(X1,X1)|~p0(X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_044)).
% 0.42/1.61 cnf(rule_018, axiom, (m1(X1,X1,X1)|~q0(X2,X3)|~q0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_018)).
% 0.42/1.61 cnf(rule_224, axiom, (l3(d,c)|~s2(d)|~k3(a,c,a)|~r0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_224)).
% 0.42/1.61 cnf(rule_227, axiom, (m3(X1,X1,X1)|~q0(X2,X3)|~s0(X4)|~s2(X3)|~r2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_227)).
% 0.42/1.61 cnf(rule_038, axiom, (n1(X1,X1,X1)|~n0(X1,X1)|~q0(a,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_038)).
% 0.42/1.61 cnf(rule_300, axiom, (k5(X1)|~s4(X2)|~r3(X3,X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_300)).
% 0.42/1.61 cnf(rule_278, axiom, (l4(X1)|~m0(X2,X1,X1)|~l4(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_278)).
% 0.42/1.61 cnf(rule_140, axiom, (n2(e)|~r1(b)|~r0(e)|~p1(b,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_140)).
% 0.42/1.61 cnf(rule_073, axiom, (p1(X1,X1,X1)|~n0(e,b)|~k0(b)|~k0(X1)|~k1(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_073)).
% 0.42/1.61 cnf(rule_037, axiom, (n1(X1,X2,X1)|~p0(X3,X1)|~l0(X2)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_037)).
% 0.42/1.61 cnf(rule_009, axiom, (m1(X1,X1,X1)|~s0(X2)|~r0(X2)|~q0(X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_009)).
% 0.42/1.61 cnf(rule_189, axiom, (s2(X1)|~q2(b,X1,b)|~s1(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_189)).
% 0.42/1.61 cnf(rule_277, axiom, (l4(X1)|~p3(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_277)).
% 0.42/1.61 cnf(rule_240, axiom, (n3(X1)|~p2(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_240)).
% 0.42/1.61 cnf(rule_137, axiom, (n2(X1)|~p1(X2,X3,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_137)).
% 0.42/1.61 cnf(rule_311, axiom, (n5(d,d)|~p4(c,d,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_311)).
% 0.42/1.61 cnf(rule_053, axiom, (n1(a,X1,b)|~p0(X1,d)|~p0(a,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_053)).
% 0.42/1.61 cnf(rule_034, axiom, (m1(X1,X2,X2)|~k1(a)|~k1(X2)|~q0(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_034)).
% 0.42/1.61 cnf(rule_026, axiom, (m1(X1,X1,X1)|~l0(X1)|~l0(X2)|~p0(X2,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_026)).
% 0.42/1.61 cnf(rule_183, axiom, (q2(X1,c,X2)|~k1(X2)|~l0(c)|~l2(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_183)).
% 0.42/1.61 cnf(rule_050, axiom, (n1(X1,X2,X1)|~s0(b)|~l0(X1)|~p0(b,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_050)).
% 0.42/1.61 cnf(rule_301, axiom, (k5(b)|~s4(e)|~n1(b,b,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_301)).
% 0.42/1.61 cnf(rule_027, axiom, (m1(b,b,b)|~q0(c,d)|~l1(a,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_027)).
% 0.42/1.61 cnf(rule_318, axiom, (p5(X1,X1,X2)|~s4(X2)|~l2(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_318)).
% 0.42/1.61 cnf(rule_320, axiom, (p5(X1,X2,X1)|~q4(X2,X3)|~s1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_320)).
% 0.42/1.61 cnf(rule_286, axiom, (p4(X1,X1,X1)|~q3(X2,X3)|~n3(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_286)).
% 0.42/1.61 cnf(rule_232, axiom, (m3(X1,X1,X1)|~l2(X1,X1)|~n2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_232)).
% 0.42/1.61 cnf(rule_074, axiom, (p1(X1,X1,X2)|~p0(X2,X1)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_074)).
% 0.42/1.61 cnf(rule_043, axiom, (n1(X1,X1,X1)|~k1(X1)|~p0(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_043)).
% 0.42/1.61 cnf(rule_011, axiom, (m1(X1,X1,X2)|~k0(X1)|~n0(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_011)).
% 0.42/1.61 cnf(rule_007, axiom, (m1(X1,X2,X1)|~p0(X3,X2)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_007)).
% 0.42/1.61 cnf(rule_029, axiom, (m1(X1,X2,X1)|~p0(X1,X2)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_029)).
% 0.42/1.61 cnf(rule_260, axiom, (r3(X1,X2,X2)|~s2(X2)|~l2(c,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_260)).
% 0.42/1.61 cnf(rule_231, axiom, (m3(X1,X2,X1)|~r2(X1)|~k2(c,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_231)).
% 0.42/1.61 cnf(rule_063, axiom, (p1(X1,X1,X2)|~n0(d,X1)|~k0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_063)).
% 0.42/1.61 cnf(rule_197, axiom, (k3(X1,X1,X1)|~l2(X2,b)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_197)).
% 0.42/1.61 cnf(rule_105, axiom, (q1(X1,X1,X2)|~s0(X1)|~p0(X2,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_105)).
% 0.42/1.61 cnf(rule_017, axiom, (m1(X1,X1,X1)|~s0(X1)|~q0(X2,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_017)).
% 0.42/1.61 cnf(rule_208, axiom, (k3(X1,X1,X1)|~r2(c)|~l1(b,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_208)).
% 0.42/1.61 cnf(rule_265, axiom, (r3(X1,X1,X1)|~l2(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_265)).
% 0.42/1.61 cnf(rule_246, axiom, (p3(X1,X1,X1)|~l2(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_246)).
% 0.42/1.61 cnf(rule_194, axiom, (k3(X1,X1,X2)|~k2(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_194)).
% 0.42/1.61 cnf(rule_186, axiom, (q2(X1,X1,X2)|~l1(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_186)).
% 0.42/1.61 cnf(rule_175, axiom, (p2(X1,X1,X1)|~l1(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_175)).
% 0.42/1.61 cnf(rule_100, axiom, (q1(X1,X1,X1)|~n0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_100)).
% 0.42/1.61 cnf(rule_093, axiom, (q1(X1,X1,X1)|~q0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_093)).
% 0.42/1.61 cnf(rule_095, axiom, (q1(X1,X2,X2)|~p0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_095)).
% 0.42/1.61 cnf(rule_085, axiom, (p1(X1,X1,X1)|~p0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_085)).
% 0.42/1.61 cnf(rule_066, axiom, (p1(X1,X1,X1)|~n0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_066)).
% 0.42/1.61 cnf(rule_067, axiom, (p1(X1,X1,X1)|~q0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_067)).
% 0.42/1.61 cnf(rule_069, axiom, (p1(X1,X1,X2)|~p0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_069)).
% 0.42/1.61 cnf(rule_013, axiom, (m1(X1,X1,X1)|~q0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_013)).
% 0.42/1.61 cnf(rule_157, axiom, (p2(X1,X1,X1)|~l1(X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_157)).
% 0.42/1.61 cnf(rule_195, axiom, (k3(c,c,c)|~s2(e)|~k2(c,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_195)).
% 0.42/1.61 cnf(rule_147, axiom, (p2(e,c,c)|~r1(d)|~l1(e,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_147)).
% 0.42/1.61 cnf(rule_211, axiom, (k3(X1,X1,X1)|~l0(X1)|~r2(e)|~r0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_211)).
% 0.42/1.61 cnf(rule_079, axiom, (p1(X1,X1,X1)|~k0(e)|~k1(X1)|~l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_079)).
% 0.42/1.61 cnf(rule_249, axiom, (p3(X1,X1,X1)|~k1(X1)|~n2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_249)).
% 0.42/1.61 cnf(rule_233, axiom, (m3(X1,X1,X1)|~n2(X1)|~m2(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_233)).
% 0.42/1.61 cnf(rule_167, axiom, (p2(X1,X1,X1)|~s1(X1)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_167)).
% 0.42/1.61 cnf(rule_173, axiom, (p2(X1,X1,X1)|~r1(X2)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_173)).
% 0.42/1.61 cnf(rule_102, axiom, (q1(X1,X1,X1)|~k0(X1)|~l0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_102)).
% 0.42/1.61 cnf(rule_072, axiom, (p1(X1,X1,X1)|~s0(X2)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_072)).
% 0.42/1.61 cnf(rule_061, axiom, (n1(X1,X1,X1)|~k0(X1)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_061)).
% 0.42/1.61 cnf(rule_021, axiom, (m1(X1,X2,X1)|~l0(X1)|~k0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_021)).
% 0.42/1.61 cnf(rule_035, axiom, (m1(X1,X2,X1)|~r0(X1)|~l0(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_035)).
% 0.42/1.61 cnf(rule_253, axiom, (p3(b,c,b)|~k2(c,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_253)).
% 0.42/1.61 cnf(rule_239, axiom, (m3(b,b,b)|~l2(a,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_239)).
% 0.42/1.61 cnf(rule_070, axiom, (p1(c,c,c)|~p0(a,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_070)).
% 0.42/1.61 cnf(rule_075, axiom, (p1(a,a,a)|~p0(b,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_075)).
% 0.42/1.61 cnf(rule_045, axiom, (n1(d,d,d)|~q0(d,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_045)).
% 0.42/1.61 cnf(rule_219, axiom, (l3(X1,X1)|~n2(X2)|~l1(X3,X1)|~l3(X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_219)).
% 0.42/1.61 cnf(rule_174, axiom, (p2(X1,X1,X1)|~n2(X1)|~k1(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_174)).
% 0.42/1.61 cnf(rule_112, axiom, (q1(X1,X1,X1)|~k1(X1)|~s0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_112)).
% 0.42/1.61 cnf(rule_310, axiom, (n5(X1,X1)|~p0(X1,X2)|~m4(X3,X3)|~k5(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_310)).
% 0.42/1.61 cnf(rule_131, axiom, (l2(X1,X2)|~s1(X1)|~n0(e,X2)|~l2(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_131)).
% 0.42/1.61 cnf(rule_094, axiom, (q1(b,e,e)|~s0(e)|~k0(b)|~l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_094)).
% 0.42/1.61 cnf(rule_119, axiom, (q1(X1,b,b)|~s0(X1)|~s0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_119)).
% 0.42/1.61 cnf(rule_264, axiom, (r3(X1,X1,X1)|~s2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_264)).
% 0.42/1.61 cnf(rule_266, axiom, (r3(X1,X1,X1)|~r2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_266)).
% 0.42/1.61 cnf(rule_244, axiom, (p3(X1,X1,X1)|~n2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_244)).
% 0.42/1.61 cnf(rule_236, axiom, (m3(X1,X1,X1)|~n2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_236)).
% 0.42/1.61 cnf(rule_210, axiom, (k3(X1,X1,X1)|~n2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_210)).
% 0.42/1.61 cnf(rule_212, axiom, (k3(X1,X1,X1)|~m2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_212)).
% 0.42/1.61 cnf(rule_159, axiom, (p2(X1,X1,X1)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_159)).
% 0.42/1.61 cnf(rule_116, axiom, (q1(X1,X1,X1)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_116)).
% 0.42/1.61 cnf(rule_106, axiom, (q1(X1,X1,X1)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_106)).
% 0.42/1.61 cnf(rule_097, axiom, (q1(X1,X1,X1)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_097)).
% 0.42/1.61 cnf(rule_068, axiom, (p1(X1,X1,X1)|~k0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_068)).
% 0.42/1.61 cnf(rule_057, axiom, (n1(X1,X1,X1)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_057)).
% 0.42/1.61 cnf(rule_032, axiom, (m1(X1,X1,X1)|~s0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_032)).
% 0.42/1.61 cnf(rule_198, axiom, (k3(c,c,c)|~k0(a)|~r2(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_198)).
% 0.42/1.61 cnf(rule_151, axiom, (p2(d,d,d)|~k1(d)|~s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_151)).
% 0.42/1.61 cnf(rule_117, axiom, (q1(d,d,d)|~k0(e)|~s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_117)).
% 0.42/1.61 cnf(rule_090, axiom, (p1(e,e,e)|~r0(e)|~k0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_090)).
% 0.42/1.61 cnf(rule_056, axiom, (n1(a,a,a)|~l0(a)|~r0(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_056)).
% 0.42/1.61 cnf(rule_023, axiom, (m1(a,a,a)|~l0(a)|~s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_023)).
% 0.42/1.61 cnf(rule_279, axiom, (m4(X1,X2)|~l2(X3,X2)|~s3(a,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_279)).
% 0.42/1.61 cnf(rule_298, axiom, (r4(X1)|~n3(X1)|~q3(X2,X3)|~p0(X4,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_298)).
% 0.42/1.61 cnf(rule_214, axiom, (k3(c,c,c)|~r2(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_214)).
% 0.42/1.61 cnf(rule_204, axiom, (k3(a,a,a)|~r2(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_204)).
% 0.42/1.61 cnf(rule_115, axiom, (q1(b,b,b)|~l0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_115)).
% 0.42/1.61 cnf(rule_120, axiom, (q1(b,b,b)|~r0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_120)).
% 0.42/1.61 cnf(rule_088, axiom, (p1(a,a,a)|~l0(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_088)).
% 0.42/1.61 cnf(rule_049, axiom, (n1(c,c,c)|~l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_049)).
% 0.42/1.61 cnf(rule_020, axiom, (m1(c,c,c)|~l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_020)).
% 0.42/1.61 cnf(rule_008, axiom, (m1(b,b,b)|~l0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_008)).
% 0.42/1.61 cnf(rule_030, axiom, (m1(e,e,e)|~r0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_030)).
% 0.42/1.61 cnf(rule_012, axiom, (m1(e,e,e)|~r0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_012)).
% 0.42/1.61 cnf(rule_022, axiom, (m1(e,e,e)|~s0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_022)).
% 0.42/1.61 cnf(axiom_19, axiom, (m0(X1,d,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_19)).
% 0.42/1.61 cnf(axiom_12, axiom, (m0(a,X1,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_12)).
% 0.42/1.61 cnf(rule_296, axiom, (q4(X1,X1)|~r1(X1)|~l4(X2)|~q4(X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_296)).
% 0.42/1.61 cnf(rule_258, axiom, (q3(X1,X1)|~r2(X1)|~s1(X2)|~l2(X3,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_258)).
% 0.42/1.61 cnf(rule_004, axiom, (l1(X1,X1)|~k1(X1)|~l0(X2)|~l1(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_004)).
% 0.42/1.61 cnf(axiom_16, axiom, (m0(c,b,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_16)).
% 0.42/1.61 cnf(axiom_31, axiom, (m0(b,b,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_31)).
% 0.42/1.61 cnf(axiom_38, axiom, (m0(b,a,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_38)).
% 0.42/1.61 cnf(axiom_23, axiom, (m0(a,e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_23)).
% 0.42/1.61 cnf(axiom_27, axiom, (m0(e,b,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_27)).
% 0.42/1.61 cnf(axiom_4, axiom, (m0(e,d,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_4)).
% 0.42/1.61 cnf(axiom_8, axiom, (m0(e,d,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_8)).
% 0.42/1.61 cnf(axiom_35, axiom, (m0(d,e,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_35)).
% 0.42/1.61 cnf(rule_330, axiom, (s5(X1)|~k4(X1)|~s3(X1,X2)|~l5(X3)|~s5(X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_330)).
% 0.42/1.61 cnf(rule_220, axiom, (l3(X1,X1)|~s2(X2)|~l1(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_220)).
% 0.42/1.61 cnf(rule_274, axiom, (k4(c)|~n0(c,d)|~q3(e,b)|~n3(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_274)).
% 0.42/1.61 cnf(rule_305, axiom, (m5(X1,X1)|~s4(X1)|~m4(e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_305)).
% 0.42/1.61 cnf(rule_325, axiom, (q5(X1,X1)|~q4(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_325)).
% 0.42/1.61 cnf(rule_326, axiom, (q5(X1,X1)|~m4(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_326)).
% 0.42/1.61 cnf(rule_313, axiom, (n5(X1,X1)|~q4(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_313)).
% 0.42/1.61 cnf(rule_309, axiom, (n5(X1,X1)|~n4(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_309)).
% 0.42/1.61 cnf(rule_002, axiom, (l1(X1,X1)|~n0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_002)).
% 0.42/1.61 cnf(rule_302, axiom, (l5(X1)|~q4(X2,X2)|~k1(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_302)).
% 0.42/1.61 cnf(rule_135, axiom, (m2(X1)|~s0(X1)|~l1(X2,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_135)).
% 0.42/1.61 cnf(rule_126, axiom, (s1(X1)|~q0(X1,X2)|~s1(X3)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_126)).
% 0.42/1.61 cnf(rule_327, axiom, (r5(X1,X2)|~s4(X1)|~k0(b)|~n3(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_327)).
% 0.42/1.61 cnf(rule_223, axiom, (l3(c,c)|~k2(b,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_223)).
% 0.42/1.61 cnf(rule_221, axiom, (l3(d,d)|~k2(a,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_221)).
% 0.42/1.61 cnf(rule_130, axiom, (k2(e,e)|~l1(e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_130)).
% 0.42/1.61 cnf(rule_322, axiom, (q5(X1,X2)|~s4(X1)|~m2(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_322)).
% 0.42/1.61 cnf(rule_315, axiom, (n5(X1,X1)|~s1(X1)|~k4(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_315)).
% 0.42/1.61 cnf(rule_306, axiom, (m5(X1,X1)|~s4(X2)|~r0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_306)).
% 0.42/1.61 cnf(rule_125, axiom, (s1(X1)|~p0(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_125)).
% 0.42/1.61 cnf(rule_001, axiom, (k1(X1)|~n0(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_001)).
% 0.42/1.61 cnf(rule_217, axiom, (l3(X1,X1)|~n2(X1)|~m2(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_217)).
% 0.42/1.61 cnf(rule_139, axiom, (n2(c)|~l1(e,c)|~k0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_139)).
% 0.42/1.61 cnf(rule_328, axiom, (r5(X1,X1)|~k4(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_328)).
% 0.42/1.61 cnf(rule_324, axiom, (q5(X1,X1)|~l4(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_324)).
% 0.42/1.61 cnf(rule_314, axiom, (n5(X1,X1)|~r4(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_314)).
% 0.42/1.61 cnf(rule_304, axiom, (m5(X1,X1)|~k4(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_304)).
% 0.42/1.61 cnf(rule_218, axiom, (l3(X1,X1)|~r2(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_218)).
% 0.42/1.61 cnf(prove_this, negated_conjecture, (~l3(d,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_this)).
% 0.42/1.61 cnf(rule_329, axiom, (s5(X1)|~l4(X1)|~r4(X2)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_329)).
% 0.42/1.61 cnf(rule_188, axiom, (r2(X1)|~r1(X1)|~l0(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_188)).
% 0.42/1.61 cnf(rule_323, axiom, (q5(a,a)|~r4(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_323)).
% 0.42/1.61 cnf(axiom_14, axiom, (p0(b,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_14)).
% 0.42/1.61 cnf(axiom_17, axiom, (q0(X1,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_17)).
% 0.42/1.61 cnf(rule_191, axiom, (s2(d)|~r1(d)|~s1(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_191)).
% 0.42/1.61 cnf(rule_190, axiom, (s2(d)|~s1(a)|~s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_190)).
% 0.42/1.61 cnf(axiom_18, axiom, (p0(c,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_18)).
% 0.42/1.61 cnf(axiom_22, axiom, (p0(b,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_22)).
% 0.42/1.61 cnf(axiom_10, axiom, (p0(b,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_10)).
% 0.42/1.61 cnf(axiom_34, axiom, (n0(c,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_34)).
% 0.42/1.61 cnf(axiom_37, axiom, (n0(b,a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_37)).
% 0.42/1.61 cnf(axiom_15, axiom, (n0(a,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_15)).
% 0.42/1.61 cnf(axiom_11, axiom, (n0(e,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_11)).
% 0.42/1.61 cnf(axiom_30, axiom, (n0(e,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_30)).
% 0.42/1.61 cnf(axiom_26, axiom, (n0(d,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_26)).
% 0.42/1.61 cnf(axiom_7, axiom, (n0(d,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_7)).
% 0.42/1.61 cnf(axiom_3, axiom, (n0(d,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_3)).
% 0.42/1.61 cnf(axiom_6, axiom, (q0(b,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_6)).
% 0.42/1.61 cnf(axiom_21, axiom, (q0(b,e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_21)).
% 0.42/1.61 cnf(axiom_36, axiom, (q0(a,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_36)).
% 0.42/1.61 cnf(axiom_2, axiom, (q0(e,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_2)).
% 0.42/1.61 cnf(axiom_33, axiom, (q0(d,c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_33)).
% 0.42/1.61 cnf(axiom_29, axiom, (q0(d,b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_29)).
% 0.42/1.61 cnf(axiom_25, axiom, (q0(d,d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_25)).
% 0.42/1.61 cnf(rule_136, axiom, (m2(b)|~k1(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', rule_136)).
% 0.42/1.61 cnf(axiom_32, axiom, (k0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_32)).
% 0.42/1.61 cnf(axiom_28, axiom, (k0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_28)).
% 0.42/1.61 cnf(axiom_24, axiom, (l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_24)).
% 0.42/1.61 cnf(axiom_20, axiom, (l0(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_20)).
% 0.42/1.61 cnf(axiom_9, axiom, (r0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_9)).
% 0.42/1.61 cnf(axiom_13, axiom, (r0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_13)).
% 0.42/1.61 cnf(axiom_5, axiom, (s0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_5)).
% 0.42/1.61 cnf(axiom_1, axiom, (s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax', axiom_1)).
% 0.42/1.61 cnf(i_0_362, axiom, (q1(X1,X1,X1)|~n1(X2,X3,X3)|~p0(X2,X4)|~m1(X1,X3,X2)|~q1(X4,X2,X3)), rule_096, ['final']).
% 0.42/1.61 cnf(i_0_363, axiom, (q2(X1,X2,X1)|~p1(X1,X1,X3)|~n1(X2,X1,X3)|~q2(X2,X3,X1)), rule_182, ['final']).
% 0.42/1.61 cnf(i_0_364, axiom, (n1(X1,X1,X1)|~m1(c,X1,X2)|~m0(b,X2,c)|~n1(X2,X1,X2)), rule_051, ['final']).
% 0.42/1.61 cnf(i_0_365, axiom, (p2(b,c,c)|~p1(X1,b,b)|~n1(e,e,X1)|~q1(e,c,X1)), rule_162, ['final']).
% 0.42/1.61 cnf(i_0_366, axiom, (q4(X1,X2)|~k3(X3,X3,X1)|~q2(X4,X2,X1)|~m3(X4,X5,X4)), rule_295, ['final']).
% 0.42/1.61 cnf(i_0_367, axiom, (k2(X1,X1)|~n1(e,d,X1)|~m1(X1,e,X1)|~q1(X1,X1,d)), rule_128, ['final']).
% 0.42/1.61 cnf(i_0_368, axiom, (m3(X1,X2,X1)|~m0(X3,X3,X2)|~l2(X4,X1)|~m0(X1,X4,X4)|~s2(X3)), rule_225, ['final']).
% 0.42/1.61 cnf(i_0_369, axiom, (p4(X1,X1,X1)|~k3(X2,X3,X3)|~n4(X1,X3)|~p1(X3,X2,X1)), rule_292, ['final']).
% 0.42/1.61 cnf(i_0_370, axiom, (r3(X1,X1,X1)|~p1(X2,X3,X1)|~l2(X3,X2)|~r3(X1,X2,X1)), rule_262, ['final']).
% 0.42/1.61 cnf(i_0_371, axiom, (p2(X1,X2,X2)|~p1(X1,X3,X4)|~l1(X3,X4)|~p2(X1,X2,X1)), rule_146, ['final']).
% 0.42/1.61 cnf(i_0_372, axiom, (p2(X1,X2,X2)|~n1(X3,X2,X3)|~p0(X1,X2)|~p2(X1,X2,X1)), rule_152, ['final']).
% 0.42/1.61 cnf(i_0_373, axiom, (n2(a)|~m1(b,a,e)|~k1(c)|~n1(e,a,e)|~q1(c,a,d)), rule_138, ['final']).
% 0.42/1.61 cnf(i_0_374, axiom, (q2(X1,X2,X1)|~r1(X2)|~m0(X3,X4,X1)|~k0(X2)|~q2(X2,X2,X2)), rule_187, ['final']).
% 0.42/1.61 cnf(i_0_375, axiom, (m1(X1,a,X2)|~m0(a,X3,a)|~q0(X1,X2)|~m1(X2,c,X2)), rule_024, ['final']).
% 0.42/1.61 cnf(i_0_376, axiom, (r3(a,a,e)|~k2(a,a)|~q2(X1,e,X1)|~m2(b)|~m3(a,X1,X1)), rule_269, ['final']).
% 0.42/1.61 cnf(i_0_377, axiom, (p3(X1,d,e)|~l3(b,e)|~p2(d,b,c)|~n3(X1)|~q2(X1,d,X1)), rule_243, ['final']).
% 0.42/1.61 cnf(i_0_378, axiom, (p2(X1,X1,X2)|~q1(c,X1,X3)|~s1(c)|~s0(e)|~p2(X1,X3,X1)), rule_158, ['final']).
% 0.42/1.61 cnf(i_0_379, axiom, (r3(X1,X1,X2)|~m2(X2)|~m3(X3,b,X1)|~r3(X2,X4,X4)), rule_268, ['final']).
% 0.42/1.61 cnf(i_0_380, axiom, (q2(X1,X1,X1)|~n1(X2,d,X3)|~k1(X1)|~q2(X3,X3,X2)), rule_185, ['final']).
% 0.42/1.61 cnf(i_0_381, axiom, (k3(X1,X1,X1)|~p2(X2,X3,e)|~s1(X2)|~k3(X1,X2,X2)), rule_200, ['final']).
% 0.42/1.61 cnf(i_0_382, axiom, (p4(X1,X1,X1)|~m3(X2,X3,X1)|~p4(X1,X3,X1)), rule_290, ['final']).
% 0.42/1.61 cnf(i_0_383, axiom, (p4(X1,X2,X2)|~r3(X2,X2,X1)|~p4(X3,X3,X4)), rule_288, ['final']).
% 0.42/1.61 cnf(i_0_384, axiom, (r3(X1,X1,X1)|~p3(X2,X1,X3)|~r3(X2,X2,X2)), rule_271, ['final']).
% 0.42/1.61 cnf(i_0_385, axiom, (p3(X1,X2,X2)|~m3(X2,X3,X4)|~p2(X1,X2,X4)), rule_251, ['final']).
% 0.42/1.61 cnf(i_0_386, axiom, (k3(X1,X1,X1)|~p2(X2,X3,X2)|~m1(X1,X1,X3)), rule_196, ['final']).
% 0.42/1.61 cnf(i_0_387, axiom, (p2(X1,X1,X1)|~q1(X2,X3,X2)|~p2(X2,X2,X3)), rule_165, ['final']).
% 0.42/1.61 cnf(i_0_388, axiom, (p2(X1,X1,X1)|~q1(X2,X2,X2)|~p1(X1,X3,X1)), rule_169, ['final']).
% 0.42/1.61 cnf(i_0_389, axiom, (p2(X1,X1,X1)|~m1(X2,X3,X1)|~p2(X2,X1,X2)), rule_148, ['final']).
% 0.42/1.61 cnf(i_0_390, axiom, (p1(X1,X2,X3)|~m0(X3,X1,X4)|~p1(X3,X1,X4)), rule_082, ['final']).
% 0.42/1.61 cnf(i_0_391, axiom, (n1(X1,X1,X1)|~m0(X2,X2,X3)|~n1(X2,X1,X2)), rule_062, ['final']).
% 0.42/1.61 cnf(i_0_392, axiom, (n1(X1,X1,X2)|~m0(X3,X4,X4)|~m0(X2,X3,X1)), rule_059, ['final']).
% 0.42/1.61 cnf(i_0_393, axiom, (m1(X1,X2,X2)|~m1(X3,X2,X1)|~m1(X3,X4,X2)), rule_016, ['final']).
% 0.42/1.61 cnf(i_0_394, axiom, (r3(X1,X1,X1)|~m0(d,X2,X1)|~r3(X1,X1,X2)), rule_263, ['final']).
% 0.42/1.61 cnf(i_0_395, axiom, (p2(X1,X1,X1)|~m1(a,a,X2)|~p2(a,X3,X1)), rule_160, ['final']).
% 0.42/1.61 cnf(i_0_396, axiom, (q1(e,X1,X1)|~m0(X1,d,X1)|~m0(e,d,X1)), rule_107, ['final']).
% 0.42/1.61 cnf(i_0_397, axiom, (p2(X1,e,X2)|~n1(e,X1,a)|~q1(a,X2,X1)), rule_156, ['final']).
% 0.42/1.61 cnf(i_0_398, axiom, (p3(e,b,e)|~m3(e,X1,e)|~q2(X1,X1,b)), rule_254, ['final']).
% 0.42/1.61 cnf(i_0_399, axiom, (l2(X1,X1)|~m0(X2,X1,X3)|~m1(X3,X2,X2)|~p0(X2,X1)), rule_134, ['final']).
% 0.42/1.61 cnf(i_0_400, axiom, (q1(d,d,c)|~m0(c,b,a)|~m1(c,d,a)), rule_111, ['final']).
% 0.42/1.61 cnf(i_0_401, axiom, (m3(X1,X1,X1)|~k2(X2,X3)|~m3(X1,X3,X1)|~n0(X3,a)|~l2(a,a)), rule_226, ['final']).
% 0.42/1.61 cnf(i_0_402, axiom, (s3(X1,X2)|~q2(X3,X1,X3)|~s2(X1)|~m0(X3,X4,X2)), rule_273, ['final']).
% 0.42/1.61 cnf(i_0_403, axiom, (k4(e)|~q3(X1,X1)|~q1(a,a,X2)|~r3(X1,e,X2)), rule_276, ['final']).
% 0.42/1.61 cnf(i_0_404, axiom, (n5(X1,X1)|~p4(X2,X1,X1)|~s1(X1)|~p4(b,b,X3)), rule_316, ['final']).
% 0.42/1.61 cnf(i_0_405, axiom, (l3(X1,X1)|~p1(X1,X1,X2)|~p2(X2,X3,X1)), rule_216, ['final']).
% 0.42/1.61 cnf(i_0_406, axiom, (p5(X1,X2,X2)|~l2(X1,X3)|~p5(X1,X3,X1)|~m4(X3,X2)), rule_319, ['final']).
% 0.42/1.61 cnf(i_0_407, axiom, (p3(X1,X1,X1)|~l1(X2,X2)|~l3(X2,X1)|~p3(X3,X3,X2)), rule_245, ['final']).
% 0.42/1.61 cnf(i_0_408, axiom, (k3(X1,X1,X2)|~q0(X3,X2)|~k2(X1,X4)|~k3(X2,X5,X4)), rule_202, ['final']).
% 0.42/1.61 cnf(i_0_409, axiom, (k3(X1,X1,X1)|~m2(X2)|~l1(X3,X4)|~s2(X1)|~k3(X3,X4,X3)), rule_209, ['final']).
% 0.42/1.61 cnf(i_0_410, axiom, (n1(X1,X1,X1)|~m0(X2,X2,X2)|~k1(X1)|~s0(X1)|~p0(X3,X2)), rule_052, ['final']).
% 0.42/1.61 cnf(i_0_411, axiom, (p2(b,c,a)|~r0(e)|~n1(c,X1,X1)|~p0(b,X1)|~k2(c,a)), rule_144, ['final']).
% 0.42/1.61 cnf(i_0_412, axiom, (q1(X1,X1,X1)|~p0(X2,X3)|~p1(X1,b,b)|~q0(b,b)), rule_108, ['final']).
% 0.42/1.61 cnf(i_0_413, axiom, (p4(X1,X1,X1)|~l4(X1)|~n0(X1,X2)|~p4(X3,X4,X3)), rule_289, ['final']).
% 0.42/1.61 cnf(i_0_414, axiom, (r3(X1,X1,X1)|~l1(X2,X3)|~n1(X3,X3,X3)|~r2(X1)), rule_261, ['final']).
% 0.42/1.61 cnf(i_0_415, axiom, (r3(X1,X2,X3)|~k2(X2,X3)|~r2(X3)|~r3(X3,X1,X1)), rule_272, ['final']).
% 0.42/1.61 cnf(i_0_416, axiom, (k3(X1,X2,X1)|~s1(X2)|~p2(X3,X2,X4)|~n0(X1,X4)), rule_192, ['final']).
% 0.42/1.61 cnf(i_0_417, axiom, (p2(X1,X1,X1)|~p0(X1,X1)|~r1(X2)|~p2(X3,X2,X1)), rule_164, ['final']).
% 0.42/1.61 cnf(i_0_418, axiom, (p1(X1,X1,X1)|~q0(X2,X3)|~k1(X4)|~n1(X2,X1,X5)), rule_091, ['final']).
% 0.42/1.61 cnf(i_0_419, axiom, (p1(X1,X1,X1)|~n0(X2,X2)|~l0(X3)|~n1(X2,X4,X1)), rule_080, ['final']).
% 0.42/1.61 cnf(i_0_420, axiom, (p1(X1,X1,X1)|~m1(X2,X3,X1)|~q0(X3,X4)|~l0(X5)), rule_081, ['final']).
% 0.42/1.61 cnf(i_0_421, axiom, (n1(X1,X1,X1)|~m0(X2,X3,X2)|~k0(X1)|~q0(X4,X3)), rule_042, ['final']).
% 0.42/1.61 cnf(i_0_422, axiom, (n1(X1,X2,X2)|~l0(X3)|~l1(X3,X1)|~n1(X1,X2,X1)), rule_054, ['final']).
% 0.42/1.61 cnf(i_0_423, axiom, (p2(a,c,b)|~l1(e,c)|~l2(e,b)|~r1(e)|~m1(d,a,c)), rule_168, ['final']).
% 0.42/1.61 cnf(i_0_424, axiom, (n4(d,d)|~k3(c,c,e)|~q1(d,d,d)), rule_282, ['final']).
% 0.42/1.61 cnf(i_0_425, axiom, (n5(X1,X2)|~q4(X3,X4)|~n4(X1,X4)|~p4(X5,X5,X2)|~n5(X5,X2)), rule_307, ['final']).
% 0.42/1.61 cnf(i_0_426, axiom, (p1(d,d,X1)|~s0(X1)|~n1(c,d,X1)|~r0(d)|~n0(c,X1)), rule_089, ['final']).
% 0.42/1.61 cnf(i_0_427, axiom, (r3(X1,b,X1)|~r0(X1)|~p2(b,X1,b)|~l2(X1,X1)), rule_270, ['final']).
% 0.42/1.61 cnf(i_0_428, axiom, (q1(X1,X1,X1)|~k1(X1)|~q0(X1,b)|~p1(b,b,X1)), rule_101, ['final']).
% 0.42/1.61 cnf(i_0_429, axiom, (q2(X1,X1,X1)|~q0(X2,X1)|~n1(X2,X1,X3)), rule_178, ['final']).
% 0.42/1.61 cnf(i_0_430, axiom, (p2(X1,X1,X1)|~n1(X2,X2,X2)|~p0(X1,X1)), rule_171, ['final']).
% 0.42/1.61 cnf(i_0_431, axiom, (m1(X1,X1,X1)|~q0(X2,X2)|~m1(X3,X2,X1)), rule_033, ['final']).
% 0.42/1.61 cnf(i_0_432, axiom, (q1(X1,X1,X1)|~p0(b,d)|~s0(b)|~n1(X2,d,X1)), rule_118, ['final']).
% 0.42/1.61 cnf(i_0_433, axiom, (p3(X1,X2,X3)|~q2(X4,d,X1)|~k2(X2,X3)), rule_241, ['final']).
% 0.42/1.61 cnf(i_0_434, axiom, (p2(X1,X1,X1)|~q1(X2,c,X2)|~k2(X1,c)), rule_163, ['final']).
% 0.42/1.61 cnf(i_0_435, axiom, (p1(X1,X1,X1)|~m0(b,X2,b)|~l1(X1,b)), rule_084, ['final']).
% 0.42/1.61 cnf(i_0_436, axiom, (p3(X1,X1,X1)|~n2(X1)|~q2(X2,X3,X1)|~s1(X2)), rule_247, ['final']).
% 0.42/1.61 cnf(i_0_437, axiom, (m3(X1,X2,X2)|~n2(X1)|~m2(X2)|~m3(X3,X1,X3)), rule_228, ['final']).
% 0.42/1.61 cnf(i_0_438, axiom, (k3(X1,X1,X2)|~p1(X2,X3,X1)|~m2(X4)|~m2(X3)), rule_201, ['final']).
% 0.42/1.61 cnf(i_0_439, axiom, (q1(X1,X2,X2)|~k0(X3)|~l0(X1)|~q1(X2,X2,X3)), rule_099, ['final']).
% 0.42/1.61 cnf(i_0_440, axiom, (m1(X1,X1,X1)|~l0(X1)|~k0(X1)|~m0(X1,X1,X1)), rule_028, ['final']).
% 0.42/1.61 cnf(i_0_441, axiom, (p2(a,X1,d)|~n0(X1,d)|~m1(a,X1,d)), rule_166, ['final']).
% 0.42/1.61 cnf(i_0_442, axiom, (p1(X1,X2,X1)|~l0(X3)|~p1(X2,X4,X1)|~s0(b)), rule_071, ['final']).
% 0.42/1.61 cnf(i_0_443, axiom, (m3(c,b,d)|~l1(d,b)|~m2(d)|~q2(b,c,d)), rule_230, ['final']).
% 0.42/1.61 cnf(i_0_444, axiom, (k3(d,d,d)|~p1(a,d,b)|~r2(a)|~l2(e,b)), rule_203, ['final']).
% 0.42/1.61 cnf(i_0_445, axiom, (q2(d,a,a)|~q2(d,c,a)|~s1(c)|~q0(e,c)), rule_180, ['final']).
% 0.42/1.61 cnf(i_0_446, axiom, (n1(d,e,e)|~p0(d,d)|~n1(e,e,e)|~r0(b)), rule_055, ['final']).
% 0.42/1.61 cnf(i_0_447, axiom, (n1(d,d,b)|~q0(b,e)|~m1(d,e,e)|~k0(b)), rule_060, ['final']).
% 0.42/1.61 cnf(i_0_448, axiom, (k3(X1,X1,X1)|~s1(X1)|~q2(d,X2,d)|~s2(X2)), rule_193, ['final']).
% 0.42/1.61 cnf(i_0_449, axiom, (p4(X1,X1,X2)|~r0(X1)|~r3(X2,X1,X2)), rule_285, ['final']).
% 0.42/1.61 cnf(i_0_450, axiom, (p3(X1,X1,X1)|~p2(X2,X1,X1)|~n3(X1)), rule_248, ['final']).
% 0.42/1.61 cnf(i_0_451, axiom, (p3(X1,X1,X1)|~k1(X1)|~q2(X2,X3,X1)), rule_250, ['final']).
% 0.42/1.61 cnf(i_0_452, axiom, (p3(X1,X2,X3)|~r2(X2)|~k3(X2,X3,X1)), rule_242, ['final']).
% 0.42/1.61 cnf(i_0_453, axiom, (m3(X1,X1,X2)|~r2(X2)|~k3(X1,X2,X1)), rule_235, ['final']).
% 0.42/1.61 cnf(i_0_454, axiom, (k3(X1,X1,X1)|~r1(X1)|~p2(X2,X3,X3)), rule_213, ['final']).
% 0.42/1.61 cnf(i_0_455, axiom, (q2(X1,X1,X1)|~k1(X2)|~n1(X1,X1,X2)), rule_179, ['final']).
% 0.42/1.61 cnf(i_0_456, axiom, (q2(X1,X2,X2)|~k0(X2)|~p1(X1,X1,X1)), rule_177, ['final']).
% 0.42/1.61 cnf(i_0_457, axiom, (q1(X1,X1,X1)|~m0(X1,X1,X2)|~k0(X2)), rule_114, ['final']).
% 0.42/1.61 cnf(i_0_458, axiom, (q1(X1,X1,X1)|~s0(X1)|~m0(X2,X2,X3)), rule_098, ['final']).
% 0.42/1.61 cnf(i_0_459, axiom, (q1(X1,X1,X2)|~r0(X3)|~m1(X1,X2,X2)), rule_113, ['final']).
% 0.42/1.61 cnf(i_0_460, axiom, (p1(X1,X1,X1)|~l0(X1)|~m0(X2,X3,X1)), rule_086, ['final']).
% 0.42/1.61 cnf(i_0_461, axiom, (n1(X1,X1,X1)|~m1(X2,X3,X1)|~k0(X2)), rule_046, ['final']).
% 0.42/1.61 cnf(i_0_462, axiom, (m1(X1,X2,X2)|~l0(X3)|~m0(X2,X2,X1)), rule_015, ['final']).
% 0.42/1.61 cnf(i_0_463, axiom, (p2(c,e,e)|~l1(c,b)|~q1(e,e,e)), rule_143, ['final']).
% 0.42/1.61 cnf(i_0_464, axiom, (p1(d,d,b)|~p0(d,b)|~m0(e,a,a)), rule_078, ['final']).
% 0.42/1.61 cnf(i_0_465, axiom, (m1(c,a,c)|~r0(e)|~m0(a,e,c)|~r0(X1)|~k0(e)), rule_031, ['final']).
% 0.42/1.61 cnf(i_0_466, axiom, (p2(X1,X2,X2)|~k1(X3)|~p2(e,X1,X2)), rule_155, ['final']).
% 0.42/1.61 cnf(i_0_467, axiom, (q1(X1,X1,X1)|~m0(c,X1,X1)|~r0(X1)), rule_123, ['final']).
% 0.42/1.61 cnf(i_0_468, axiom, (p1(X1,X1,X1)|~m0(X2,X3,b)|~l0(X1)), rule_064, ['final']).
% 0.42/1.61 cnf(i_0_469, axiom, (p1(X1,b,X2)|~m1(X1,X2,b)|~k0(X2)), rule_083, ['final']).
% 0.42/1.61 cnf(i_0_470, axiom, (n1(X1,e,e)|~m0(X1,X2,e)|~k1(X1)), rule_040, ['final']).
% 0.42/1.61 cnf(i_0_471, axiom, (p2(e,X1,X2)|~r0(e)|~p1(X1,X2,e)), rule_145, ['final']).
% 0.42/1.61 cnf(i_0_472, axiom, (p2(X1,X1,d)|~r1(a)|~m0(X2,X1,d)), rule_149, ['final']).
% 0.42/1.61 cnf(i_0_473, axiom, (p5(b,b,b)|~p4(X1,X1,X2)|~k5(b)), rule_321, ['final']).
% 0.42/1.61 cnf(i_0_474, axiom, (p4(X1,X1,X1)|~p3(X2,X2,X1)), rule_291, ['final']).
% 0.42/1.61 cnf(i_0_475, axiom, (p4(X1,X2,X1)|~k3(X1,X1,X2)), rule_287, ['final']).
% 0.42/1.61 cnf(i_0_476, axiom, (r3(X1,X2,X1)|~p2(X1,X3,X2)), rule_267, ['final']).
% 0.42/1.61 cnf(i_0_477, axiom, (m3(X1,X1,X1)|~p2(X1,X1,X1)), rule_238, ['final']).
% 0.42/1.61 cnf(i_0_478, axiom, (k3(X1,X1,X1)|~p2(X2,X1,X1)), rule_205, ['final']).
% 0.42/1.61 cnf(i_0_479, axiom, (k3(X1,X2,X1)|~p2(X2,X1,X1)), rule_206, ['final']).
% 0.42/1.61 cnf(i_0_480, axiom, (q2(X1,X1,X1)|~p1(X1,X1,X1)), rule_181, ['final']).
% 0.42/1.61 cnf(i_0_481, axiom, (p2(X1,X1,X1)|~q1(X1,X1,X1)), rule_154, ['final']).
% 0.42/1.61 cnf(i_0_482, axiom, (p2(X1,X1,X1)|~m1(X2,X2,X1)), rule_150, ['final']).
% 0.42/1.61 cnf(i_0_483, axiom, (p2(X1,X2,X1)|~m1(X2,X1,X2)), rule_176, ['final']).
% 0.42/1.61 cnf(i_0_484, axiom, (q1(X1,X1,X1)|~m0(X1,X2,X1)), rule_122, ['final']).
% 0.42/1.61 cnf(i_0_485, axiom, (q1(X1,X1,X1)|~m0(X2,X3,X1)), rule_121, ['final']).
% 0.42/1.61 cnf(i_0_486, axiom, (q1(X1,X1,X1)|~m0(X2,X3,X1)), rule_110, ['final']).
% 0.42/1.61 cnf(i_0_487, axiom, (m1(X1,X1,X1)|~m0(X2,X2,X1)), rule_006, ['final']).
% 0.42/1.62 cnf(i_0_488, axiom, (m1(X1,X1,X1)|~m0(X2,X3,X1)), rule_025, ['final']).
% 0.42/1.62 cnf(i_0_489, axiom, (m1(X1,X1,X1)|~m0(X2,X3,X1)), rule_014, ['final']).
% 0.42/1.62 cnf(i_0_490, axiom, (m1(X1,X2,X1)|~m0(X2,X2,X1)), rule_005, ['final']).
% 0.42/1.62 cnf(i_0_491, axiom, (m3(X1,c,X1)|~s2(c)|~q2(X1,c,c)), rule_237, ['final']).
% 0.42/1.62 cnf(i_0_492, axiom, (n1(X1,X1,X2)|~m0(b,X2,X1)), rule_036, ['final']).
% 0.42/1.62 cnf(i_0_493, axiom, (q2(X1,X1,X1)|~q1(X2,c,X1)), rule_184, ['final']).
% 0.42/1.62 cnf(i_0_494, axiom, (n1(e,e,X1)|~s0(b)|~m1(b,X1,e)), rule_041, ['final']).
% 0.42/1.62 cnf(i_0_495, axiom, (p4(c,c,X1)|~n3(a)|~m3(X1,c,a)), rule_294, ['final']).
% 0.42/1.62 cnf(i_0_496, axiom, (m3(X1,e,e)|~n2(e)|~p2(X1,e,e)), rule_234, ['final']).
% 0.42/1.62 cnf(i_0_497, axiom, (p2(X1,a,X1)|~q1(X1,a,X1)), rule_141, ['final']).
% 0.42/1.62 cnf(i_0_498, axiom, (n1(X1,c,X1)|~m0(X2,X1,c)), rule_039, ['final']).
% 0.42/1.62 cnf(i_0_499, axiom, (p2(X1,X1,X1)|~n1(d,d,X1)), rule_153, ['final']).
% 0.42/1.62 cnf(i_0_500, axiom, (q1(X1,X1,X1)|~m0(X1,c,b)), rule_103, ['final']).
% 0.42/1.62 cnf(i_0_501, axiom, (p2(X1,e,X1)|~n1(X1,e,e)), rule_170, ['final']).
% 0.42/1.62 cnf(i_0_502, axiom, (p1(a,b,a)|~r0(b)|~p1(a,a,a)), rule_087, ['final']).
% 0.42/1.62 cnf(i_0_503, axiom, (q3(X1,X1)|~m0(X2,d,X2)|~k1(X1)|~r2(d)|~q3(X2,X1)), rule_259, ['final']).
% 0.42/1.62 cnf(i_0_504, axiom, (q3(X1,X2)|~n1(X3,X1,X2)|~s2(X1)|~q3(X2,X1)), rule_257, ['final']).
% 0.42/1.62 cnf(i_0_505, axiom, (l2(X1,X1)|~p0(X2,X2)|~s1(X3)|~m0(X4,X3,X1)), rule_133, ['final']).
% 0.42/1.62 cnf(i_0_506, axiom, (k2(X1,X2)|~m1(X3,X2,X1)|~k1(X4)|~k2(X4,X2)), rule_127, ['final']).
% 0.42/1.62 cnf(i_0_507, axiom, (l1(X1,X2)|~p0(X3,X1)|~r0(X4)|~m0(X2,X1,X3)), rule_003, ['final']).
% 0.42/1.62 cnf(i_0_508, axiom, (m3(b,b,b)|~q2(a,b,a)), rule_229, ['final']).
% 0.42/1.62 cnf(i_0_509, axiom, (p2(a,a,a)|~p1(e,e,a)), rule_172, ['final']).
% 0.42/1.62 cnf(i_0_510, axiom, (p2(d,b,b)|~p1(d,b,e)), rule_161, ['final']).
% 0.42/1.62 cnf(i_0_511, axiom, (p1(c,e,b)|~m0(b,c,e)), rule_077, ['final']).
% 0.42/1.62 cnf(i_0_512, axiom, (n5(X1,X1)|~m0(X2,X1,X2)|~n5(X2,X1)), rule_308, ['final']).
% 0.42/1.62 cnf(i_0_513, axiom, (n4(X1,X2)|~p3(X1,X2,X2)|~n4(X1,X1)), rule_281, ['final']).
% 0.42/1.62 cnf(i_0_514, axiom, (q3(X1,X1)|~p2(X2,X1,X1)|~q3(X2,X1)), rule_256, ['final']).
% 0.42/1.62 cnf(i_0_515, axiom, (q3(X1,X2)|~q2(X3,X1,X2)|~n0(X3,X1)), rule_255, ['final']).
% 0.42/1.62 cnf(i_0_516, axiom, (l3(X1,X1)|~k3(X2,X1,X1)|~l2(X3,X3)), rule_222, ['final']).
% 0.42/1.62 cnf(i_0_517, axiom, (p4(X1,X1,X1)|~q3(X2,X3)|~n4(X3,X1)|~l3(X2,X2)), rule_293, ['final']).
% 0.42/1.62 cnf(i_0_518, axiom, (p1(X1,X1,X1)|~l1(X2,X2)|~p0(X1,X2)|~n0(X2,X2)), rule_065, ['final']).
% 0.42/1.62 cnf(i_0_519, axiom, (m1(X1,X1,c)|~n0(X2,X2)|~l1(c,c)|~p0(X2,X1)), rule_010, ['final']).
% 0.42/1.62 cnf(i_0_520, axiom, (q1(X1,X2,X1)|~l0(X1)|~r0(X3)|~p0(X4,X1)|~q0(X2,X2)), rule_104, ['final']).
% 0.42/1.62 cnf(i_0_521, axiom, (n5(d,X1)|~k3(d,X1,a)|~n4(X1,d)), rule_317, ['final']).
% 0.42/1.62 cnf(i_0_522, axiom, (r1(X1)|~q0(X1,X2)|~s0(d)|~q1(d,X2,d)), rule_124, ['final']).
% 0.42/1.62 cnf(i_0_523, axiom, (s4(X1)|~p3(X2,X3,X4)|~l1(X1,X3)), rule_299, ['final']).
% 0.42/1.62 cnf(i_0_524, axiom, (p2(X1,X1,X1)|~k1(X2)|~k0(X2)|~l2(a,X2)|~k2(X1,a)), rule_142, ['final']).
% 0.42/1.62 cnf(i_0_525, axiom, (n5(b,e)|~r3(d,b,c)|~n4(b,e)), rule_312, ['final']).
% 0.42/1.62 cnf(i_0_526, axiom, (q4(b,b)|~k3(c,e,b)|~l1(b,c)), rule_297, ['final']).
% 0.42/1.62 cnf(i_0_527, axiom, (n4(e,e)|~l3(b,a)|~p3(b,e,a)), rule_283, ['final']).
% 0.42/1.62 cnf(i_0_528, axiom, (m5(X1,X2)|~r0(X1)|~p4(X1,X3,X2)), rule_303, ['final']).
% 0.42/1.62 cnf(i_0_529, axiom, (n4(X1,X1)|~k4(X2)|~m3(X1,X1,X1)), rule_284, ['final']).
% 0.42/1.62 cnf(i_0_530, axiom, (l3(X1,X2)|~r0(X1)|~p2(X1,X2,X1)), rule_215, ['final']).
% 0.42/1.62 cnf(i_0_531, axiom, (q1(X1,X1,X2)|~p0(X3,X3)|~q0(X2,X1)|~k1(X1)), rule_109, ['final']).
% 0.42/1.62 cnf(i_0_532, axiom, (m1(X1,X2,c)|~r0(c)|~s0(d)|~q0(X2,d)|~p0(X1,X2)), rule_019, ['final']).
% 0.42/1.62 cnf(i_0_533, axiom, (n1(X1,d,X2)|~p0(X2,X2)|~r0(X1)|~l1(X2,d)), rule_047, ['final']).
% 0.42/1.62 cnf(i_0_534, axiom, (k2(X1,X1)|~q1(X2,X1,X1)), rule_129, ['final']).
% 0.42/1.62 cnf(i_0_535, axiom, (p3(X1,X1,X1)|~q0(X2,X1)|~k2(X3,X3)), rule_252, ['final']).
% 0.42/1.62 cnf(i_0_536, axiom, (q1(X1,X2,X1)|~n0(X3,X2)|~p0(X4,X1)), rule_092, ['final']).
% 0.42/1.62 cnf(i_0_537, axiom, (n1(X1,X1,X1)|~l1(X2,X1)|~n0(X2,X1)), rule_058, ['final']).
% 0.42/1.62 cnf(i_0_538, axiom, (n1(X1,X2,X1)|~p0(X1,X1)|~p0(X2,X3)), rule_044, ['final']).
% 0.42/1.62 cnf(i_0_539, axiom, (m1(X1,X1,X1)|~q0(X2,X3)|~q0(X2,X1)), rule_018, ['final']).
% 0.42/1.62 cnf(i_0_540, axiom, (l3(d,c)|~s2(d)|~k3(a,c,a)|~r0(b)), rule_224, ['final']).
% 0.42/1.62 cnf(i_0_541, axiom, (m3(X1,X1,X1)|~q0(X2,X3)|~s0(X4)|~s2(X3)|~r2(X1)), rule_227, ['final']).
% 0.42/1.62 cnf(i_0_542, axiom, (n1(X1,X1,X1)|~n0(X1,X1)|~q0(a,X1)), rule_038, ['final']).
% 0.42/1.62 cnf(i_0_543, axiom, (k5(X1)|~s4(X2)|~r3(X3,X1,X1)), rule_300, ['final']).
% 0.42/1.62 cnf(i_0_544, axiom, (l4(X1)|~m0(X2,X1,X1)|~l4(X2)), rule_278, ['final']).
% 0.42/1.62 cnf(i_0_545, axiom, (n2(e)|~r1(b)|~r0(e)|~p1(b,X1,X2)), rule_140, ['final']).
% 0.42/1.62 cnf(i_0_546, axiom, (p1(X1,X1,X1)|~n0(e,b)|~k0(b)|~k0(X1)|~k1(X2)), rule_073, ['final']).
% 0.42/1.62 cnf(i_0_547, axiom, (n1(X1,X2,X1)|~p0(X3,X1)|~l0(X2)|~r0(X1)), rule_037, ['final']).
% 0.42/1.62 cnf(i_0_548, axiom, (m1(X1,X1,X1)|~s0(X2)|~r0(X2)|~q0(X3,X1)), rule_009, ['final']).
% 0.42/1.62 cnf(i_0_549, axiom, (s2(X1)|~q2(b,X1,b)|~s1(b)), rule_189, ['final']).
% 0.42/1.62 cnf(i_0_550, axiom, (l4(X1)|~p3(X2,X3,X1)), rule_277, ['final']).
% 0.42/1.62 cnf(i_0_551, axiom, (n3(X1)|~p2(X2,X3,X1)), rule_240, ['final']).
% 0.42/1.62 cnf(i_0_552, axiom, (n2(X1)|~p1(X2,X3,X1)), rule_137, ['final']).
% 0.42/1.62 cnf(i_0_553, axiom, (n5(d,d)|~p4(c,d,c)), rule_311, ['final']).
% 0.42/1.62 cnf(i_0_554, axiom, (n1(a,X1,b)|~p0(X1,d)|~p0(a,b)), rule_053, ['final']).
% 0.42/1.62 cnf(i_0_555, axiom, (m1(X1,X2,X2)|~k1(a)|~k1(X2)|~q0(X1,X1)), rule_034, ['final']).
% 0.42/1.62 cnf(i_0_556, axiom, (m1(X1,X1,X1)|~l0(X1)|~l0(X2)|~p0(X2,d)), rule_026, ['final']).
% 0.42/1.62 cnf(i_0_557, axiom, (q2(X1,c,X2)|~k1(X2)|~l0(c)|~l2(X2,X1)), rule_183, ['final']).
% 0.42/1.62 cnf(i_0_558, axiom, (n1(X1,X2,X1)|~s0(b)|~l0(X1)|~p0(b,X2)), rule_050, ['final']).
% 0.42/1.62 cnf(i_0_559, axiom, (k5(b)|~s4(e)|~n1(b,b,b)), rule_301, ['final']).
% 0.42/1.62 cnf(i_0_560, axiom, (m1(b,b,b)|~q0(c,d)|~l1(a,b)), rule_027, ['final']).
% 0.42/1.62 cnf(i_0_561, axiom, (p5(X1,X1,X2)|~s4(X2)|~l2(X1,X1)), rule_318, ['final']).
% 0.42/1.62 cnf(i_0_562, axiom, (p5(X1,X2,X1)|~q4(X2,X3)|~s1(X1)), rule_320, ['final']).
% 0.42/1.62 cnf(i_0_563, axiom, (p4(X1,X1,X1)|~q3(X2,X3)|~n3(X1)), rule_286, ['final']).
% 0.42/1.62 cnf(i_0_564, axiom, (m3(X1,X1,X1)|~l2(X1,X1)|~n2(X1)), rule_232, ['final']).
% 0.42/1.62 cnf(i_0_565, axiom, (p1(X1,X1,X2)|~p0(X2,X1)|~r0(X1)), rule_074, ['final']).
% 0.42/1.62 cnf(i_0_566, axiom, (n1(X1,X1,X1)|~k1(X1)|~p0(X1,X1)), rule_043, ['final']).
% 0.42/1.62 cnf(i_0_567, axiom, (m1(X1,X1,X2)|~k0(X1)|~n0(X2,X2)), rule_011, ['final']).
% 0.42/1.62 cnf(i_0_568, axiom, (m1(X1,X2,X1)|~p0(X3,X2)|~r0(X1)), rule_007, ['final']).
% 0.42/1.62 cnf(i_0_569, axiom, (m1(X1,X2,X1)|~p0(X1,X2)|~s0(X1)), rule_029, ['final']).
% 0.42/1.62 cnf(i_0_570, axiom, (r3(X1,X2,X2)|~s2(X2)|~l2(c,X1)), rule_260, ['final']).
% 0.42/1.62 cnf(i_0_571, axiom, (m3(X1,X2,X1)|~r2(X1)|~k2(c,X2)), rule_231, ['final']).
% 0.42/1.62 cnf(i_0_572, axiom, (p1(X1,X1,X2)|~n0(d,X1)|~k0(X2)), rule_063, ['final']).
% 0.42/1.62 cnf(i_0_573, axiom, (k3(X1,X1,X1)|~l2(X2,b)|~k1(X1)), rule_197, ['final']).
% 0.42/1.62 cnf(i_0_574, axiom, (q1(X1,X1,X2)|~s0(X1)|~p0(X2,d)), rule_105, ['final']).
% 0.42/1.62 cnf(i_0_575, axiom, (m1(X1,X1,X1)|~s0(X1)|~q0(X2,d)), rule_017, ['final']).
% 0.42/1.62 cnf(i_0_576, axiom, (k3(X1,X1,X1)|~r2(c)|~l1(b,X1)), rule_208, ['final']).
% 0.42/1.62 cnf(i_0_577, axiom, (r3(X1,X1,X1)|~l2(X2,X1)), rule_265, ['final']).
% 0.42/1.62 cnf(i_0_578, axiom, (p3(X1,X1,X1)|~l2(X1,X1)), rule_246, ['final']).
% 0.42/1.62 cnf(i_0_579, axiom, (k3(X1,X1,X2)|~k2(X2,X1)), rule_194, ['final']).
% 0.42/1.62 cnf(i_0_580, axiom, (q2(X1,X1,X2)|~l1(X2,X1)), rule_186, ['final']).
% 0.42/1.62 cnf(i_0_581, axiom, (p2(X1,X1,X1)|~l1(X2,X1)), rule_175, ['final']).
% 0.42/1.62 cnf(i_0_582, axiom, (q1(X1,X1,X1)|~n0(X2,X1)), rule_100, ['final']).
% 0.42/1.62 cnf(i_0_583, axiom, (q1(X1,X1,X1)|~q0(X2,X1)), rule_093, ['final']).
% 0.42/1.62 cnf(i_0_584, axiom, (q1(X1,X2,X2)|~p0(X2,X1)), rule_095, ['final']).
% 0.42/1.62 cnf(i_0_585, axiom, (p1(X1,X1,X1)|~p0(X2,X1)), rule_085, ['final']).
% 0.42/1.62 cnf(i_0_586, axiom, (p1(X1,X1,X1)|~n0(X2,X1)), rule_066, ['final']).
% 0.42/1.62 cnf(i_0_587, axiom, (p1(X1,X1,X1)|~q0(X2,X1)), rule_067, ['final']).
% 0.42/1.62 cnf(i_0_588, axiom, (p1(X1,X1,X2)|~p0(X2,X1)), rule_069, ['final']).
% 0.42/1.62 cnf(i_0_589, axiom, (m1(X1,X1,X1)|~q0(X2,X1)), rule_013, ['final']).
% 0.42/1.62 cnf(i_0_590, axiom, (p2(X1,X1,X1)|~l1(X1,d)), rule_157, ['final']).
% 0.42/1.62 cnf(i_0_591, axiom, (k3(c,c,c)|~s2(e)|~k2(c,e)), rule_195, ['final']).
% 0.42/1.62 cnf(i_0_592, axiom, (p2(e,c,c)|~r1(d)|~l1(e,c)), rule_147, ['final']).
% 0.42/1.62 cnf(i_0_593, axiom, (k3(X1,X1,X1)|~l0(X1)|~r2(e)|~r0(e)), rule_211, ['final']).
% 0.42/1.62 cnf(i_0_594, axiom, (p1(X1,X1,X1)|~k0(e)|~k1(X1)|~l0(c)), rule_079, ['final']).
% 0.42/1.62 cnf(i_0_595, axiom, (p3(X1,X1,X1)|~k1(X1)|~n2(X1)), rule_249, ['final']).
% 0.42/1.62 cnf(i_0_596, axiom, (m3(X1,X1,X1)|~n2(X1)|~m2(X2)), rule_233, ['final']).
% 0.42/1.62 cnf(i_0_597, axiom, (p2(X1,X1,X1)|~s1(X1)|~k1(X1)), rule_167, ['final']).
% 0.42/1.62 cnf(i_0_598, axiom, (p2(X1,X1,X1)|~r1(X2)|~r0(X1)), rule_173, ['final']).
% 0.42/1.62 cnf(i_0_599, axiom, (q1(X1,X1,X1)|~k0(X1)|~l0(X2)), rule_102, ['final']).
% 0.42/1.62 cnf(i_0_600, axiom, (p1(X1,X1,X1)|~s0(X2)|~s0(X1)), rule_072, ['final']).
% 0.42/1.62 cnf(i_0_601, axiom, (n1(X1,X1,X1)|~k0(X1)|~s0(X1)), rule_061, ['final']).
% 0.42/1.62 cnf(i_0_602, axiom, (m1(X1,X2,X1)|~l0(X1)|~k0(X2)), rule_021, ['final']).
% 0.42/1.62 cnf(i_0_603, axiom, (m1(X1,X2,X1)|~r0(X1)|~l0(X2)), rule_035, ['final']).
% 0.42/1.62 cnf(i_0_604, axiom, (p3(b,c,b)|~k2(c,b)), rule_253, ['final']).
% 0.42/1.62 cnf(i_0_605, axiom, (m3(b,b,b)|~l2(a,b)), rule_239, ['final']).
% 0.42/1.62 cnf(i_0_606, axiom, (p1(c,c,c)|~p0(a,c)), rule_070, ['final']).
% 0.42/1.62 cnf(i_0_607, axiom, (p1(a,a,a)|~p0(b,a)), rule_075, ['final']).
% 0.42/1.62 cnf(i_0_608, axiom, (n1(d,d,d)|~q0(d,d)), rule_045, ['final']).
% 0.42/1.62 cnf(i_0_609, axiom, (l3(X1,X1)|~n2(X2)|~l1(X3,X1)|~l3(X3,X3)), rule_219, ['final']).
% 0.42/1.62 cnf(i_0_610, axiom, (p2(X1,X1,X1)|~n2(X1)|~k1(e)), rule_174, ['final']).
% 0.42/1.62 cnf(i_0_611, axiom, (q1(X1,X1,X1)|~k1(X1)|~s0(b)), rule_112, ['final']).
% 0.42/1.62 cnf(i_0_612, axiom, (n5(X1,X1)|~p0(X1,X2)|~m4(X3,X3)|~k5(d)), rule_310, ['final']).
% 0.42/1.62 cnf(i_0_613, axiom, (l2(X1,X2)|~s1(X1)|~n0(e,X2)|~l2(X2,X2)), rule_131, ['final']).
% 0.42/1.62 cnf(i_0_614, axiom, (q1(b,e,e)|~s0(e)|~k0(b)|~l0(c)), rule_094, ['final']).
% 0.42/1.62 cnf(i_0_615, axiom, (q1(X1,b,b)|~s0(X1)|~s0(b)), rule_119, ['final']).
% 0.42/1.62 cnf(i_0_616, axiom, (r3(X1,X1,X1)|~s2(X1)), rule_264, ['final']).
% 0.42/1.62 cnf(i_0_617, axiom, (r3(X1,X1,X1)|~r2(X1)), rule_266, ['final']).
% 0.42/1.62 cnf(i_0_618, axiom, (p3(X1,X1,X1)|~n2(X1)), rule_244, ['final']).
% 0.42/1.62 cnf(i_0_619, axiom, (m3(X1,X1,X1)|~n2(X1)), rule_236, ['final']).
% 0.42/1.62 cnf(i_0_620, axiom, (k3(X1,X1,X1)|~n2(X1)), rule_210, ['final']).
% 0.42/1.62 cnf(i_0_621, axiom, (k3(X1,X1,X1)|~m2(X1)), rule_212, ['final']).
% 0.42/1.62 cnf(i_0_622, axiom, (p2(X1,X1,X1)|~k1(X1)), rule_159, ['final']).
% 0.42/1.62 cnf(i_0_623, axiom, (q1(X1,X1,X1)|~r0(X1)), rule_116, ['final']).
% 0.42/1.62 cnf(i_0_624, axiom, (q1(X1,X1,X1)|~s0(X1)), rule_106, ['final']).
% 0.42/1.62 cnf(i_0_625, axiom, (q1(X1,X1,X1)|~s0(X1)), rule_097, ['final']).
% 0.42/1.62 cnf(i_0_626, axiom, (p1(X1,X1,X1)|~k0(X1)), rule_068, ['final']).
% 0.42/1.62 cnf(i_0_627, axiom, (n1(X1,X1,X1)|~r0(X1)), rule_057, ['final']).
% 0.42/1.62 cnf(i_0_628, axiom, (m1(X1,X1,X1)|~s0(X1)), rule_032, ['final']).
% 0.42/1.62 cnf(i_0_629, axiom, (k3(c,c,c)|~k0(a)|~r2(c)), rule_198, ['final']).
% 0.42/1.62 cnf(i_0_630, axiom, (p2(d,d,d)|~k1(d)|~s0(d)), rule_151, ['final']).
% 0.42/1.62 cnf(i_0_631, axiom, (q1(d,d,d)|~k0(e)|~s0(d)), rule_117, ['final']).
% 0.42/1.62 cnf(i_0_632, axiom, (p1(e,e,e)|~r0(e)|~k0(e)), rule_090, ['final']).
% 0.42/1.62 cnf(i_0_633, axiom, (n1(a,a,a)|~l0(a)|~r0(a)), rule_056, ['final']).
% 0.42/1.62 cnf(i_0_634, axiom, (m1(a,a,a)|~l0(a)|~s0(d)), rule_023, ['final']).
% 0.42/1.62 cnf(i_0_635, axiom, (m4(X1,X2)|~l2(X3,X2)|~s3(a,X1)), rule_279, ['final']).
% 0.42/1.62 cnf(i_0_636, axiom, (r4(X1)|~n3(X1)|~q3(X2,X3)|~p0(X4,X1)), rule_298, ['final']).
% 0.42/1.62 cnf(i_0_637, axiom, (k3(c,c,c)|~r2(c)), rule_214, ['final']).
% 0.42/1.62 cnf(i_0_638, axiom, (k3(a,a,a)|~r2(a)), rule_204, ['final']).
% 0.42/1.62 cnf(i_0_639, axiom, (q1(b,b,b)|~l0(b)), rule_115, ['final']).
% 0.42/1.62 cnf(i_0_640, axiom, (q1(b,b,b)|~r0(b)), rule_120, ['final']).
% 0.42/1.62 cnf(i_0_641, axiom, (p1(a,a,a)|~l0(a)), rule_088, ['final']).
% 0.42/1.62 cnf(i_0_642, axiom, (n1(c,c,c)|~l0(c)), rule_049, ['final']).
% 0.42/1.62 cnf(i_0_643, axiom, (m1(c,c,c)|~l0(c)), rule_020, ['final']).
% 0.42/1.62 cnf(i_0_644, axiom, (m1(b,b,b)|~l0(b)), rule_008, ['final']).
% 0.42/1.62 cnf(i_0_645, axiom, (m1(e,e,e)|~r0(e)), rule_030, ['final']).
% 0.42/1.62 cnf(i_0_646, axiom, (m1(e,e,e)|~r0(e)), rule_012, ['final']).
% 0.42/1.62 cnf(i_0_647, axiom, (m1(e,e,e)|~s0(e)), rule_022, ['final']).
% 0.42/1.62 cnf(i_0_648, axiom, (m0(X1,d,X2)), axiom_19, ['final']).
% 0.42/1.62 cnf(i_0_649, axiom, (m0(a,X1,a)), axiom_12, ['final']).
% 0.42/1.62 cnf(i_0_650, axiom, (q4(X1,X1)|~r1(X1)|~l4(X2)|~q4(X2,X3)), rule_296, ['final']).
% 0.42/1.62 cnf(i_0_651, axiom, (q3(X1,X1)|~r2(X1)|~s1(X2)|~l2(X3,X3)), rule_258, ['final']).
% 0.42/1.62 cnf(i_0_652, axiom, (l1(X1,X1)|~k1(X1)|~l0(X2)|~l1(X2,X2)), rule_004, ['final']).
% 0.42/1.62 cnf(i_0_653, axiom, (m0(c,b,a)), axiom_16, ['final']).
% 0.42/1.62 cnf(i_0_654, axiom, (m0(b,b,e)), axiom_31, ['final']).
% 0.42/1.62 cnf(i_0_655, axiom, (m0(b,a,a)), axiom_38, ['final']).
% 0.42/1.62 cnf(i_0_656, axiom, (m0(a,e,e)), axiom_23, ['final']).
% 0.42/1.62 cnf(i_0_657, axiom, (m0(e,b,c)), axiom_27, ['final']).
% 0.42/1.62 cnf(i_0_658, axiom, (m0(e,d,a)), axiom_4, ['final']).
% 0.42/1.62 cnf(i_0_659, axiom, (m0(e,d,e)), axiom_8, ['final']).
% 0.42/1.62 cnf(i_0_660, axiom, (m0(d,e,c)), axiom_35, ['final']).
% 0.42/1.62 cnf(i_0_661, axiom, (s5(X1)|~k4(X1)|~s3(X1,X2)|~l5(X3)|~s5(X3)), rule_330, ['final']).
% 0.42/1.62 cnf(i_0_662, axiom, (l3(X1,X1)|~s2(X2)|~l1(X1,X1)), rule_220, ['final']).
% 0.42/1.62 cnf(i_0_663, axiom, (k4(c)|~n0(c,d)|~q3(e,b)|~n3(e)), rule_274, ['final']).
% 0.42/1.62 cnf(i_0_664, axiom, (m5(X1,X1)|~s4(X1)|~m4(e,e)), rule_305, ['final']).
% 0.42/1.62 cnf(i_0_665, axiom, (q5(X1,X1)|~q4(X1,X1)), rule_325, ['final']).
% 0.42/1.62 cnf(i_0_666, axiom, (q5(X1,X1)|~m4(X1,X1)), rule_326, ['final']).
% 0.42/1.62 cnf(i_0_667, axiom, (n5(X1,X1)|~q4(X2,X1)), rule_313, ['final']).
% 0.42/1.62 cnf(i_0_668, axiom, (n5(X1,X1)|~n4(X2,X1)), rule_309, ['final']).
% 0.42/1.62 cnf(i_0_669, axiom, (l1(X1,X1)|~n0(X2,X1)), rule_002, ['final']).
% 0.42/1.62 cnf(i_0_670, axiom, (l5(X1)|~q4(X2,X2)|~k1(X1)), rule_302, ['final']).
% 0.42/1.62 cnf(i_0_671, axiom, (m2(X1)|~s0(X1)|~l1(X2,X3)), rule_135, ['final']).
% 0.42/1.62 cnf(i_0_672, axiom, (s1(X1)|~q0(X1,X2)|~s1(X3)), rule_126, ['final']).
% 0.42/1.62 cnf(i_0_673, axiom, (r5(X1,X2)|~s4(X1)|~k0(b)|~n3(X2)), rule_327, ['final']).
% 0.42/1.62 cnf(i_0_674, axiom, (l3(c,c)|~k2(b,c)), rule_223, ['final']).
% 0.42/1.62 cnf(i_0_675, axiom, (l3(d,d)|~k2(a,d)), rule_221, ['final']).
% 0.42/1.62 cnf(i_0_676, axiom, (k2(e,e)|~l1(e,e)), rule_130, ['final']).
% 0.42/1.62 cnf(i_0_677, axiom, (q5(X1,X2)|~s4(X1)|~m2(X2)), rule_322, ['final']).
% 0.42/1.62 cnf(i_0_678, axiom, (n5(X1,X1)|~s1(X1)|~k4(X1)), rule_315, ['final']).
% 0.42/1.62 cnf(i_0_679, axiom, (m5(X1,X1)|~s4(X2)|~r0(X1)), rule_306, ['final']).
% 0.42/1.62 cnf(i_0_680, axiom, (s1(X1)|~p0(X1,X1)), rule_125, ['final']).
% 0.42/1.62 cnf(i_0_681, axiom, (k1(X1)|~n0(X2,X1)), rule_001, ['final']).
% 0.42/1.62 cnf(i_0_682, axiom, (l3(X1,X1)|~n2(X1)|~m2(b)), rule_217, ['final']).
% 0.42/1.62 cnf(i_0_683, axiom, (n2(c)|~l1(e,c)|~k0(b)), rule_139, ['final']).
% 0.42/1.62 cnf(i_0_684, axiom, (r5(X1,X1)|~k4(X1)), rule_328, ['final']).
% 0.42/1.62 cnf(i_0_685, axiom, (q5(X1,X1)|~l4(X1)), rule_324, ['final']).
% 0.42/1.62 cnf(i_0_686, axiom, (n5(X1,X1)|~r4(X1)), rule_314, ['final']).
% 0.42/1.62 cnf(i_0_687, axiom, (m5(X1,X1)|~k4(X1)), rule_304, ['final']).
% 0.42/1.62 cnf(i_0_688, axiom, (l3(X1,X1)|~r2(X1)), rule_218, ['final']).
% 0.42/1.62 cnf(i_0_689, negated_conjecture, (~l3(d,X1)), prove_this, ['final']).
% 0.42/1.62 cnf(i_0_690, axiom, (s5(X1)|~l4(X1)|~r4(X2)), rule_329, ['final']).
% 0.42/1.62 cnf(i_0_691, axiom, (r2(X1)|~r1(X1)|~l0(X1)), rule_188, ['final']).
% 0.42/1.62 cnf(i_0_692, axiom, (q5(a,a)|~r4(a)), rule_323, ['final']).
% 0.42/1.62 cnf(i_0_693, axiom, (p0(b,X1)), axiom_14, ['final']).
% 0.42/1.62 cnf(i_0_694, axiom, (q0(X1,d)), axiom_17, ['final']).
% 0.42/1.62 cnf(i_0_695, axiom, (s2(d)|~r1(d)|~s1(d)), rule_191, ['final']).
% 0.42/1.62 cnf(i_0_696, axiom, (s2(d)|~s1(a)|~s0(d)), rule_190, ['final']).
% 0.42/1.62 cnf(i_0_697, axiom, (p0(c,b)), axiom_18, ['final']).
% 0.42/1.62 cnf(i_0_698, axiom, (p0(b,c)), axiom_22, ['final']).
% 0.42/1.62 cnf(i_0_699, axiom, (p0(b,d)), axiom_10, ['final']).
% 0.42/1.62 cnf(i_0_700, axiom, (n0(c,d)), axiom_34, ['final']).
% 0.42/1.62 cnf(i_0_701, axiom, (n0(b,a)), axiom_37, ['final']).
% 0.42/1.62 cnf(i_0_702, axiom, (n0(a,b)), axiom_15, ['final']).
% 0.42/1.62 cnf(i_0_703, axiom, (n0(e,b)), axiom_11, ['final']).
% 0.42/1.62 cnf(i_0_704, axiom, (n0(e,e)), axiom_30, ['final']).
% 0.42/1.62 cnf(i_0_705, axiom, (n0(d,c)), axiom_26, ['final']).
% 0.42/1.62 cnf(i_0_706, axiom, (n0(d,b)), axiom_7, ['final']).
% 0.42/1.62 cnf(i_0_707, axiom, (n0(d,e)), axiom_3, ['final']).
% 0.42/1.62 cnf(i_0_708, axiom, (q0(b,b)), axiom_6, ['final']).
% 0.42/1.62 cnf(i_0_709, axiom, (q0(b,e)), axiom_21, ['final']).
% 0.42/1.62 cnf(i_0_710, axiom, (q0(a,b)), axiom_36, ['final']).
% 0.42/1.62 cnf(i_0_711, axiom, (q0(e,d)), axiom_2, ['final']).
% 0.42/1.62 cnf(i_0_712, axiom, (q0(d,c)), axiom_33, ['final']).
% 0.42/1.62 cnf(i_0_713, axiom, (q0(d,b)), axiom_29, ['final']).
% 0.42/1.62 cnf(i_0_714, axiom, (q0(d,d)), axiom_25, ['final']).
% 0.42/1.62 cnf(i_0_715, axiom, (m2(b)|~k1(b)), rule_136, ['final']).
% 0.42/1.62 cnf(i_0_716, axiom, (k0(b)), axiom_32, ['final']).
% 0.42/1.62 cnf(i_0_717, axiom, (k0(e)), axiom_28, ['final']).
% 0.42/1.62 cnf(i_0_718, axiom, (l0(c)), axiom_24, ['final']).
% 0.42/1.62 cnf(i_0_719, axiom, (l0(a)), axiom_20, ['final']).
% 0.42/1.62 cnf(i_0_720, axiom, (r0(b)), axiom_9, ['final']).
% 0.42/1.62 cnf(i_0_721, axiom, (r0(e)), axiom_13, ['final']).
% 0.42/1.62 cnf(i_0_722, axiom, (s0(b)), axiom_5, ['final']).
% 0.42/1.62 cnf(i_0_723, axiom, (s0(d)), axiom_1, ['final']).
% 1.13/2.38 cnf(i_0_724, plain, (~q0(X1,X2)|~m1(X2,c,X2)|m1(X1,a,X2)), inference(scs_inference,[],[i_0_648,i_0_375])).
% 1.13/2.38 cnf(i_0_725, plain, (~n1(c,X1,X1)|~p0(b,X1)|p2(b,c,a)|~k2(c,a)), inference(scs_inference,[],[i_0_721,i_0_411])).
% 1.13/2.38 cnf(i_0_726, plain, (q1(X1,X1,X1)|~p1(X1,b,b)), inference(scs_inference,[],[i_0_693,i_0_708,i_0_412])).
% 1.13/2.38 cnf(i_0_727, plain, (p1(X1,X1,X1)|~n0(X2,X2)|~n1(X2,X3,X1)), inference(scs_inference,[],[i_0_718,i_0_419])).
% 1.13/2.38 cnf(i_0_728, plain, (p1(X1,X1,X1)|~m1(X2,X3,X1)|~q0(X3,X4)), inference(scs_inference,[],[i_0_718,i_0_420])).
% 1.13/2.38 cnf(i_0_729, plain, (q1(X1,X1,X1)|~n1(X2,d,X1)), inference(scs_inference,[],[i_0_693,i_0_722,i_0_432])).
% 1.13/2.38 cnf(i_0_730, plain, (p1(X1,X1,X1)|~l1(X1,b)), inference(scs_inference,[],[i_0_648,i_0_435])).
% 1.13/2.38 cnf(i_0_731, plain, (p1(X1,X2,X1)|~p1(X2,X3,X1)), inference(scs_inference,[],[i_0_718,i_0_722,i_0_442])).
% 1.13/2.38 cnf(i_0_732, plain, (n1(d,d,b)|~m1(d,e,e)), inference(scs_inference,[],[i_0_709,i_0_716,i_0_447])).
% 1.13/2.38 cnf(i_0_733, plain, (~m1(X1,X2,X2)|q1(X1,X1,X2)), inference(scs_inference,[],[i_0_720,i_0_459])).
% 1.13/2.38 cnf(i_0_734, plain, (~m0(X1,X1,X2)|m1(X2,X1,X1)), inference(scs_inference,[],[i_0_718,i_0_462])).
% 1.13/2.38 cnf(i_0_735, plain, (~l0(X1)|p1(X1,X1,X1)), inference(scs_inference,[],[i_0_648,i_0_468])).
% 1.13/2.38 cnf(i_0_736, plain, (~p1(X1,X2,e)|p2(e,X1,X2)), inference(scs_inference,[],[i_0_721,i_0_471])).
% 1.13/2.38 cnf(i_0_737, plain, (~m1(b,X1,e)|n1(e,e,X1)), inference(scs_inference,[],[i_0_722,i_0_494])).
% 1.13/2.38 cnf(i_0_738, plain, (p1(a,b,a)|~p1(a,a,a)), inference(scs_inference,[],[i_0_720,i_0_502])).
% 1.13/2.38 cnf(i_0_739, plain, (~m0(X1,X2,X3)|l1(X2,X1)|~p0(X3,X2)), inference(scs_inference,[],[i_0_720,i_0_507])).
% 1.13/2.38 cnf(i_0_740, plain, (~l0(X1)|~q0(X2,X2)|q1(X1,X2,X1)|~p0(X3,X1)), inference(scs_inference,[],[i_0_720,i_0_520])).
% 1.13/2.38 cnf(i_0_741, plain, (r1(X1)|~q0(X1,X2)|~q1(d,X2,d)), inference(scs_inference,[],[i_0_723,i_0_522])).
% 1.13/2.38 cnf(i_0_742, plain, (~s2(d)|~k3(a,c,a)), inference(scs_inference,[],[i_0_689,i_0_720,i_0_540])).
% 1.13/2.38 cnf(i_0_743, plain, (~s2(X1)|~r2(X2)|m3(X2,X2,X2)|~q0(X3,X1)), inference(scs_inference,[],[i_0_722,i_0_541])).
% 1.13/2.38 cnf(i_0_744, plain, (~p1(b,X1,X2)|n2(e)|~r1(b)), inference(scs_inference,[],[i_0_721,i_0_545])).
% 1.13/2.38 cnf(i_0_745, plain, (~k1(X1)|~l2(X1,X2)|q2(X2,c,X1)), inference(scs_inference,[],[i_0_718,i_0_557])).
% 1.13/2.38 cnf(i_0_746, plain, (~l0(X1)|n1(X1,X2,X1)|~p0(b,X2)), inference(scs_inference,[],[i_0_722,i_0_558])).
% 1.13/2.38 cnf(i_0_747, plain, (m1(b,b,b)|~l1(a,b)), inference(scs_inference,[],[i_0_694,i_0_560])).
% 1.13/2.38 cnf(i_0_748, plain, (~l0(X1)|k3(X1,X1,X1)|~r2(e)), inference(scs_inference,[],[i_0_721,i_0_593])).
% 1.13/2.38 cnf(i_0_749, plain, (~k1(X1)|p1(X1,X1,X1)), inference(scs_inference,[],[i_0_717,i_0_718,i_0_594])).
% 1.13/2.38 cnf(i_0_750, plain, (~k0(X1)|q1(X1,X1,X1)), inference(scs_inference,[],[i_0_718,i_0_599])).
% 1.13/2.38 cnf(i_0_751, plain, (~s0(X1)|p1(X1,X1,X1)), inference(scs_inference,[],[i_0_722,i_0_600])).
% 1.13/2.38 cnf(i_0_752, plain, (n1(d,d,d)), inference(scs_inference,[],[i_0_694,i_0_608])).
% 1.13/2.38 cnf(i_0_753, plain, (~k1(X1)|q1(X1,X1,X1)), inference(scs_inference,[],[i_0_722,i_0_611])).
% 1.13/2.38 cnf(i_0_754, plain, (~s0(X1)|q1(X1,b,b)), inference(scs_inference,[],[i_0_722,i_0_615])).
% 1.13/2.38 cnf(i_0_755, plain, (m1(a,a,a)), inference(scs_inference,[],[i_0_719,i_0_723,i_0_634])).
% 1.13/2.38 cnf(i_0_756, plain, (p1(a,a,a)), inference(scs_inference,[],[i_0_719,i_0_641])).
% 1.13/2.38 cnf(i_0_757, plain, (n1(c,c,c)), inference(scs_inference,[],[i_0_718,i_0_642])).
% 1.13/2.38 cnf(i_0_758, plain, (m1(c,c,c)), inference(scs_inference,[],[i_0_718,i_0_643])).
% 1.13/2.38 cnf(i_0_759, plain, (m1(e,e,e)), inference(scs_inference,[],[i_0_721,i_0_646])).
% 1.13/2.38 cnf(i_0_760, plain, (k4(c)|~q3(e,b)|~n3(e)), inference(scs_inference,[],[i_0_700,i_0_663])).
% 1.13/2.38 cnf(i_0_761, plain, (~k2(a,d)), inference(scs_inference,[],[i_0_689,i_0_675])).
% 1.13/2.38 cnf(i_0_762, plain, (~l1(e,c)|n2(c)), inference(scs_inference,[],[i_0_716,i_0_683])).
% 1.13/2.38 cnf(i_0_763, plain, (s2(d)|~s1(a)), inference(scs_inference,[],[i_0_723,i_0_696])).
% 1.13/2.38 cnf(i_0_764, plain, (p1(X1,X1,b)), inference(scs_inference,[],[i_0_693,i_0_588])).
% 1.13/2.38 cnf(i_0_765, plain, (~p0(X1,X2)|p1(X2,X2,X1)), inference(rename_variables,[],[i_0_588])).
% 1.13/2.38 cnf(i_0_766, plain, (p1(e,e,e)), inference(scs_inference,[],[i_0_693,i_0_717,i_0_588,i_0_626])).
% 1.13/2.38 cnf(i_0_767, plain, (~k0(X1)|p1(X1,X1,X1)), inference(rename_variables,[],[i_0_626])).
% 1.13/2.38 cnf(i_0_768, plain, (q2(b,b,b)), inference(scs_inference,[],[i_0_693,i_0_717,i_0_588,i_0_626,i_0_480])).
% 1.13/2.38 cnf(i_0_769, plain, (~p1(X1,X1,X1)|q2(X1,X1,X1)), inference(rename_variables,[],[i_0_480])).
% 1.13/2.38 cnf(i_0_770, plain, (m1(X1,d,X1)), inference(scs_inference,[],[i_0_648,i_0_693,i_0_717,i_0_588,i_0_626,i_0_480,i_0_490])).
% 1.13/2.38 cnf(i_0_771, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_772, plain, (~m0(X1,X1,X2)|m1(X2,X1,X2)), inference(rename_variables,[],[i_0_490])).
% 1.13/2.38 cnf(i_0_773, plain, (n1(X1,X1,d)), inference(scs_inference,[],[i_0_648,i_0_771,i_0_693,i_0_717,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492])).
% 1.13/2.38 cnf(i_0_774, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_775, plain, (~m0(b,X1,X2)|n1(X2,X2,X1)), inference(rename_variables,[],[i_0_492])).
% 1.13/2.38 cnf(i_0_776, plain, (q1(b,b,b)), inference(scs_inference,[],[i_0_648,i_0_771,i_0_693,i_0_717,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584])).
% 1.13/2.38 cnf(i_0_777, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_778, plain, (~p0(X1,X2)|q1(X2,X1,X1)), inference(rename_variables,[],[i_0_584])).
% 1.13/2.38 cnf(i_0_779, plain, (q1(e,e,e)), inference(scs_inference,[],[i_0_721,i_0_648,i_0_771,i_0_693,i_0_717,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623])).
% 1.13/2.38 cnf(i_0_780, plain, (~r0(X1)|q1(X1,X1,X1)), inference(rename_variables,[],[i_0_623])).
% 1.13/2.38 cnf(i_0_781, plain, (q1(d,d,d)), inference(scs_inference,[],[i_0_721,i_0_648,i_0_771,i_0_693,i_0_717,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625])).
% 1.13/2.38 cnf(i_0_782, plain, (~s0(X1)|q1(X1,X1,X1)), inference(rename_variables,[],[i_0_625])).
% 1.13/2.38 cnf(i_0_783, plain, (n1(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_693,i_0_717,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627])).
% 1.13/2.38 cnf(i_0_784, plain, (~r0(X1)|n1(X1,X1,X1)), inference(rename_variables,[],[i_0_627])).
% 1.13/2.38 cnf(i_0_785, plain, (m1(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_693,i_0_717,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628])).
% 1.13/2.38 cnf(i_0_786, plain, (~s0(X1)|m1(X1,X1,X1)), inference(rename_variables,[],[i_0_628])).
% 1.13/2.38 cnf(i_0_787, plain, (s1(b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_693,i_0_777,i_0_717,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680])).
% 1.13/2.38 cnf(i_0_788, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_789, plain, (~p0(X1,X1)|s1(X1)), inference(rename_variables,[],[i_0_680])).
% 1.13/2.38 cnf(i_0_790, plain, (p2(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_693,i_0_777,i_0_788,i_0_717,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430])).
% 1.13/2.38 cnf(i_0_791, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_792, plain, (~p0(X1,X1)|p2(X1,X1,X1)|~n1(X2,X2,X2)), inference(rename_variables,[],[i_0_430])).
% 1.13/2.38 cnf(i_0_793, plain, (p1(c,c,c)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_693,i_0_777,i_0_788,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460])).
% 1.13/2.38 cnf(i_0_794, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_795, plain, (~l0(X1)|p1(X1,X1,X1)|~m0(X2,X3,X1)), inference(rename_variables,[],[i_0_460])).
% 1.13/2.38 cnf(i_0_796, plain, (s2(b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_693,i_0_777,i_0_788,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549])).
% 1.13/2.38 cnf(i_0_797, plain, (~s1(b)|~q2(b,X1,b)|s2(X1)), inference(rename_variables,[],[i_0_549])).
% 1.13/2.38 cnf(i_0_798, plain, (n1(a,a,a)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_649,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392])).
% 1.13/2.38 cnf(i_0_799, plain, (m0(a,X1,a)), inference(rename_variables,[],[i_0_649])).
% 1.13/2.38 cnf(i_0_800, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_801, plain, (~m0(X1,X2,X3)|n1(X3,X3,X1)|~m0(X2,X4,X4)), inference(rename_variables,[],[i_0_392])).
% 1.13/2.38 cnf(i_0_802, plain, (q2(b,e,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_649,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456])).
% 1.13/2.38 cnf(i_0_803, plain, (~k0(X1)|~p1(X2,X2,X2)|q2(X2,X1,X1)), inference(rename_variables,[],[i_0_456])).
% 1.13/2.38 cnf(i_0_804, plain, (n1(e,e,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_649,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461])).
% 1.13/2.38 cnf(i_0_805, plain, (~k0(X1)|n1(X2,X2,X2)|~m1(X1,X3,X2)), inference(rename_variables,[],[i_0_461])).
% 1.13/2.38 cnf(i_0_806, plain, (m1(b,b,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_649,i_0_704,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567])).
% 1.13/2.38 cnf(i_0_807, plain, (~k0(X1)|~n0(X2,X2)|m1(X1,X1,X2)), inference(rename_variables,[],[i_0_567])).
% 1.13/2.38 cnf(i_0_808, plain, (m1(b,X1,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_649,i_0_704,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568])).
% 1.13/2.38 cnf(i_0_809, plain, (~r0(X1)|m1(X1,X2,X1)|~p0(X3,X2)), inference(rename_variables,[],[i_0_568])).
% 1.13/2.38 cnf(i_0_810, plain, (m1(c,b,c)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_649,i_0_704,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602])).
% 1.13/2.38 cnf(i_0_811, plain, (~l0(X1)|~k0(X2)|m1(X1,X2,X1)), inference(rename_variables,[],[i_0_602])).
% 1.13/2.38 cnf(i_0_812, plain, (m1(e,c,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_649,i_0_704,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603])).
% 1.13/2.38 cnf(i_0_813, plain, (~r0(X1)|~l0(X2)|m1(X1,X2,X1)), inference(rename_variables,[],[i_0_603])).
% 1.13/2.38 cnf(i_0_814, plain, (m1(b,a,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724])).
% 1.13/2.38 cnf(i_0_815, plain, (~m1(X1,c,X1)|m1(X2,a,X1)|~q0(X2,X1)), inference(rename_variables,[],[i_0_724])).
% 1.13/2.38 cnf(i_0_816, plain, (r1(X1)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741])).
% 1.13/2.38 cnf(i_0_817, plain, (~q1(d,X1,d)|r1(X2)|~q0(X2,X1)), inference(rename_variables,[],[i_0_741])).
% 1.13/2.38 cnf(i_0_818, plain, (n1(c,X1,c)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_693,i_0_777,i_0_788,i_0_791,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746])).
% 1.13/2.38 cnf(i_0_819, plain, (~p0(b,X1)|n1(X2,X1,X2)|~l0(X2)), inference(rename_variables,[],[i_0_746])).
% 1.13/2.38 cnf(i_0_820, plain, (l2(d,d)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_693,i_0_777,i_0_788,i_0_791,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399])).
% 1.13/2.38 cnf(i_0_821, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_822, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_823, plain, (~m1(X1,X2,X2)|~p0(X2,X3)|l2(X3,X3)|~m0(X2,X3,X1)), inference(rename_variables,[],[i_0_399])).
% 1.13/2.38 cnf(i_0_824, plain, (s3(b,X1)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_693,i_0_777,i_0_788,i_0_791,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402])).
% 1.13/2.38 cnf(i_0_825, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_826, plain, (~s2(X1)|s3(X1,X2)|~q2(X3,X1,X3)|~m0(X3,X4,X2)), inference(rename_variables,[],[i_0_402])).
% 1.13/2.38 cnf(i_0_827, plain, (q1(c,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_693,i_0_777,i_0_788,i_0_791,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439])).
% 1.13/2.38 cnf(i_0_828, plain, (~l0(X1)|~q1(X2,X2,X3)|q1(X1,X2,X2)|~k0(X3)), inference(rename_variables,[],[i_0_439])).
% 1.13/2.38 cnf(i_0_829, plain, (n1(b,c,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547])).
% 1.13/2.38 cnf(i_0_830, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_831, plain, (~l0(X1)|~r0(X2)|n1(X2,X1,X2)|~p0(X3,X2)), inference(rename_variables,[],[i_0_547])).
% 1.13/2.38 cnf(i_0_832, plain, (m3(d,e,d)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368])).
% 1.13/2.38 cnf(i_0_833, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_834, plain, (~m0(X1,X2,X2)|~s2(X3)|m3(X1,X4,X1)|~m0(X3,X3,X4)|~l2(X2,X1)), inference(rename_variables,[],[i_0_368])).
% 1.13/2.38 cnf(i_0_835, plain, (q2(X1,b,X1)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374])).
% 1.13/2.38 cnf(i_0_836, plain, (~r1(X1)|~k0(X1)|~q2(X1,X1,X1)|q2(X2,X1,X2)|~m0(X3,X4,X2)), inference(rename_variables,[],[i_0_374])).
% 1.13/2.38 cnf(i_0_837, plain, (k3(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479])).
% 1.13/2.38 cnf(i_0_838, plain, (~p2(X1,X2,X2)|k3(X2,X1,X2)), inference(rename_variables,[],[i_0_479])).
% 1.13/2.38 cnf(i_0_839, plain, (p2(e,e,e)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481])).
% 1.13/2.38 cnf(i_0_840, plain, (~q1(X1,X1,X1)|p2(X1,X1,X1)), inference(rename_variables,[],[i_0_481])).
% 1.13/2.38 cnf(i_0_841, plain, (p2(d,e,d)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483])).
% 1.13/2.38 cnf(i_0_842, plain, (~m1(X1,X2,X1)|p2(X2,X1,X2)), inference(rename_variables,[],[i_0_483])).
% 1.13/2.38 cnf(i_0_843, plain, (p2(d,d,d)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499])).
% 1.13/2.38 cnf(i_0_844, plain, (~n1(d,d,X1)|p2(X1,X1,X1)), inference(rename_variables,[],[i_0_499])).
% 1.13/2.38 cnf(i_0_845, plain, (p4(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475])).
% 1.13/2.38 cnf(i_0_846, plain, (~k3(X1,X1,X2)|p4(X1,X2,X1)), inference(rename_variables,[],[i_0_475])).
% 1.13/2.38 cnf(i_0_847, plain, (m3(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477])).
% 1.13/2.38 cnf(i_0_848, plain, (~p2(X1,X1,X1)|m3(X1,X1,X1)), inference(rename_variables,[],[i_0_477])).
% 1.13/2.38 cnf(i_0_849, plain, (p3(d,d,d)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578])).
% 1.13/2.38 cnf(i_0_850, plain, (~l2(X1,X1)|p3(X1,X1,X1)), inference(rename_variables,[],[i_0_578])).
% 1.13/2.38 cnf(i_0_851, plain, (q1(c,c,c)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729])).
% 1.13/2.38 cnf(i_0_852, plain, (~n1(X1,d,X2)|q1(X2,X2,X2)), inference(rename_variables,[],[i_0_729])).
% 1.13/2.38 cnf(i_0_853, plain, (r3(b,b,b)), inference(scs_inference,[],[i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616])).
% 1.13/2.38 cnf(i_0_854, plain, (~s2(X1)|r3(X1,X1,X1)), inference(rename_variables,[],[i_0_616])).
% 1.13/2.38 cnf(i_0_855, plain, (~p1(d,d,d)), inference(scs_inference,[],[i_0_689,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405])).
% 1.13/2.38 cnf(i_0_856, plain, (~l3(d,X1)), inference(rename_variables,[],[i_0_689])).
% 1.13/2.38 cnf(i_0_857, plain, (l3(X1,X1)|~p1(X1,X1,X2)|~p2(X2,X3,X1)), inference(rename_variables,[],[i_0_405])).
% 1.13/2.38 cnf(i_0_858, plain, (~k3(X1,d,d)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516])).
% 1.13/2.38 cnf(i_0_859, plain, (~l3(d,X1)), inference(rename_variables,[],[i_0_689])).
% 1.13/2.38 cnf(i_0_860, plain, (l3(X1,X1)|~k3(X2,X1,X1)|~l2(X3,X3)), inference(rename_variables,[],[i_0_516])).
% 1.13/2.38 cnf(i_0_861, plain, (l3(b,b)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530])).
% 1.13/2.38 cnf(i_0_862, plain, (~r0(X1)|~p2(X1,X2,X1)|l3(X1,X2)), inference(rename_variables,[],[i_0_530])).
% 1.13/2.38 cnf(i_0_863, plain, (r3(X1,X1,X1)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384])).
% 1.13/2.38 cnf(i_0_864, plain, (~r3(X1,X1,X1)|r3(X2,X2,X2)|~p3(X1,X2,X3)), inference(rename_variables,[],[i_0_384])).
% 1.13/2.38 cnf(i_0_865, plain, (p2(X1,X1,X1)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387])).
% 1.13/2.38 cnf(i_0_866, plain, (~p2(X1,X1,X2)|p2(X3,X3,X3)|~q1(X1,X2,X1)), inference(rename_variables,[],[i_0_387])).
% 1.13/2.38 cnf(i_0_867, plain, (~n1(e,X1,d)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727])).
% 1.13/2.38 cnf(i_0_868, plain, (p1(X1,X1,X1)|~n0(X2,X2)|~n1(X2,X3,X1)), inference(rename_variables,[],[i_0_727])).
% 1.13/2.38 cnf(i_0_869, plain, (~m1(X1,b,d)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728])).
% 1.13/2.38 cnf(i_0_870, plain, (q0(X1,d)), inference(rename_variables,[],[i_0_694])).
% 1.13/2.38 cnf(i_0_871, plain, (p1(X1,X1,X1)|~m1(X2,X3,X1)|~q0(X3,X4)), inference(rename_variables,[],[i_0_728])).
% 1.13/2.38 cnf(i_0_872, plain, (p4(X1,X1,X1)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383])).
% 1.13/2.38 cnf(i_0_873, plain, (~r3(X1,X1,X2)|p4(X2,X1,X1)|~p4(X3,X3,X4)), inference(rename_variables,[],[i_0_383])).
% 1.13/2.38 cnf(i_0_874, plain, (p3(b,b,b)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385])).
% 1.13/2.38 cnf(i_0_875, plain, (~p2(X1,X2,X3)|p3(X1,X2,X2)|~m3(X2,X4,X3)), inference(rename_variables,[],[i_0_385])).
% 1.13/2.38 cnf(i_0_876, plain, (q3(b,a)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_649,i_0_654,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515])).
% 1.13/2.38 cnf(i_0_877, plain, (~n0(X1,X2)|q3(X2,X3)|~q2(X1,X2,X3)), inference(rename_variables,[],[i_0_515])).
% 1.13/2.38 cnf(i_0_878, plain, (~p3(b,X1,X2)|~k1(X3)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_870,i_0_649,i_0_654,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418])).
% 1.13/2.38 cnf(i_0_879, plain, (q0(X1,d)), inference(rename_variables,[],[i_0_694])).
% 1.13/2.38 cnf(i_0_880, plain, (p1(X1,X1,X1)|~q0(X2,X3)|~n1(X2,X1,X4)|~k1(X5)), inference(rename_variables,[],[i_0_418])).
% 1.13/2.38 cnf(i_0_881, plain, (n5(b,b)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_694,i_0_870,i_0_649,i_0_654,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404])).
% 1.13/2.38 cnf(i_0_882, plain, (~p4(b,b,X1)|~s1(X2)|n5(X2,X2)|~p4(X3,X2,X2)), inference(rename_variables,[],[i_0_404])).
% 1.13/2.38 cnf(i_0_883, plain, (p0(b,X1)), inference(rename_variables,[],[i_0_693])).
% 1.13/2.38 cnf(i_0_884, plain, (~p1(d,X1,d)|~p3(b,X2,X3)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_830,i_0_694,i_0_870,i_0_879,i_0_649,i_0_654,i_0_700,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404,i_0_478,i_0_585,i_0_586,i_0_587,i_0_731])).
% 1.13/2.38 cnf(i_0_885, plain, (p1(X1,X2,X1)|~p1(X2,X3,X1)), inference(rename_variables,[],[i_0_731])).
% 1.13/2.38 cnf(i_0_886, plain, (~l0(d)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_830,i_0_694,i_0_870,i_0_879,i_0_649,i_0_654,i_0_700,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404,i_0_478,i_0_585,i_0_586,i_0_587,i_0_731,i_0_735])).
% 1.13/2.38 cnf(i_0_887, plain, (p1(X1,X1,X1)|~l0(X1)), inference(rename_variables,[],[i_0_735])).
% 1.13/2.38 cnf(i_0_888, plain, (q2(c,c,c)|~p3(b,X1,X2)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_830,i_0_694,i_0_870,i_0_879,i_0_649,i_0_654,i_0_700,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404,i_0_478,i_0_585,i_0_586,i_0_587,i_0_731,i_0_735,i_0_751,i_0_493])).
% 1.13/2.38 cnf(i_0_889, plain, (~q1(X1,c,X2)|q2(X2,X2,X2)), inference(rename_variables,[],[i_0_493])).
% 1.13/2.38 cnf(i_0_890, plain, (~p3(b,X1,X2)|~m1(b,d,e)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_830,i_0_694,i_0_870,i_0_879,i_0_649,i_0_654,i_0_700,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404,i_0_478,i_0_585,i_0_586,i_0_587,i_0_731,i_0_735,i_0_751,i_0_493,i_0_681,i_0_737])).
% 1.13/2.38 cnf(i_0_891, plain, (n1(e,e,X1)|~m1(b,X1,e)), inference(rename_variables,[],[i_0_737])).
% 1.13/2.38 cnf(i_0_892, plain, (~p3(b,X1,X2)|q1(e,a,a)), inference(scs_inference,[],[i_0_689,i_0_856,i_0_720,i_0_721,i_0_648,i_0_771,i_0_774,i_0_794,i_0_800,i_0_822,i_0_825,i_0_833,i_0_693,i_0_777,i_0_788,i_0_791,i_0_821,i_0_830,i_0_694,i_0_870,i_0_879,i_0_649,i_0_799,i_0_654,i_0_700,i_0_702,i_0_704,i_0_709,i_0_716,i_0_717,i_0_718,i_0_722,i_0_723,i_0_588,i_0_626,i_0_480,i_0_490,i_0_492,i_0_584,i_0_623,i_0_625,i_0_627,i_0_628,i_0_680,i_0_430,i_0_460,i_0_549,i_0_392,i_0_456,i_0_461,i_0_567,i_0_568,i_0_602,i_0_603,i_0_724,i_0_741,i_0_746,i_0_399,i_0_402,i_0_439,i_0_547,i_0_368,i_0_374,i_0_479,i_0_481,i_0_483,i_0_499,i_0_475,i_0_477,i_0_578,i_0_729,i_0_616,i_0_405,i_0_516,i_0_530,i_0_384,i_0_387,i_0_727,i_0_728,i_0_383,i_0_385,i_0_515,i_0_418,i_0_404,i_0_478,i_0_585,i_0_586,i_0_587,i_0_731,i_0_735,i_0_751,i_0_493,i_0_681,i_0_737,i_0_390,i_0_469,i_0_671,i_0_691,i_0_396])).
% 1.13/2.38 cnf(i_0_893, plain, (m0(X1,d,X2)), inference(rename_variables,[],[i_0_648])).
% 1.13/2.38 cnf(i_0_894, plain, (m0(a,X1,a)), inference(rename_variables,[],[i_0_649])).
% 1.13/2.38 cnf(i_0_895, plain, (~m0(e,d,X1)|~m0(X1,d,X1)|q1(e,X1,X1)), inference(rename_variables,[],[i_0_396])).
% 1.13/2.38 cnf(i_0_897,plain, ($false), inference(scs_inference,[],[i_0+867, i_0_773]), ['proof']).
% 1.13/2.38 % SZS output end CNFRefutation
% 1.13/2.38 % Total time : 1.273s
%------------------------------------------------------------------------------