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