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