Bob is kind. Harry is white. Red, blue people are green. If someone is green and red then they are kind. White people are kind. All green people are furry. Kind, white people are green. Furry, green people are blue.
Bob is kind.
("Bob" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
Red, blue people are green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is green and red then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Kind, white people are green.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Furry, green people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Harry is white.
True
1
proof
[(triple2)]
("Harry" "is" "white" "+")
triple2
Harry is not white.
False
1
inv-proof
[(triple2)]
("Harry" "is" "white" "-")
triple2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is kind.[(triple1)] Harry is white.[(triple2)] @1: Harry is kind.[(((triple2) -> rule3))] @2: Harry is green.[(((((triple2) -> rule3) triple2) -> rule5))] @3: Harry is furry.[(((((((triple2) -> rule3) triple2) -> rule5)) -> rule4))] @4: Harry is blue.[(((((((((triple2) -> rule3) triple2) -> rule5)) -> rule4) ((((triple2) -> rule3) triple2) -> rule5)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple2) -> (rule3 % int4)) triple2) -> (rule5 % int3))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4