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