Charlie is kind. Gary is furry. Gary is rough. If something is rough then it is white. Rough things are smart. White things are rough. All red, smart things are white. Kind things are red. White, nice things are furry. If Charlie is red then Charlie is white. If something is nice and smart then it is white.
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
All red, smart things are white.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
White, nice things are furry.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Charlie is red then Charlie is white.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "white" "+"))
If something is nice and smart then it is white.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Gary is not furry.
False
1
inv-proof
[(triple2)]
("Gary" "is" "furry" "-")
triple2
Charlie is red.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] Gary is furry.[(triple2)] Gary is rough.[(triple3)] @1: Charlie is red.[(((triple1) -> rule5))] Gary is smart.[(((triple3) -> rule2))] Gary is white.[(((triple3) -> rule1))] @2: Charlie is white.[(((((triple1) -> rule5)) -> rule7))] @3: Charlie is rough.[(((((((triple1) -> rule5)) -> rule7)) -> rule3))] @4: Charlie is smart.[(((((((((triple1) -> rule5)) -> rule7)) -> rule3)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4