Anne is blue. Anne is nice. Bob is blue. Bob is round. Dave is kind. Dave is not nice. Erin is nice. If someone is white then they are kind. If Anne is not round then Anne is not kind. If someone is round and not blue then they are not white. All nice, round people are rough. All blue people are nice. If someone is kind and smart then they are nice. If someone is nice and not white then they are not smart. If someone is rough then they are not smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Anne is not round then Anne is not kind.
((("Anne" "is" "round" "~")) -> ("Anne" "is" "kind" "-"))
If someone is round and not blue then they are not white.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "-"))
All nice, round people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and smart then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and not white then they are not smart.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "smart" "-"))
If someone is rough then they are not smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
Dave is kind.
True
1
proof
[(triple5)]
("Dave" "is" "kind" "+")
triple5
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Bob is nice.
True
2
proof
[(((triple3) -> rule5))]
("Bob" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
True
4
proof
[(((((triple3) -> rule5) triple4) -> rule4))]
("Bob" "is" "rough" "+")
((((triple3) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple3) -> rule5) triple4) -> rule4))]
("Bob" "is" "rough" "-")
((((triple3) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not smart.
True
5
proof
[(((((((triple3) -> rule5) triple4) -> rule4)) -> rule8))]
("Bob" "is" "smart" "-")
((((((triple3) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is smart.
False
5
inv-proof
[(((((((triple3) -> rule5) triple4) -> rule4)) -> rule8))]
("Bob" "is" "smart" "+")
((((((triple3) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2 OR ((triple1) -> rule5))] Bob is blue.[(triple3)] Bob is round.[(triple4)] Dave is kind.[(triple5)] Dave is not nice.[(triple6)] Erin is nice.[(triple7)] @1: Bob is nice.[(((triple3) -> rule5))] @2: Bob is rough.[(((((triple3) -> rule5) triple4) -> rule4))] @3: Bob is not smart.[(((((((triple3) -> rule5) triple4) -> rule4)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not nice.
("Dave" "is" "nice" "-")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple3) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not smart.
("Bob" "is" "smart" "-")
((((((triple3) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3