Bob is rough. Bob is smart. Bob is white. Dave is blue. Dave is not cold. Harry is not cold. Harry is not nice. If something is rough and green then it is blue. Rough, smart things are not blue. All cold things are white.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not nice.
("Harry" "is" "nice" "-")
If something is rough and green then it is blue.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Rough, smart things are not blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "-"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Harry is not cold.
True
1
proof
[(triple6)]
("Harry" "is" "cold" "-")
triple6
Harry is cold.
False
1
inv-proof
[(triple6)]
("Harry" "is" "cold" "+")
triple6
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is rough.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Dave is blue.[(triple4)] Dave is not cold.[(triple5)] Harry is not cold.[(triple6)] Harry is not nice.[(triple7)] @1: Bob is not blue.[(((triple1 triple2) -> rule2))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is not cold.
("Dave" "is" "cold" "-")
triple5
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple7
Bob is not blue.
("Bob" "is" "blue" "-")
((triple1 triple2) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1