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