Anne is big. Erin is rough. Erin is smart. Rough people are young. All rough, round people are quiet. All smart, young people are furry. All rough, furry people are big. If someone is big then they are young. Big people are smart.
Anne is big.
("Anne" "is" "big" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All rough, round people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All smart, young people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All rough, furry people are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Erin is not rough.
False
1
inv-proof
[(triple2)]
("Erin" "is" "rough" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "young" "-")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
True
5
proof
[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule3))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is not furry.
False
4
inv-proof
[(((triple3 ((triple2) -> rule1)) -> rule3))]
("Erin" "is" "furry" "-")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
True
6
proof
[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule3)) -> rule4))]
("Erin" "is" "big" "+")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not big.
False
6
inv-proof
[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule3)) -> rule4))]
("Erin" "is" "big" "-")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is big.[(triple1)] Erin is rough.[(triple2)] Erin is smart.[(triple3)] @1: Anne is smart.[(((triple1) -> rule6))] Anne is young.[(((triple1) -> rule5))] Erin is young.[(((triple2) -> rule1))] @2: Anne is furry.[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule3))] Erin is furry.[(((triple3 ((triple2) -> rule1)) -> rule3))] @3: Erin is big.[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3