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