Anne is nice. Anne is young. Bob is furry. Bob is quiet. Erin is furry. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Erin is smart. Erin is young. Fiona is furry. Fiona is kind. Fiona is quiet. Fiona is rough. Fiona is smart. Kind, nice people are quiet. Quiet, furry people are rough. If someone is kind then they are nice. Rough, furry people are young. All rough people are furry. If Fiona is young then Fiona is smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Kind, nice people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, furry people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Rough, furry people are young.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If Fiona is young then Fiona is smart.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "smart" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple9 OR ((triple8 triple5) -> rule2) OR ((((triple6 triple7) -> rule1) triple5) -> rule2) OR ((((triple6 ((triple6) -> rule3)) -> rule1) triple5) -> rule2))]
("Erin" "is" "rough" "-")
triple9
((triple8 triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple6 ((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Fiona is young.
True
3
proof
[(((triple15 triple12) -> rule4) OR ((triple15 ((triple15) -> rule5)) -> rule4) OR ((((triple14 triple12) -> rule2) triple12) -> rule4) OR ((((triple14 triple12) -> rule2) ((triple15) -> rule5)) -> rule4) OR ((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) triple12) -> rule4) OR ((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) ((triple15) -> rule5)) -> rule4))]
("Fiona" "is" "young" "+")
((triple15 triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple15 ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple14 triple12) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple14 triple12) -> (rule2 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple13 ((triple13) -> (rule3 % int4))) -> (rule1 % int3)) triple12) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((((triple13 ((triple13) -> (rule3 % int5))) -> (rule1 % int4)) triple12) -> (rule2 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is not nice.
False
2
inv-proof
[(((triple13) -> rule3))]
("Fiona" "is" "nice" "-")
((triple13) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Bob is young.
True
5
proof
[(((((triple4 triple3) -> rule2) triple3) -> rule4))]
("Bob" "is" "young" "+")
((((triple4 triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not young.
False
5
inv-proof
[(((((triple4 triple3) -> rule2) triple3) -> rule4))]
("Bob" "is" "young" "-")
((((triple4 triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Anne is young.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4)] Erin is furry.[(triple5 OR ((triple9) -> rule5))] Erin is kind.[(triple6)] Erin is nice.[(triple7 OR ((triple6) -> rule3))] Erin is quiet.[(triple8 OR ((triple6 triple7) -> rule1) OR ((triple6 ((triple6) -> rule3)) -> rule1))] Erin is rough.[(triple9 OR ((triple8 triple5) -> rule2) OR ((((triple6 triple7) -> rule1) triple5) -> rule2) OR ((((triple6 ((triple6) -> rule3)) -> rule1) triple5) -> rule2))] Erin is smart.[(triple10)] Erin is young.[(triple11 OR ((triple9 triple5) -> rule4) OR ((triple9 ((triple9) -> rule5)) -> rule4) OR ((((triple8 triple5) -> rule2) triple5) -> rule4) OR ((((triple8 triple5) -> rule2) ((triple9) -> rule5)) -> rule4) OR ((((((triple6 triple7) -> rule1) triple5) -> rule2) triple5) -> rule4) OR ((((((triple6 triple7) -> rule1) triple5) -> rule2) ((triple9) -> rule5)) -> rule4) OR ((((((triple6 ((triple6) -> rule3)) -> rule1) triple5) -> rule2) triple5) -> rule4) OR ((((((triple6 ((triple6) -> rule3)) -> rule1) triple5) -> rule2) ((triple9) -> rule5)) -> rule4))] Fiona is furry.[(triple12 OR ((triple15) -> rule5))] Fiona is kind.[(triple13)] Fiona is quiet.[(triple14 OR ((triple13 ((triple13) -> rule3)) -> rule1))] Fiona is rough.[(triple15 OR ((triple14 triple12) -> rule2) OR ((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2))] Fiona is smart.[(triple16 OR ((((triple15 triple12) -> rule4)) -> rule6) OR ((((triple15 ((triple15) -> rule5)) -> rule4)) -> rule6) OR ((((((triple14 triple12) -> rule2) triple12) -> rule4)) -> rule6) OR ((((((triple14 triple12) -> rule2) ((triple15) -> rule5)) -> rule4)) -> rule6) OR ((((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) triple12) -> rule4)) -> rule6) OR ((((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) ((triple15) -> rule5)) -> rule4)) -> rule6))] @1: Bob is rough.[(((triple4 triple3) -> rule2))] Fiona is nice.[(((triple13) -> rule3))] Fiona is young.[(((triple15 triple12) -> rule4) OR ((triple15 ((triple15) -> rule5)) -> rule4) OR ((((triple14 triple12) -> rule2) triple12) -> rule4) OR ((((triple14 triple12) -> rule2) ((triple15) -> rule5)) -> rule4) OR ((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) triple12) -> rule4) OR ((((((triple13 ((triple13) -> rule3)) -> rule1) triple12) -> rule2) ((triple15) -> rule5)) -> rule4))] @2: Bob is young.[(((((triple4 triple3) -> rule2) triple3) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
((triple9) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
((triple6) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
((triple6 triple7) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple8 triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple6 ((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple11
((triple9 triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple8 triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple8 triple5) -> (rule2 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple6 triple7) -> (rule1 % int3)) triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple6 triple7) -> (rule1 % int4)) triple5) -> (rule2 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((triple6 ((triple6) -> (rule3 % int4))) -> (rule1 % int3)) triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((((triple6 ((triple6) -> (rule3 % int5))) -> (rule1 % int4)) triple5) -> (rule2 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
int5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple12
((triple15) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
((triple13 ((triple13) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
((triple14 triple12) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple13 ((triple13) -> (rule3 % int3))) -> (rule1 % int2)) triple12) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple16
((((triple15 triple12) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple15 ((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple14 triple12) -> (rule2 % int3)) triple12) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple14 triple12) -> (rule2 % int4)) ((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((((((triple13 ((triple13) -> (rule3 % int5))) -> (rule1 % int4)) triple12) -> (rule2 % int3)) triple12) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((((((((triple13 ((triple13) -> (rule3 % int6))) -> (rule1 % int5)) triple12) -> (rule2 % int4)) ((triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Fiona is nice.
("Fiona" "is" "nice" "+")
int6
Bob is rough.
("Bob" "is" "rough" "+")
((triple4 triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple13) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple15 triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple15 ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple14 triple12) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple14 triple12) -> (rule2 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple13 ((triple13) -> (rule3 % int4))) -> (rule1 % int3)) triple12) -> (rule2 % int2)) triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((((triple13 ((triple13) -> (rule3 % int5))) -> (rule1 % int4)) triple12) -> (rule2 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Bob is young.
("Bob" "is" "young" "+")
((((triple4 triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2