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