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