Anne is kind. Erin is not furry. Fiona is not rough. Fiona is round. Fiona is smart. Harry is quiet. Harry is round. All quiet, kind things are furry. If something is kind and not rough then it is furry. If Erin is quiet and Erin is not rough then Erin is kind. Quiet, big things are kind. All quiet things are big. If something is smart then it is big. If Erin is smart then Erin is furry. Rough, quiet things are smart.
Anne is kind.
("Anne" "is" "kind" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
All quiet, kind things are furry.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If something is kind and not rough then it is furry.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "furry" "+"))
If Erin is quiet and Erin is not rough then Erin is kind.
((("Erin" "is" "quiet" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "kind" "+"))
Quiet, big things are kind.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If Erin is smart then Erin is furry.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "furry" "+"))
Rough, quiet things are smart.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Erin is furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Harry is big.
True
2
proof
[(((triple6) -> rule5))]
("Harry" "is" "big" "+")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule5))]
("Harry" "is" "big" "-")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
True
4
proof
[(((triple6 ((triple6) -> rule5)) -> rule4))]
("Harry" "is" "kind" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((triple6 ((triple6) -> rule5)) -> rule4))]
("Harry" "is" "kind" "-")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
True
6
proof
[(((triple6 ((triple6 ((triple6) -> rule5)) -> rule4)) -> rule1))]
("Harry" "is" "furry" "+")
((triple6 ((triple6 ((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not furry.
False
6
inv-proof
[(((triple6 ((triple6 ((triple6) -> rule5)) -> rule4)) -> rule1))]
("Harry" "is" "furry" "-")
((triple6 ((triple6 ((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "smart" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "kind" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "smart" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is kind.[(triple1)] Erin is not furry.[(triple2)] Fiona is not rough.[(triple3)] Fiona is round.[(triple4)] Fiona is smart.[(triple5)] Harry is quiet.[(triple6)] Harry is round.[(triple7)] @1: Fiona is big.[(((triple5) -> rule6))] Harry is big.[(((triple6) -> rule5))] @2: Harry is kind.[(((triple6 ((triple6) -> rule5)) -> rule4))] @3: Harry is furry.[(((triple6 ((triple6 ((triple6) -> rule5)) -> rule4)) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Erin is not furry.
("Erin" "is" "furry" "-")
triple2
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
((triple5) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple6 ((triple6 ((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3