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