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