Bob is blue. Bob is kind. Bob is red. Bob is rough. Bob is young. Dave is rough. Dave is white. Dave is not young. Gary is big. Gary is blue. Gary is red. Gary is rough. Gary is young. Harry is blue. Harry is not red. Harry is not young. All white things are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is not young.
("Harry" "is" "young" "-")
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Dave is young.
False
1
inv-proof
[(triple8)]
("Dave" "is" "young" "+")
triple8
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4)] Bob is young.[(triple5)] Dave is not young.[(triple8)] Dave is rough.[(triple6)] Dave is white.[(triple7)] Gary is big.[(triple9)] Gary is blue.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] Gary is young.[(triple13)] Harry is blue.[(triple14)] Harry is not red.[(triple15)] Harry is not young.[(triple16)] @1: Dave is kind.[(((triple7) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is not young.
("Dave" "is" "young" "-")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is young.
("Gary" "is" "young" "+")
triple13
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is not red.
("Harry" "is" "red" "-")
triple15
Harry is not young.
("Harry" "is" "young" "-")
triple16
Dave is kind.
("Dave" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1