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