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