Anne is red. Charlie is big. All red, round things are cold. If something is big then it is cold. If something is cold then it is green.
Anne is red.
("Anne" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
All red, round things are cold.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Charlie is cold.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is red.[(triple1)] Charlie is big.[(triple2)] @1: Charlie is cold.[(((triple2) -> rule2))] @2: Charlie is green.[(((((triple2) -> rule2)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2