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