Anne is not furry. Anne is not kind. Anne is quiet. Charlie is big. Charlie is blue. Charlie is furry. Charlie is kind. Charlie is quiet. Charlie is not rough. Charlie is smart. Erin is furry. Erin is quiet. Fiona is kind. Fiona is not quiet. Fiona is smart. Quiet, smart things are big. All furry things are big. If something is big then it is not rough. Big, smart things are not rough. If Erin is kind and Erin is quiet then Erin is not rough. All rough things are not furry. Furry, quiet things are smart. If something is rough and not blue then it is kind.
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Quiet, smart things are big.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big then it is not rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
Big, smart things are not rough.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "-"))
If Erin is kind and Erin is quiet then Erin is not rough.
((("Erin" "is" "kind" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "rough" "-"))
All rough things are not furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "-"))
Furry, quiet things are smart.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is rough and not blue then it is kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
Anne is not furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "blue" "-")
triple5
Erin is big.
True
2
proof
[(((triple11) -> rule2) OR ((triple12 ((triple11 triple12) -> rule7)) -> rule1))]
("Erin" "is" "big" "+")
((triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple12 ((triple11 triple12) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not big.
False
2
inv-proof
[(((triple11) -> rule2) OR ((triple12 ((triple11 triple12) -> rule7)) -> rule1))]
("Erin" "is" "big" "-")
((triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple12 ((triple11 triple12) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not rough.
True
3
proof
[(((((triple11) -> rule2)) -> rule3) OR ((((triple11) -> rule2) ((triple11 triple12) -> rule7)) -> rule4) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1)) -> rule3) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1) ((triple11 triple12) -> rule7)) -> rule4))]
("Erin" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple11 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2)) ((triple11 triple12) -> (rule7 % int3))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule3) OR ((((triple11) -> rule2) ((triple11 triple12) -> rule7)) -> rule4) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1)) -> rule3) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1) ((triple11 triple12) -> rule7)) -> rule4))]
("Erin" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple11 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2)) ((triple11 triple12) -> (rule7 % int3))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "smart" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is not furry.[(triple1)] Anne is not kind.[(triple2)] Anne is quiet.[(triple3)] Charlie is big.[(triple4 OR ((triple6) -> rule2) OR ((triple8 triple10) -> rule1) OR ((triple8 ((triple6 triple8) -> rule7)) -> rule1))] Charlie is blue.[(triple5)] Charlie is furry.[(triple6)] Charlie is kind.[(triple7)] Charlie is not rough.[(triple9 OR ((triple4) -> rule3) OR ((triple4 triple10) -> rule4) OR ((((triple6) -> rule2)) -> rule3) OR ((((triple8 triple10) -> rule1)) -> rule3) OR ((triple4 ((triple6 triple8) -> rule7)) -> rule4) OR ((((triple6) -> rule2) triple10) -> rule4) OR ((((triple8 triple10) -> rule1) triple10) -> rule4) OR ((((triple6) -> rule2) ((triple6 triple8) -> rule7)) -> rule4) OR ((((triple8 triple10) -> rule1) ((triple6 triple8) -> rule7)) -> rule4) OR ((((triple8 ((triple6 triple8) -> rule7)) -> rule1)) -> rule3) OR ((((triple8 ((triple6 triple8) -> rule7)) -> rule1) triple10) -> rule4) OR ((((triple8 ((triple6 triple8) -> rule7)) -> rule1) ((triple6 triple8) -> rule7)) -> rule4))] Charlie is quiet.[(triple8)] Charlie is smart.[(triple10 OR ((triple6 triple8) -> rule7))] Erin is furry.[(triple11)] Erin is quiet.[(triple12)] Fiona is kind.[(triple13)] Fiona is not quiet.[(triple14)] Fiona is smart.[(triple15)] @1: Erin is big.[(((triple11) -> rule2) OR ((triple12 ((triple11 triple12) -> rule7)) -> rule1))] Erin is smart.[(((triple11 triple12) -> rule7))] @2: Erin is not rough.[(((((triple11) -> rule2)) -> rule3) OR ((((triple11) -> rule2) ((triple11 triple12) -> rule7)) -> rule4) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1)) -> rule3) OR ((((triple12 ((triple11 triple12) -> rule7)) -> rule1) ((triple11 triple12) -> rule7)) -> rule4))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Anne is not kind.
("Anne" "is" "kind" "-")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple6) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple8 triple10) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple8 ((triple6 triple8) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple9
((triple4) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((triple4 triple10) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple8 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple4 ((triple6 triple8) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple6) -> (rule2 % int2)) triple10) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple8 triple10) -> (rule1 % int2)) triple10) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple6 triple8) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple8 triple10) -> (rule1 % int3)) ((triple6 triple8) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple8 ((triple6 triple8) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((triple8 ((triple6 triple8) -> (rule7 % int3))) -> (rule1 % int2)) triple10) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((triple8 ((triple6 triple8) -> (rule7 % int3))) -> (rule1 % int2)) ((triple6 triple8) -> (rule7 % int3))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
((triple6 triple8) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple11
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
Fiona is kind.
("Fiona" "is" "kind" "+")
triple13
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Erin is big.
("Erin" "is" "big" "+")
((triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple12 ((triple11 triple12) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple11 triple12) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple11 triple12) -> (rule7 % int2))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple12 ((triple11 triple12) -> (rule7 % int3))) -> (rule1 % int2)) ((triple11 triple12) -> (rule7 % int3))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3