Anne is cold. Anne is smart. Harry is cold. Harry is furry. Harry is nice. Harry is rough. Harry is smart. Quiet people are smart. All quiet, kind people are rough. All kind, cold people are quiet. Kind, cold people are furry. All cold people are furry. Furry people are quiet. If Anne is kind and Anne is furry then Anne is nice. Kind, quiet people are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All quiet, kind people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All kind, cold people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Kind, cold people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is kind and Anne is furry then Anne is nice.
((("Anne" "is" "kind" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "nice" "+"))
Kind, quiet people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Harry is furry.
True
1
proof
[(triple4 OR ((triple3) -> rule5))]
("Harry" "is" "furry" "+")
triple4
((triple3) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple5)]
("Harry" "is" "nice" "-")
triple5
Harry is quiet.
True
2
proof
[(((triple4) -> rule6) OR ((((triple3) -> rule5)) -> rule6))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "furry" "-")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is smart.[(triple2 OR ((((((triple1) -> rule5)) -> rule6)) -> rule1))] Harry is cold.[(triple3)] Harry is furry.[(triple4 OR ((triple3) -> rule5))] Harry is nice.[(triple5)] Harry is rough.[(triple6)] Harry is smart.[(triple7 OR ((((triple4) -> rule6)) -> rule1) OR ((((((triple3) -> rule5)) -> rule6)) -> rule1))] @1: Anne is furry.[(((triple1) -> rule5))] Harry is quiet.[(((triple4) -> rule6) OR ((((triple3) -> rule5)) -> rule6))] @2: Anne is quiet.[(((((triple1) -> rule5)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((triple3) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2