Anne is smart. Charlie is furry. Erin is quiet. Rough things are smart. Furry things are rough. If Anne is kind and Anne is not rough then Anne is blue.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Anne is kind and Anne is not rough then Anne is blue.
((("Anne" "is" "kind" "+") ("Anne" "is" "rough" "~")) -> ("Anne" "is" "blue" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "smart" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is smart.[(triple1)] Charlie is furry.[(triple2)] Erin is quiet.[(triple3)] @1: Charlie is rough.[(((triple2) -> rule2))] @2: Charlie is smart.[(((((triple2) -> rule2)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2