Anne is red. Bob is smart. Erin is quiet. Fiona is blue. All round people are young. If someone is red and furry then they are quiet. Quiet people are furry. If someone is furry and red then they are quiet. If Anne is furry then Anne is quiet. Furry people are round. Blue, round people are young. Round people are smart.
Anne is red.
("Anne" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is red and furry then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and red then they are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is furry then Anne is quiet.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "quiet" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Blue, round people are young.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Erin is furry.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "furry" "-")
((triple3) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "round" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule1))]
("Erin" "is" "young" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not smart.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule8))]
("Erin" "is" "smart" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not quiet.
Unknown
inv-rconc
[@3: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is red.[(triple1)] Bob is smart.[(triple2)] Erin is quiet.[(triple3)] Fiona is blue.[(triple4)] @1: Erin is furry.[(((triple3) -> rule3))] @2: Erin is round.[(((((triple3) -> rule3)) -> rule6))] @3: Erin is smart.[(((((((triple3) -> rule3)) -> rule6)) -> rule8))] Erin is young.[(((((((triple3) -> rule3)) -> rule6)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3