Bob is round. Charlie is blue. Erin is round. Harry is red. Green, blue people are round. If someone is green and red then they are round. If Harry is blue then Harry is green.
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Green, blue people are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is green and red then they are round.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Harry is blue then Harry is green.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple4)]
("Harry" "is" "red" "-")
triple4
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is round.[(triple1)] Charlie is blue.[(triple2)] Erin is round.[(triple3)] Harry is red.[(triple4)]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4