Anne is round. Anne is young. Bob is round. Young people are green. Green people are kind. Round people are red. All young, round people are white. Green, white people are round. All quiet, kind people are red.
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is round.
("Bob" "is" "round" "+")
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All young, round people are white.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Green, white people are round.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Bob is round.
True
1
proof
[(triple3)]
("Bob" "is" "round" "+")
triple3
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Anne is white.
True
3
proof
[(((triple2 triple1) -> rule4))]
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "red" "-")
((triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is round.[(triple1)] Anne is young.[(triple2)] Bob is round.[(triple3)] @1: Anne is green.[(((triple2) -> rule1))] Anne is red.[(((triple1) -> rule3))] Anne is white.[(((triple2 triple1) -> rule4))] Bob is red.[(((triple3) -> rule3))] @2: Anne is kind.[(((((triple2) -> rule1)) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2