Anne is smart. Bob is nice. Erin is rough. Harry is kind. If someone is green then they are kind. All nice people are green. If Erin is kind and Erin is rough then Erin is quiet.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Erin is kind and Erin is rough then Erin is quiet.
((("Erin" "is" "kind" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "quiet" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Bob is green.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "green" "-")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Erin is quiet.
Unknown
rconc
[@3: Erin is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is smart.[(triple1)] Bob is nice.[(triple2)] Erin is rough.[(triple3)] Harry is kind.[(triple4)] @1: Bob is green.[(((triple2) -> rule2))] @2: Bob is kind.[(((((triple2) -> rule2)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2