Anne is blue. Bob is cold. All rough people are cold. If someone is blue and quiet then they are kind. All nice people are kind. Rough, smart people are not blue. Cold people are nice. Kind people are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and quiet then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Rough, smart people are not blue.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Bob is nice.
True
2
proof
[(((triple2) -> rule5))]
("Bob" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule3))]
("Bob" "is" "kind" "-")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
True
4
proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "-")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@4: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is kind.
Unknown
rconc
[@5: Anne is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is nice.
Unknown
rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Bob is cold.[(triple2)] @1: Bob is nice.[(((triple2) -> rule5))] @2: Bob is kind.[(((((triple2) -> rule5)) -> rule3))] @3: Bob is quiet.[(((((((triple2) -> rule5)) -> rule3)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3