Charlie is furry. Fiona is blue. Harry is rough. If someone is blue then they are red. Furry people are red. If someone is furry and green then they are blue.
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and green then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Harry is rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "+")
triple3
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Fiona is red.
True
2
proof
[(((triple2) -> rule1))]
("Fiona" "is" "red" "+")
((triple2) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "red" "-")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Charlie is furry.[(triple1)] Fiona is blue.[(triple2)] Harry is rough.[(triple3)] @1: Charlie is red.[(((triple1) -> rule2))] Fiona is red.[(((triple2) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple2) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1