Anne is white. Charlie is furry. Charlie is nice. Charlie is white. Dave is big. Dave is blue. Dave is furry. All big, white people are young. If Dave is red then Dave is young. All white, blue people are nice. If Charlie is young then Charlie is blue. All young, red people are blue. If someone is young and furry then they are red. If someone is nice then they are young. Blue, red people are big.
Anne is white.
("Anne" "is" "white" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
All big, white people are young.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Dave is red then Dave is young.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "young" "+"))
All white, blue people are nice.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is young then Charlie is blue.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "blue" "+"))
All young, red people are blue.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and furry then they are red.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Blue, red people are big.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Charlie is young.
True
2
proof
[(((triple3) -> rule7))]
("Charlie" "is" "young" "+")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "young" "-")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
True
4
proof
[(((((triple3) -> rule7) triple2) -> rule6))]
("Charlie" "is" "red" "+")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple3) -> rule7) triple2) -> rule6))]
("Charlie" "is" "red" "-")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
True
8
proof
[(((((((triple3) -> rule7)) -> rule4) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule7) ((((triple3) -> rule7) triple2) -> rule6)) -> rule5) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "+")
((((((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not big.
False
8
inv-proof
[(((((((triple3) -> rule7)) -> rule4) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule7) ((((triple3) -> rule7) triple2) -> rule6)) -> rule5) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "-")
((((((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is young.
Unknown
rconc
[@4: Anne is young.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is young.
Unknown
rconc
[@4: Dave is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule7 <- rule3 <- FAIL)]]
("Dave" "is" "young" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is white.[(triple1)] Charlie is furry.[(triple2)] Charlie is nice.[(triple3)] Charlie is white.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6)] Dave is furry.[(triple7)] @1: Charlie is young.[(((triple3) -> rule7))] @2: Charlie is blue.[(((((triple3) -> rule7)) -> rule4) OR ((((triple3) -> rule7) ((((triple3) -> rule7) triple2) -> rule6)) -> rule5))] Charlie is red.[(((((triple3) -> rule7) triple2) -> rule6))] @3: Charlie is big.[(((((((triple3) -> rule7)) -> rule4) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule7) ((((triple3) -> rule7) triple2) -> rule6)) -> rule5) ((((triple3) -> rule7) triple2) -> rule6)) -> rule8))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple3) -> (rule7 % int3)) ((((triple3) -> (rule7 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((triple3) -> (rule7 % int2)) triple2) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple3) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((triple3) -> (rule7 % int4)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule5 % int2)) ((((triple3) -> (rule7 % int4)) triple2) -> (rule6 % int3))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4