Anne is white. Bob is cold. All kind people are rough. If someone is white and green then they are cold. If Anne is white then Anne is cold. White, big people are rough. If Bob is kind then Bob is white. Blue people are green. If Bob is green then Bob is blue. If Anne is cold then Anne is rough.
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is white and green then they are cold.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Anne is white then Anne is cold.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "cold" "+"))
White, big people are rough.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Bob is kind then Bob is white.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "white" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Bob is green then Bob is blue.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "blue" "+"))
If Anne is cold then Anne is rough.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "rough" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is cold.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is white.[(triple1)] Bob is cold.[(triple2)] @1: Anne is cold.[(((triple1) -> rule3))] @2: Anne is rough.[(((((triple1) -> rule3)) -> rule8))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2