Charlie is not furry. Charlie is white. Charlie is young. If someone is red and not young then they are white. Rough people are not red. Round people are not red. If someone is smart then they are red. All white people are not smart. All white, red people are not smart. If Charlie is furry then Charlie is smart. If Charlie is smart and Charlie is round then Charlie is not red.
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is red and not young then they are white.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "+"))
Rough people are not red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
Round people are not red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All white people are not smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "-"))
All white, red people are not smart.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "-"))
If Charlie is furry then Charlie is smart.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "smart" "+"))
If Charlie is smart and Charlie is round then Charlie is not red.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "-"))
Charlie is white.
True
1
proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "-")
triple2
Charlie is not smart.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is smart.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is not furry.[(triple1)] Charlie is white.[(triple2)] Charlie is young.[(triple3)] @1: Charlie is not smart.[(((triple2) -> rule5))]
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1