Anne is furry. Charlie is big. Dave is young. Fiona is white. If something is round then it is big. Kind, furry things are young. If something is kind then it is white. Furry things are young. Kind things are furry. All furry things are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Kind, furry things are young.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Dave is young.
True
1
proof
[(triple3)]
("Dave" "is" "young" "+")
triple3
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "furry" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Dave is young.[(triple3)] Fiona is white.[(triple4)] @1: Anne is kind.[(((triple1) -> rule6))] Anne is young.[(((triple1) -> rule4) OR ((((triple1) -> rule6) triple1) -> rule2))] @2: Anne is white.[(((((triple1) -> rule6)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2