Bob is furry. Bob is quiet. Bob is red. Charlie is big. Charlie is furry. Charlie is young. Dave is big. Dave is blue. Dave is furry. Dave is red. Dave is rough. Harry is big. Harry is quiet. Harry is red. Harry is young. Furry, big things are red. If something is red then it is quiet.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Furry, big things are red.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple12)]
("Harry" "is" "big" "-")
triple12
Charlie is red.
True
3
proof
[(((triple5 triple4) -> rule1))]
("Charlie" "is" "red" "+")
((triple5 triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "-")
((triple10) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is quiet.
True
4
proof
[(((((triple5 triple4) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple5 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not quiet.
False
4
inv-proof
[(((((triple5 triple4) -> rule1)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple5 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is furry.[(triple1)] Bob is quiet.[(triple2 OR ((triple3) -> rule2))] Bob is red.[(triple3)] Charlie is big.[(triple4)] Charlie is furry.[(triple5)] Charlie is young.[(triple6)] Dave is big.[(triple7)] Dave is blue.[(triple8)] Dave is furry.[(triple9)] Dave is red.[(triple10 OR ((triple9 triple7) -> rule1))] Dave is rough.[(triple11)] Harry is big.[(triple12)] Harry is quiet.[(triple13 OR ((triple14) -> rule2))] Harry is red.[(triple14)] Harry is young.[(triple15)] @1: Charlie is red.[(((triple5 triple4) -> rule1))] Dave is quiet.[(((triple10) -> rule2) OR ((((triple9 triple7) -> rule1)) -> rule2))] @2: Charlie is quiet.[(((((triple5 triple4) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
((triple9 triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple14) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Charlie is red.
("Charlie" "is" "red" "+")
((triple5 triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple9 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple5 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2