Anne is big. Anne is kind. Anne is round. Bob is kind. Bob is smart. Charlie is big. Charlie is blue. If someone is blue and not kind then they are smart. Smart people are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
If someone is blue and not kind then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "smart" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple4)]
("Bob" "is" "kind" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple4)]
("Bob" "is" "kind" "-")
triple4
Bob is young.
True
2
proof
[(((triple5) -> rule2))]
("Bob" "is" "young" "+")
((triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple5) -> rule2))]
("Bob" "is" "young" "-")
((triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule2 <- 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 blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is round.[(triple3)] Bob is kind.[(triple4)] Bob is smart.[(triple5)] Charlie is big.[(triple6)] Charlie is blue.[(triple7)] @1: Bob is young.[(((triple5) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple5) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1