Bob is nice. Erin is not cold. If something is kind then it is not cold. If Erin is young and Erin is kind then Erin is nice. Nice things are red.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
If something is kind then it is not cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
If Erin is young and Erin is kind then Erin is nice.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Bob is red.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "red" "+")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "red" "-")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is nice.[(triple1)] Erin is not cold.[(triple2)] @1: Bob is red.[(((triple1) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is not cold.
("Erin" "is" "cold" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1