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