Anne is furry. Anne is kind. Anne is round. Anne is smart. Bob is white. Charlie is kind. Charlie is quiet. Charlie is white. Harry is furry. Harry is kind. Harry is quiet. Harry is red. Harry is round. Harry is smart. Harry is white. If something is kind and quiet then it is round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is kind and quiet then it is round.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Harry is white.
True
1
proof
[(triple15)]
("Harry" "is" "white" "+")
triple15
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is round.
True
3
proof
[(((triple6 triple7) -> rule1))]
("Charlie" "is" "round" "+")
((triple6 triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("Charlie" "is" "round" "-")
((triple6 triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is round.[(triple3)] Anne is smart.[(triple4)] Bob is white.[(triple5)] Charlie is kind.[(triple6)] Charlie is quiet.[(triple7)] Charlie is white.[(triple8)] Harry is furry.[(triple9)] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is red.[(triple12)] Harry is round.[(triple13 OR ((triple10 triple11) -> rule1))] Harry is smart.[(triple14)] Harry is white.[(triple15)] @1: Charlie is round.[(((triple6 triple7) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple10 triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Charlie is round.
("Charlie" "is" "round" "+")
((triple6 triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1