Anne is big. Anne is furry. Anne is green. Anne is quiet. Anne is smart. Bob is big. Bob is green. Bob is quiet. Bob is red. Bob is smart. Charlie is furry. Charlie is red. Gary is big. Gary is kind. Gary is quiet. Gary is red. Furry things are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Gary is big.
True
1
proof
[(triple13)]
("Gary" "is" "big" "+")
triple13
Gary is not quiet.
False
1
inv-proof
[(triple15)]
("Gary" "is" "quiet" "-")
triple15
Charlie is quiet.
True
2
proof
[(((triple11) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple11) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple11) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple11) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3)] Anne is quiet.[(triple4 OR ((triple2) -> rule1))] Anne is smart.[(triple5)] Bob is big.[(triple6)] Bob is green.[(triple7)] Bob is quiet.[(triple8)] Bob is red.[(triple9)] Bob is smart.[(triple10)] Charlie is furry.[(triple11)] Charlie is red.[(triple12)] Gary is big.[(triple13)] Gary is kind.[(triple14)] Gary is quiet.[(triple15)] Gary is red.[(triple16)] @1: Charlie is quiet.[(((triple11) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple2) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is green.
("Bob" "is" "green" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is red.
("Bob" "is" "red" "+")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
triple11
Charlie is red.
("Charlie" "is" "red" "+")
triple12
Gary is big.
("Gary" "is" "big" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple16
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple11) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1