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