Anne is furry. Anne is smart. Anne is young. Erin is kind. Erin is quiet. Fiona is cold. Fiona is kind. All smart, cold things are young. Furry, green things are young. Quiet, young things are cold. If something is kind and furry then it is smart. If something is furry then it is kind. Smart, young things are furry. Furry, smart things are quiet. Kind things are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
All smart, cold things are young.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Furry, green things are young.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Quiet, young things are cold.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is kind and furry then it is smart.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Smart, young things are furry.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Furry, smart things are quiet.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Anne is smart.
True
1
proof
[(triple2 OR ((((triple1) -> rule5) triple1) -> rule4))]
("Anne" "is" "smart" "+")
triple2
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is not quiet.
False
1
inv-proof
[(triple5 OR ((((triple4) -> rule8) ((triple4 ((triple4) -> rule8)) -> rule4)) -> rule7))]
("Erin" "is" "quiet" "-")
triple5
((((triple4) -> (rule8 % int3)) ((triple4 ((triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Anne is kind.
True
2
proof
[(((triple1) -> rule5) OR ((((triple2 triple3) -> rule6)) -> rule5))]
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is not furry.
False
2
inv-proof
[(((triple4) -> rule8))]
("Erin" "is" "furry" "-")
((triple4) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is young.
Unknown
rconc
[@3: Erin is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is furry.[(triple1 OR ((triple2 triple3) -> rule6))] Anne is smart.[(triple2 OR ((((triple1) -> rule5) triple1) -> rule4))] Anne is young.[(triple3)] Erin is kind.[(triple4)] Erin is quiet.[(triple5 OR ((((triple4) -> rule8) ((triple4 ((triple4) -> rule8)) -> rule4)) -> rule7))] Fiona is cold.[(triple6)] Fiona is kind.[(triple7)] @1: Anne is kind.[(((triple1) -> rule5) OR ((((triple2 triple3) -> rule6)) -> rule5))] Anne is quiet.[(((triple1 triple2) -> rule7) OR ((((triple2 triple3) -> rule6) triple2) -> rule7) OR ((triple1 ((((triple1) -> rule5) triple1) -> rule4)) -> rule7) OR ((((triple2 triple3) -> rule6) ((((triple1) -> rule5) triple1) -> rule4)) -> rule7))] Erin is furry.[(((triple4) -> rule8))] Fiona is furry.[(((triple7) -> rule8))] @2: Anne is cold.[(((((triple1 triple2) -> rule7) triple3) -> rule3) OR ((((((triple2 triple3) -> rule6) triple2) -> rule7) triple3) -> rule3) OR ((((triple1 ((((triple1) -> rule5) triple1) -> rule4)) -> rule7) triple3) -> rule3) OR ((((((triple2 triple3) -> rule6) ((((triple1) -> rule5) triple1) -> rule4)) -> rule7) triple3) -> rule3))] Erin is smart.[(((triple4 ((triple4) -> rule8)) -> rule4))] Fiona is smart.[(((triple7 ((triple7) -> rule8)) -> rule4))] @3: Fiona is quiet.[(((((triple7) -> rule8) ((triple7 ((triple7) -> rule8)) -> rule4)) -> rule7))] Fiona is young.[(((((triple7 ((triple7) -> rule8)) -> rule4) triple6) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2 triple3) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((((triple4) -> (rule8 % int3)) ((triple4 ((triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 triple2) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple2 triple3) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple1 ((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((triple2 triple3) -> (rule6 % int4)) ((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple7) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1 triple2) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple2 triple3) -> (rule6 % int3)) triple2) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((triple1 ((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
((((((triple2 triple3) -> (rule6 % int5)) ((((triple1) -> (rule5 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Erin is smart.
("Erin" "is" "smart" "+")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7 ((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple7) -> (rule8 % int3)) ((triple7 ((triple7) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((((triple7 ((triple7) -> (rule8 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3