Bob is smart. Dave is furry. Fiona is rough. If someone is blue and not nice then they are not green. All round, green people are smart. All rough people are not smart. If Bob is green then Bob is smart. If Dave is not nice then Dave is not blue. Nice, round people are blue. If Dave is rough then Dave is not round. If Bob is smart and Bob is blue then Bob is green.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is blue and not nice then they are not green.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "-"))
All round, green people are smart.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All rough people are not smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
If Bob is green then Bob is smart.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
If Dave is not nice then Dave is not blue.
((("Dave" "is" "nice" "~")) -> ("Dave" "is" "blue" "-"))
Nice, round people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Dave is rough then Dave is not round.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "round" "-"))
If Bob is smart and Bob is blue then Bob is green.
((("Bob" "is" "smart" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "green" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Dave is furry.[(triple2)] Fiona is rough.[(triple3)] @1: Fiona is not smart.[(((triple3) -> rule3))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Fiona is not smart.
("Fiona" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1