/* The three-theorem provers example. */ // the first theorem prover always gives a correct answer, but is // only able to find the solution of one formula source(3): first_consistent // the second theorem prover is faster but approximate source(2): -first_consistent&second_consistent // the rough estimation of satisfiability source(1): first_consistent&-second_consistent&third_consistent // all the formulas should be considered consistent query: first_consistent&second_consistent&third_consistent