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