Anne is kind. Bob is furry. Bob is green. Bob is kind. Erin is blue. Erin is not smart. Harry is kind. If Anne is rough then Anne is smart. Green things are nice. All smart things are nice. If something is furry and kind then it is rough. If something is nice then it is blue. If something is blue and not kind then it is green.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If Anne is rough then Anne is smart.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is furry and kind then it is rough.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is blue and not kind then it is green.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "green" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Erin is not blue.
False
1
inv-proof
[(triple5)]
("Erin" "is" "blue" "-")
triple5
Bob is nice.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("Bob" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("Bob" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Anne" "is" "nice" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "+")
Anne is not blue.
Unknown
inv-rconc
[@4: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule1 <- rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is kind.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is kind.[(triple4)] Erin is blue.[(triple5)] Erin is not smart.[(triple6)] Harry is kind.[(triple7)] @1: Bob is nice.[(((triple3) -> rule2))] Bob is rough.[(((triple2 triple4) -> rule4))] @2: Bob is blue.[(((((triple3) -> rule2)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2 triple4) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2