Anne is quiet. Charlie is big. Charlie is furry. Charlie is kind. Gary is not furry. Gary is rough. Gary is round. Harry is furry. Harry is kind. Harry is quiet. Harry is rough. Harry is round. If something is big then it is kind. Furry things are kind. If Harry is furry then Harry is rough. If something is big and not young then it is round. Big, rough things are not round. All young things are round. All furry, young things are big. All young, furry things are quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Harry is furry then Harry is rough.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "rough" "+"))
If something is big and not young then it is round.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
Big, rough things are not round.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All furry, young things are big.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All young, furry things are quiet.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Harry is furry.
True
1
proof
[(triple8)]
("Harry" "is" "furry" "+")
triple8
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is quiet.[(triple1)] Charlie is big.[(triple2)] Charlie is furry.[(triple3)] Charlie is kind.[(triple4 OR ((triple2) -> rule1) OR ((triple3) -> rule2))] Gary is not furry.[(triple5)] Gary is rough.[(triple6)] Gary is round.[(triple7)] Harry is furry.[(triple8)] Harry is kind.[(triple9 OR ((triple8) -> rule2))] Harry is quiet.[(triple10)] Harry is rough.[(triple11 OR ((triple8) -> rule3))] Harry is round.[(triple12)]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple8) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple8) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple12