Anne is young. Fiona is not quiet. Harry is smart. If someone is smart then they are round. If someone is kind then they are smart. Quiet people are not kind. All furry, round people are kind. If someone is quiet and not young then they are kind. Smart, round people are quiet. If someone is kind then they are quiet. If Anne is furry then Anne is not smart.
Anne is young.
("Anne" "is" "young" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are not kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "-"))
All furry, round people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and not young then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "+"))
Smart, round people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is furry then Anne is not smart.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "smart" "-"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Fiona is quiet.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "quiet" "+")
triple2
Harry is round.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "round" "+")
((triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "round" "-")
((triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not kind.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is kind.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is round.
Unknown
rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is young.[(triple1)] Fiona is not quiet.[(triple2)] Harry is smart.[(triple3)] @1: Harry is round.[(((triple3) -> rule1))] @2: Harry is quiet.[(((triple3 ((triple3) -> rule1)) -> rule6))] @3: Harry is not kind.[(((((triple3 ((triple3) -> rule1)) -> rule6)) -> rule3))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
((triple3) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not kind.
("Harry" "is" "kind" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3