Anne is big. Anne is furry. Anne is kind. Anne is nice. Anne is quiet. Anne is young. Bob is furry. Bob is kind. Bob is nice. Bob is red. Harry is furry. Harry is kind. Harry is nice. Harry is quiet. Harry is young. Red people are quiet. All red people are young. If someone is kind and young then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and young then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Anne is young.
True
1
proof
[(triple6)]
("Anne" "is" "young" "+")
triple6
Anne is not quiet.
False
1
inv-proof
[(triple5 OR ((triple3 triple6) -> rule3))]
("Anne" "is" "quiet" "-")
triple5
((triple3 triple6) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4)] Anne is quiet.[(triple5 OR ((triple3 triple6) -> rule3))] Anne is young.[(triple6)] Bob is furry.[(triple7)] Bob is kind.[(triple8)] Bob is nice.[(triple9)] Bob is red.[(triple10)] Harry is furry.[(triple11)] Harry is kind.[(triple12)] Harry is nice.[(triple13)] Harry is quiet.[(triple14 OR ((triple12 triple15) -> rule3))] Harry is young.[(triple15)] @1: Bob is quiet.[(((triple10) -> rule1) OR ((triple8 ((triple10) -> rule2)) -> rule3))] Bob is young.[(((triple10) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple3 triple6) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
triple8
Bob is nice.
("Bob" "is" "nice" "+")
triple9
Bob is red.
("Bob" "is" "red" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
((triple12 triple15) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple8 ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple10) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1