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