Bob is blue. Bob is red. Dave is big. Dave is blue. Dave is furry. Dave is nice. Dave is quiet. Gary is not big. Gary is blue. Gary is not furry. Gary is rough. Harry is big. Harry is blue. Harry is furry. Harry is nice. Harry is rough. All rough, quiet people are red. All big people are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All rough, quiet people are red.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple16 OR ((triple12) -> rule2))]
("Harry" "is" "rough" "+")
triple16
((triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is not blue.
False
1
inv-proof
[(triple4)]
("Dave" "is" "blue" "-")
triple4
Dave is rough.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
True
4
proof
[(((((triple3) -> rule2) triple7) -> rule1))]
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not red.
False
4
inv-proof
[(((((triple3) -> rule2) triple7) -> rule1))]
("Dave" "is" "red" "-")
((((triple3) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is red.[(triple2)] Dave is big.[(triple3)] Dave is blue.[(triple4)] Dave is furry.[(triple5)] Dave is nice.[(triple6)] Dave is quiet.[(triple7)] Gary is blue.[(triple9)] Gary is not big.[(triple8)] Gary is not furry.[(triple10)] Gary is rough.[(triple11)] Harry is big.[(triple12)] Harry is blue.[(triple13)] Harry is furry.[(triple14)] Harry is nice.[(triple15)] Harry is rough.[(triple16 OR ((triple12) -> rule2))] @1: Dave is rough.[(((triple3) -> rule2))] @2: Dave is red.[(((((triple3) -> rule2) triple7) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is not big.
("Gary" "is" "big" "-")
triple8
Gary is not furry.
("Gary" "is" "furry" "-")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
((triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2