Bob is blue. Bob is cold. Bob is green. Bob is quiet. Bob is round. Bob is smart. Bob is white. All smart people are green. If someone is quiet then they are smart. All smart people are cold. All smart people are cold. Cold people are green. If someone is round then they are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule3) OR ((triple6) -> rule4) OR ((((triple4) -> rule2)) -> rule3) OR ((((triple4) -> rule2)) -> rule4) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule4))]
("Bob" "is" "cold" "-")
triple2
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple6) -> rule3) OR ((triple6) -> rule4) OR ((((triple4) -> rule2)) -> rule3) OR ((((triple4) -> rule2)) -> rule4) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule4))] Bob is green.[(triple3 OR ((triple2) -> rule5) OR ((triple6) -> rule1) OR ((((triple4) -> rule2)) -> rule1) OR ((((triple5) -> rule6)) -> rule1) OR ((((triple6) -> rule3)) -> rule5) OR ((((triple6) -> rule4)) -> rule5) OR ((((((triple4) -> rule2)) -> rule3)) -> rule5) OR ((((((triple4) -> rule2)) -> rule4)) -> rule5) OR ((((((triple5) -> rule6)) -> rule3)) -> rule5) OR ((((((triple5) -> rule6)) -> rule4)) -> rule5))] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple4) -> rule2) OR ((triple5) -> rule6))] Bob is white.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple6) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7