Dave is kind. Fiona is kind. Harry is green. Red people are kind. All white people are cold. If someone is kind then they are cold. Cold, kind people are not red. If someone is red then they are green. If someone is furry and green then they are young. All green people are young. If someone is white and not red then they are not furry.
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Cold, kind people are not red.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is furry and green then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is white and not red then they are not furry.
((("someone" "is" "white" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "furry" "-"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Dave" "is" "young" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Dave is kind.[(triple1)] Fiona is kind.[(triple2)] Harry is green.[(triple3)] @1: Dave is cold.[(((triple1) -> rule3))] Fiona is cold.[(((triple2) -> rule3))] Harry is young.[(((triple3) -> rule7))] @2: Dave is not red.[(((((triple1) -> rule3) triple1) -> rule4))] Fiona is not red.[(((((triple2) -> rule3) triple2) -> rule4))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2