Anne is smart. Charlie is blue. If someone is round then they are smart. Smart people are rough. If someone is rough then they are red.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Anne is rough.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
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 blue.[(triple2)] @1: Anne is rough.[(((triple1) -> rule2))] @2: Anne is red.[(((((triple1) -> rule2)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2