Anne is white. Bob is kind. Harry is white. If someone is kind then they are not blue. All young people are quiet. White people are kind. If someone is kind and round then they are not white. If someone is kind and not quiet then they are rough. If Harry is not blue then Harry is not rough.
Anne is white.
("Anne" "is" "white" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is kind then they are not blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and round then they are not white.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
If someone is kind and not quiet then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "rough" "+"))
If Harry is not blue then Harry is not rough.
((("Harry" "is" "blue" "~")) -> ("Harry" "is" "rough" "-"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Bob is not blue.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is not blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Harry" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is not rough.
True
4
proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule6))]
("Harry" "is" "rough" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is rough.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule6))]
("Harry" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is white.[(triple1)] Bob is kind.[(triple2)] Harry is white.[(triple3)] @1: Anne is kind.[(((triple1) -> rule3))] Bob is not blue.[(((triple2) -> rule1))] Harry is kind.[(((triple3) -> rule3))] @2: Anne is not blue.[(((((triple1) -> rule3)) -> rule1))] Harry is not blue.[(((((triple3) -> rule3)) -> rule1))] @3: Harry is not rough.[(((((((triple3) -> rule3)) -> rule1)) -> rule6))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3