Anne is green. Anne is kind. Anne is round. Bob is big. Dave is big. Dave is green. Dave is kind. Dave is red. Dave is white. Dave is young. Fiona is big. Fiona is kind. Big, kind people are green. Kind, white people are big. If someone is young and round then they are red. If someone is kind and green then they are red. All round, green people are white. White, round people are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Big, kind people are green.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Kind, white people are big.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is young and round then they are red.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is kind and green then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All round, green people are white.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
White, round people are kind.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Fiona is big.
True
1
proof
[(triple11)]
("Fiona" "is" "big" "+")
triple11
Fiona is not big.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "big" "-")
triple11
Anne is red.
True
3
proof
[(((triple2 triple1) -> rule4) OR ((((((triple3 triple1) -> rule5) triple3) -> rule6) triple1) -> rule4))]
("Anne" "is" "red" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((triple3 triple1) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Fiona is not green.
False
3
inv-proof
[(((triple11 triple12) -> rule1))]
("Fiona" "is" "green" "-")
((triple11 triple12) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
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 kind.[(triple2 OR ((((triple3 triple1) -> rule5) triple3) -> rule6))] Anne is round.[(triple3)] Bob is big.[(triple4)] Dave is big.[(triple5 OR ((triple7 triple9) -> rule2))] Dave is green.[(triple6 OR ((triple5 triple7) -> rule1) OR ((((triple7 triple9) -> rule2) triple7) -> rule1))] Dave is kind.[(triple7)] Dave is red.[(triple8 OR ((triple7 triple6) -> rule4) OR ((triple7 ((triple5 triple7) -> rule1)) -> rule4) OR ((triple7 ((((triple7 triple9) -> rule2) triple7) -> rule1)) -> rule4))] Dave is white.[(triple9)] Dave is young.[(triple10)] Fiona is big.[(triple11)] Fiona is kind.[(triple12)] @1: Anne is red.[(((triple2 triple1) -> rule4) OR ((((((triple3 triple1) -> rule5) triple3) -> rule6) triple1) -> rule4))] Anne is white.[(((triple3 triple1) -> rule5))] Fiona is green.[(((triple11 triple12) -> rule1))] @2: Anne is big.[(((triple2 ((triple3 triple1) -> rule5)) -> rule2) OR ((((((triple3 triple1) -> rule5) triple3) -> rule6) ((triple3 triple1) -> rule5)) -> rule2))] Fiona is red.[(((triple12 ((triple11 triple12) -> rule1)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple3 triple1) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
((triple7 triple9) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
((triple5 triple7) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple7 triple9) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
((triple7 triple6) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple7 ((triple5 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple7 ((((triple7 triple9) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is kind.
("Fiona" "is" "kind" "+")
triple12
Anne is red.
("Anne" "is" "red" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((triple3 triple1) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((triple3 triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple11 triple12) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple2 ((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple3 triple1) -> (rule5 % int3)) triple3) -> (rule6 % int2)) ((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((triple12 ((triple11 triple12) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2