Anne is not cold. Anne is not red. Anne is not white. Harry is blue. Harry is cold. Harry is kind. Harry is white. White, red people are not quiet. If someone is rough then they are quiet. Blue people are rough. All blue people are rough. If Anne is rough then Anne is not white. Quiet people are not red. If someone is red and not rough then they are not kind. If someone is quiet and not cold then they are not kind.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is not red.
("Anne" "is" "red" "-")
Anne is not white.
("Anne" "is" "white" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
White, red people are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "-"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Anne is rough then Anne is not white.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "white" "-"))
Quiet people are not red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
If someone is red and not rough then they are not kind.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "kind" "-"))
If someone is quiet and not cold then they are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "kind" "-"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Harry is rough.
True
2
proof
[(((triple4) -> rule3) OR ((triple4) -> rule4))]
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple4) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple4) -> rule4))]
("Harry" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple4) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not red.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule6) OR ((((((triple4) -> rule4)) -> rule2)) -> rule6))]
("Harry" "is" "red" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule6) OR ((((((triple4) -> rule4)) -> rule2)) -> rule6))]
("Harry" "is" "red" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is not cold.[(triple1)] Anne is not red.[(triple2)] Anne is not white.[(triple3)] Harry is blue.[(triple4)] Harry is cold.[(triple5)] Harry is kind.[(triple6)] Harry is white.[(triple7)] @1: Harry is rough.[(((triple4) -> rule3) OR ((triple4) -> rule4))] @2: Harry is quiet.[(((((triple4) -> rule3)) -> rule2) OR ((((triple4) -> rule4)) -> rule2))] @3: Harry is not red.[(((((((triple4) -> rule3)) -> rule2)) -> rule6) OR ((((((triple4) -> rule4)) -> rule2)) -> rule6))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple4) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not red.
("Harry" "is" "red" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3