Anne is furry. Anne is red. Anne is round. Anne is smart. Anne is white. Anne is young. Charlie is round. Charlie is smart. Charlie is young. Erin is furry. Gary is not smart. Gary is white. Round people are red. If someone is young then they are round. If someone is red and not furry then they are not white. All round, nice people are white. If someone is red then they are nice. All round, red people are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is white.
("Gary" "is" "white" "+")
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is red and not furry then they are not white.
((("someone" "is" "red" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "-"))
All round, nice people are white.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All round, red people are smart.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple2 OR ((triple3) -> rule1) OR ((((triple6) -> rule2)) -> rule1))]
("Anne" "is" "red" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not young.
False
1
inv-proof
[(triple6)]
("Anne" "is" "young" "-")
triple6
Anne is nice.
True
2
proof
[(((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Charlie is nice.
True
3
proof
[(((((triple7) -> rule1)) -> rule5) OR ((((((triple9) -> rule2)) -> rule1)) -> rule5))]
("Charlie" "is" "nice" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not nice.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule5) OR ((((((triple9) -> rule2)) -> rule1)) -> rule5))]
("Charlie" "is" "nice" "-")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not nice.
Unknown
inv-rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2 OR ((triple3) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Anne is round.[(triple3 OR ((triple6) -> rule2))] Anne is smart.[(triple4 OR ((triple3 triple2) -> rule6) OR ((triple3 ((triple3) -> rule1)) -> rule6) OR ((((triple6) -> rule2) triple2) -> rule6) OR ((((triple6) -> rule2) ((triple3) -> rule1)) -> rule6) OR ((triple3 ((((triple6) -> rule2)) -> rule1)) -> rule6) OR ((((triple6) -> rule2) ((((triple6) -> rule2)) -> rule1)) -> rule6))] Anne is white.[(triple5 OR ((triple3 ((triple2) -> rule5)) -> rule4) OR ((((triple6) -> rule2) ((triple2) -> rule5)) -> rule4) OR ((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule4) OR ((((triple6) -> rule2) ((((triple3) -> rule1)) -> rule5)) -> rule4) OR ((triple3 ((((((triple6) -> rule2)) -> rule1)) -> rule5)) -> rule4) OR ((((triple6) -> rule2) ((((((triple6) -> rule2)) -> rule1)) -> rule5)) -> rule4))] Anne is young.[(triple6)] Charlie is round.[(triple7 OR ((triple9) -> rule2))] Charlie is smart.[(triple8 OR ((triple7 ((triple7) -> rule1)) -> rule6) OR ((((triple9) -> rule2) ((triple7) -> rule1)) -> rule6) OR ((triple7 ((((triple9) -> rule2)) -> rule1)) -> rule6) OR ((((triple9) -> rule2) ((((triple9) -> rule2)) -> rule1)) -> rule6))] Charlie is young.[(triple9)] Erin is furry.[(triple10)] Gary is not smart.[(triple11)] Gary is white.[(triple12)] @1: Anne is nice.[(((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule2)) -> rule1)) -> rule5))] Charlie is red.[(((triple7) -> rule1) OR ((((triple9) -> rule2)) -> rule1))] @2: Charlie is nice.[(((((triple7) -> rule1)) -> rule5) OR ((((((triple9) -> rule2)) -> rule1)) -> rule5))] @3: Charlie is white.[(((triple7 ((((triple7) -> rule1)) -> rule5)) -> rule4) OR ((((triple9) -> rule2) ((((triple7) -> rule1)) -> rule5)) -> rule4) OR ((triple7 ((((((triple9) -> rule2)) -> rule1)) -> rule5)) -> rule4) OR ((((triple9) -> rule2) ((((((triple9) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
triple3
((triple6) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple3 triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple6) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple3 ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple6) -> (rule2 % int3)) ((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple3 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((triple6) -> (rule2 % int4)) ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((triple3 ((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((triple6) -> (rule2 % int4)) ((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple9) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple7 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple7 ((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple9) -> (rule2 % int3)) ((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple9
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Gary is not smart.
("Gary" "is" "smart" "-")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((triple7) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((triple9) -> (rule2 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((triple7 ((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple9) -> (rule2 % int4)) ((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4