Bob is blue. Bob is cold. Bob is nice. Bob is rough. Bob is round. Bob is smart. Bob is young. Nice, blue things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Nice, blue things are smart.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Bob is nice.
True
1
proof
[(triple3)]
("Bob" "is" "nice" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple6 OR ((triple3 triple1) -> rule1))]
("Bob" "is" "smart" "-")
triple6
((triple3 triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is nice.[(triple3)] Bob is rough.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple3 triple1) -> rule1))] Bob is young.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3 triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7