package inference;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;

import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.InFormula;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import utils.Product;

public class ProofSystem {

	//======================Equality Axioms=============================
	
//	private static final InferenceRule reflexivity = new InferenceRule(
//			"Reflexivity",
//			List.of(),
//			new MetaEquationFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaEvaluatableTermVariable(new Variable("te"))
//			)
//	);
//	
//	private static final InferenceRule symmetry = new InferenceRule(
//			"Symmetry",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("se"))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaEvaluatableTermVariable(new Variable("se")),
//					new MetaEvaluatableTermVariable(new Variable("te"))
//			)
//	);
//	
//	private static final InferenceRule transitivity = new InferenceRule(
//			"Transitivity",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaEvaluatableTermVariable(new Variable("se")),
//					new MetaEvaluatableTermVariable(new Variable("ue"))
//			)
//	);
//	
//	private static final InferenceRule rightSubstitution = new InferenceRule(
//			"Right Substitution",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					),
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r"))
//					),
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaRDLTerm(new MetaResource(new Variable("r")))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			)
//	);
//	
//	private static final InferenceRule leftSubstitution = new InferenceRule(
//			"Left Substitution",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r"))
//					),
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("ue")),
//							new MetaRDLTerm(new MetaResource(new Variable("r")))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					),
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			)
//	);
//	
//	private static final InferenceRule identity = new InferenceRule(
//			"Identity",
//			List.of(
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaRDLTerm(new MetaResource(new Variable("r")))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaResource(new Variable("r")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("te"))
//			)
//	);
//	
//	private static final InferenceRule mapComposition = new InferenceRule(
//			"Map Composition",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r"))
//					),
//					new MetaDependencyFormula(
//							new MetaResource(new Variable("r")),
//							new MetaResource(new Variable("p"))
//					),
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaRDLTerm(new MetaResource(new Variable("p")))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaRDLTerm(
//									new MetaResource(new Variable("r")),
//									new MetaResource(new Variable("p")),
//									new MetaEvaluatableTermVariable(new Variable("te"))
//							)
//					),
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("p")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					)
//			)
//	);
//	
//	private static final InferenceRule constantness = new InferenceRule(
//			"Constantness",
//			List.of(
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("t1")), 
//							new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m")))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
//							new MetaResource(new Variable("r1"), new Variable("m")),
//							new MetaEvaluatableTermVariable(new Variable("t1"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
//	);
//	
//	private static final InferenceRule rightNormalization = new InferenceRule(
//			"Right Normalization",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("te")),
//									new MetaResource(new Variable("r"), new Variable("n"))
//							)
//					),
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("q"), new Variable("n"))
//							)
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("te")),
//									new MetaResource(new Variable("r"), new Variable("n")),
//									new MetaEvaluatableTermVariable(new Variable("se"))
//							),
//							new MetaResource(new Variable("q"), new Variable("n")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					),
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaResource(new Variable("r"), new Variable("n")),
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("q"), new Variable("n")),
//									new MetaEvaluatableTermVariable(new Variable("ue"))
//							)
//					)
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
//	);
//	
//	private static final InferenceRule pseudoConstantness = new InferenceRule(
//			"Pseudo-Constantness",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
//									new MetaResource(new Variable("r"), new Variable("n"))
//							)
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
//							new MetaResource(new Variable("r"), new Variable("n")),
//							new MetaResource(new Variable("r"), new Variable("n"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
//	);
//	
//	//======================Dependency Axioms=============================
//	
//	private static final InferenceRule identityMapping = new InferenceRule(
//			"Identity Mapping",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaResource(new Variable("r"))
//					)
//			),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaResource(new Variable("r"))
//			)
//	);
//	
//	private static final InferenceRule compositeMapping = new InferenceRule(
//			"Composite Mapping",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaResource(new Variable("r"))
//					),
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("r")),
//							new MetaResource(new Variable("q"))
//					)
//			),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaResource(new Variable("q"))
//			)
//	);
//	
//	private static final InferenceRule constantMapping = new InferenceRule(
//			"Constant Mapping",
//			List.of(),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
//					new MetaResource(new Variable("r"), new Variable("m"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
//	);
//	
//	private static final InferenceRule slicedMapping = new InferenceRule(
//			"Sliced Mapping",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("r"))
//							),
//							new MetaResource(new Variable("p"))
//					),
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaResource(new Variable("p"))
//					)
//			),
//			new MetaDependencyFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaResource(new Variable("p"))
//			)
//	);
//	
//	//======================Set-Theoretic Axioms=============================
//	
//	private static final InferenceRule memberSubstitution = new InferenceRule(
//			"Member Substitution",
//			List.of(
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					),
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					)
//			),
//			new MetaInFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaEvaluatableTermVariable(new Variable("ue"))
//			)
//	);
//	
//	private static final InferenceRule membershipChain = new InferenceRule(
//			"Membership Chain",
//			List.of(
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			),
//			new MetaInFormula(
//					new MetaEvaluatableTermVariable(new Variable("se")),
//					new MetaEvaluatableTermVariable(new Variable("ue"))
//			)
//	);
//	
//	private static final InferenceRule collectionSubstitution = new InferenceRule(
//			"Collection Substitution",
//			List.of(
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					),
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			),
//			new MetaInFormula(
//					new MetaEvaluatableTermVariable(new Variable("se")),
//					new MetaEvaluatableTermVariable(new Variable("ue"))
//			)
//	);
//	
//	private static final InferenceRule setEquivelence = new InferenceRule(
//			"Set Equivelence",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
//							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))),
//					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
//	);
//
//	private static final InferenceRule setHomomorphism = new InferenceRule(
//			"Set Homomorphism",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r"))
//					)
//			),
//			new MetaEquationFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r")),
//							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
//					),
//					new MetaRDLTerm(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("r")),
//									new MetaEvaluatableTermVariable(new Variable("te"))
//							)
//					)
//			)
//	);
//	
//	private static final InferenceRule leftProjection = new InferenceRule(
//			"Left Projection",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
//									new MetaResource(new Variable("r"), new Variable("m"))
//							),
//							new MetaResource(new Variable("q"), new Variable("l"))
//					)
//			),
//			new MetaDependencyFormula(
//					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
//					new MetaResource(new Variable("q"), new Variable("l"))
//			)
//	);
//	
//	private static final InferenceRule rightProjection = new InferenceRule(
//			"Right Projection",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
//									new MetaResource(new Variable("r"), new Variable("m"))
//							),
//							new MetaResource(new Variable("q"), new Variable("l"))
//					)
//			),
//			new MetaDependencyFormula(
//					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))),
//					new MetaResource(new Variable("q"), new Variable("l"))
//			)
//	);
//	
//	private static final InferenceRule domainMembership = new InferenceRule(
//			"Domain Membership",
//			List.of(
//					new MetaEquationFormula(
//							new MetaRDLTerm(
//								new MetaRDLTerm(
//										new MetaEvaluatableTermVariable(new Variable("se")),
//										new MetaResource(new Variable("r1")),
//										new MetaEvaluatableTermVariable(new Variable("t1"))
//								),
//								new MetaResource(new Variable("r2")),
//								new MetaEvaluatableTermVariable(new Variable("t2"))
//							),
//							new MetaResource(new Variable("c"))
//					)
//			),
//			new MetaInFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("t1")),
//							new MetaResource(new Variable("r2")),
//							new MetaEvaluatableTermVariable(new Variable("t2"))
//					),
//					new MetaRDLTerm(
//							new MetaRDLTerm(new MetaResource(new Variable("r1"))),
//							new MetaResource(new Variable("r2")),
//							new MetaEvaluatableTermVariable(new Variable("t2"))
//					)
//			)
//	);
//
//	private static final InferenceRule codomainMembership = new InferenceRule(
//			"Codomain Membership",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("r1")),
//									new MetaEvaluatableTermVariable(new Variable("t1"))
//							),
//							new MetaResource(new Variable("r2"))
//					),
//					new MetaInFormula(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("t1")),
//									new MetaResource(new Variable("r2")),
//									new MetaEvaluatableTermVariable(new Variable("t2"))
//							),
//							new MetaRDLTerm(
//									new MetaRDLTerm(
//											new MetaResource(new Variable("r1"))
//									),
//									new MetaResource(new Variable("r2")),
//									new MetaEvaluatableTermVariable(new Variable("t2"))
//							)
//					)
//			),
//			new MetaInFormula(
//					new MetaRDLTerm(
//							new MetaRDLTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaResource(new Variable("r1")),
//									new MetaEvaluatableTermVariable(new Variable("t1"))
//							),
//							new MetaResource(new Variable("r2")),
//							new MetaEvaluatableTermVariable(new Variable("t2"))
//					),
//					new MetaRDLTerm(
//							new MetaRDLTerm(
//									new MetaResource(new Variable("se"))
//							),
//							new MetaResource(new Variable("r2")),
//							new MetaEvaluatableTermVariable(new Variable("t2"))
//					)
//			)
//	);
//	
//	private static final InferenceRule codomainMembership2 = new InferenceRule(
//			"Codomain Membership2",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r1"))
//					),
//					new MetaInFormula(
//							new MetaEvaluatableTermVariable(new Variable("t1")),
//							new MetaRDLTerm(
//									new MetaResource(new Variable("r1"))
//							)
//					)
//			),
//			new MetaInFormula(
//					new MetaRDLTerm(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaResource(new Variable("r1")),
//							new MetaEvaluatableTermVariable(new Variable("t1"))
//					),
//					new MetaRDLTerm(
//							new MetaResource(new Variable("se"))
//					)
//			)
//	);

	private static final List<InferenceRule> axioms = List.of(
//			reflexivity, 
//			symmetry, 
//			transitivity,
//			rightSubstitution, 
//			leftSubstitution, 
//			identity, 
//			mapComposition, 
//			constantness,
//			rightNormalization,
//			pseudoConstantness,
//			identityMapping,
//			compositeMapping,
//			constantMapping,
//			slicedMapping,
//			memberSubstitution, 
//			membershipChain, 
//			collectionSubstitution,
//			setEquivelence,
//			setHomomorphism,
//			leftProjection,
//			rightProjection,
//			domainMembership,
//			codomainMembership,
//			codomainMembership2
	);
	
	public static void debug() {
		for (var axiom : axioms) {
			System.out.println(axiom);
			System.out.println("==================================================================================================");
		}
	}
	
	record AxiomResult(InferenceRule axiom, List<Formula> formulas) {}
	
	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
		
		Map<Formula, AxiomResult> proofGraph = new HashMap<>();
		Map<InferenceRule, Set<List<Formula>>> appliedFormulas = new HashMap<>(); 
		
		for (InferenceRule axiom : axioms) {
			appliedFormulas.put(axiom, new HashSet<>());
		}
		
		Set<Formula> appearFormulas = new HashSet<>(assumptions);
		Set<RDLTerm> existTerms = new HashSet<>();
		for (Formula assumption : assumptions) {
			addExistTerms(assumption, existTerms);
		}
		int prevAppearFormulasSize = appearFormulas.size();
		while (! appearFormulas.contains(conclusion)) {
			Set<Formula> derivedFormulas = new HashSet<>();
			for(InferenceRule axiom : axioms) {
				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), existTerms, proofGraph));
			}
			if (derivedFormulas.size() == 0) {
				return false;
			}
			appearFormulas.addAll(derivedFormulas);
			if (appearFormulas.size() == prevAppearFormulasSize) {
				return false;
			}
			prevAppearFormulasSize = appearFormulas.size();
		}
		
		Queue<Formula> formulaQueue = new ArrayDeque<>();
		Queue<Integer> depthQueue = new ArrayDeque<>();
		List<Formula> formulaResult = new ArrayList<>();
		List<Integer> depthResult = new ArrayList<>();
		Set<Formula> used = new HashSet<>();
		Map<Integer, Set<InferenceRule>> usedAxioms = new HashMap<>();
		
		formulaQueue.add(conclusion);
		depthQueue.add(0);
		
		System.out.println("proof finish");
		System.out.println();
		
		while (formulaQueue.size() != 0) {
			Formula currentFormula = formulaQueue.poll();
//			if (used.contains(currentFormula)) {
//				continue;
//			}
			used.add(currentFormula);
			int currentDepth = depthQueue.poll();
			formulaResult.add(currentFormula);
			depthResult.add(currentDepth);
			if (! proofGraph.containsKey(currentFormula)) continue;
			for (Formula nextFormula : proofGraph.get(currentFormula).formulas) {
//				if (used.contains(nextFormula)) {
//					continue;
//				}
				formulaQueue.add(nextFormula);
				depthQueue.add(currentDepth + 1);
				if (! usedAxioms.containsKey(currentDepth + 1)) {
					usedAxioms.put(currentDepth + 1, new HashSet<>());
				}
				usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom);
			}
		}
		int prevDepth = depthResult.get(depthResult.size() - 1);
		Set<Formula> sameDepthFormulas = new HashSet<>();
		for (int i = formulaResult.size() - 1; i >= 0; i--) {
			int currentDepth = depthResult.get(i);
			Formula currentFormula = formulaResult.get(i);
			if (currentDepth != prevDepth) {
				String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", "));
				String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", "));
				System.out.println(out);
				System.out.println("==============================================================(" + axioms + ")");
				sameDepthFormulas.clear();
			}
			prevDepth = currentDepth;
			sameDepthFormulas.add(currentFormula);
			
		}
		String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(","));
		System.out.println(out);
		return true;
	}
	
	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Set<RDLTerm> existTerms, Map<Formula, AxiomResult> proofGraph) {
		Set<Formula> result = new HashSet<>();
		List<List<Formula>> matchedFormulas = new ArrayList<>();
		for (int i = 0; i < axiom.getAssumptionSize(); i++) {
			matchedFormulas.add(new ArrayList<>());
			for (Formula formula : formulas) {
				if (axiom.getAssumptions().get(i).isMatchedBy(formula)) {
					matchedFormulas.get(i).add(formula);
				}
			}
		}
		for(List<Formula> applyFormulas : Product.product(matchedFormulas)) {
			if (appliedFormulas.contains(applyFormulas)) continue;
			Set<Formula> applied = axiom.apply(applyFormulas, existTerms);
			if (applied != null) {
				for (Formula formula : applied) {
					if (! formulas.contains(formula)) {
						addExistTerms(formula, existTerms);
						proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
					}
				}
				result.addAll(applied);
				appliedFormulas.add(applyFormulas);
			}
		}
		return result;
	}
	
	private static void addExistTerms(Formula formula, Set<RDLTerm> existTerms) {
		if (formula instanceof EquationFormula) {
			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof DependencyFormula) {
			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
			existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof InFormula){
			RDLTerm leftSideHand = ((InFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((InFormula) formula).getRightSideHand();
			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		}
	}
	
	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
		if (! (conclusion instanceof EquationFormula)) {
			return false;
		}
		EquationFormula equationConclusion = (EquationFormula) conclusion;
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = constructEquationGraph(assumptions);
		Deque<EvaluatableTerm> que = new ArrayDeque<>();
		Set<EvaluatableTerm> visited = new HashSet<>();
		que.add(equationConclusion.getLeftSideHand());
		while (! que.isEmpty()) {
			EvaluatableTerm curNode = que.pollFirst();
			if (curNode.equals(equationConclusion.getRightSideHand())) {
				return true;
			}
			for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) {
				if (visited.contains(nextNode)) {
					continue;
				}
				visited.add(nextNode);
				que.add(nextNode);
			}
		}
		return false;
	}
	
	private static Map<EvaluatableTerm, List<EvaluatableTerm>> constructEquationGraph(Collection<Formula> assumptions) {
		List<EquationFormula> equations = new ArrayList<>();
		for (Formula assumption : assumptions) {
			if (assumption instanceof EquationFormula) {
				equations.add((EquationFormula) assumption);
			}
		}
		
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = new HashMap<>();
		for (EquationFormula equation : equations) {
			EvaluatableTerm lsh = equation.getLeftSideHand();
			EvaluatableTerm rsh = equation.getRightSideHand();
			if (! graph.containsKey(lsh)) {
				graph.put(lsh, new ArrayList<>());
			}
			if (! graph.containsKey(rsh)) {
				graph.put(rsh, new ArrayList<>());
			}
			graph.get(lsh).add(rsh);
			graph.get(rsh).add(lsh);
		}
		return graph;
	}
}