Anne is green. Anne is red. Bob is cold. Bob is not green. Bob is kind. Bob is nice. Bob is not young. Red, young people are cold. Red, big people are cold. If someone is kind and red then they are not young. If someone is young and not kind then they are nice. If someone is red and green then they are nice. If someone is red and nice then they are big. If someone is nice and young then they are red. All young, kind people are not red.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not young.
("Bob" "is" "young" "-")
Red, young people are cold.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Red, big people are cold.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind and red then they are not young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "-"))
If someone is young and not kind then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If someone is red and green then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and nice then they are big.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and young then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All young, kind people are not red.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
Anne is red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple6)]
("Bob" "is" "nice" "-")
triple6
Anne is nice.
True
3
proof
[(((triple2 triple1) -> rule5))]
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule5))]
("Anne" "is" "nice" "-")
((triple2 triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
True
5
proof
[(((triple2 ((triple2 triple1) -> rule5)) -> rule6))]
("Anne" "is" "big" "+")
((triple2 ((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
False
5
inv-proof
[(((triple2 ((triple2 triple1) -> rule5)) -> rule6))]
("Anne" "is" "big" "-")
((triple2 ((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
True
7
proof
[(((triple2 ((triple2 ((triple2 triple1) -> rule5)) -> rule6)) -> rule2))]
("Anne" "is" "cold" "+")
((triple2 ((triple2 ((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not cold.
False
7
inv-proof
[(((triple2 ((triple2 ((triple2 triple1) -> rule5)) -> rule6)) -> rule2))]
("Anne" "is" "cold" "-")
((triple2 ((triple2 ((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "red" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Bob is cold.[(triple3)] Bob is kind.[(triple5)] Bob is nice.[(triple6)] Bob is not green.[(triple4)] Bob is not young.[(triple7)] @1: Anne is nice.[(((triple2 triple1) -> rule5))] @2: Anne is big.[(((triple2 ((triple2 triple1) -> rule5)) -> rule6))] @3: Anne is cold.[(((triple2 ((triple2 ((triple2 triple1) -> rule5)) -> rule6)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is nice.
("Bob" "is" "nice" "+")
triple6
Bob is not green.
("Bob" "is" "green" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple2 ((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 ((triple2 ((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3