Charlie is blue. Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is white. Dave is blue. Dave is kind. Dave is quiet. Dave is red. Dave is rough. Gary is blue. Gary is quiet. Gary is red. Gary is white. If something is white and cold then it is rough. If something is white then it is red. If something is rough and cold then it is red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is white and cold then it is rough.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is rough and cold then it is red.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple9)]
("Dave" "is" "kind" "+")
triple9
Gary is not white.
False
1
inv-proof
[(triple16)]
("Gary" "is" "white" "-")
triple16
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5 OR ((triple7) -> rule2) OR ((triple6 triple2) -> rule3) OR ((((triple7 triple2) -> rule1) triple2) -> rule3))] Charlie is rough.[(triple6 OR ((triple7 triple2) -> rule1))] Charlie is white.[(triple7)] Dave is blue.[(triple8)] Dave is kind.[(triple9)] Dave is quiet.[(triple10)] Dave is red.[(triple11)] Dave is rough.[(triple12)] Gary is blue.[(triple13)] Gary is quiet.[(triple14)] Gary is red.[(triple15 OR ((triple16) -> rule2))] Gary is white.[(triple16)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple7) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple6 triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple7 triple2) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple7 triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is red.
("Gary" "is" "red" "+")
triple15
((triple16) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple16