Bob is cold. Bob is kind. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is young. All cold, young things are red. If something is young then it is nice. If something is young and round then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
All cold, young things are red.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is young and round then it is red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3 OR ((triple7) -> rule2))] Bob is red.[(triple4 OR ((triple1 triple7) -> rule1) OR ((triple7 triple6) -> rule3))] Bob is rough.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple7) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple1 triple7) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple7 triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7