Anne is cold. Anne is furry. Anne is not kind. Anne is quiet. Anne is round. Anne is smart. Gary is furry. Gary is kind. Gary is round. Harry is not big. Harry is kind. Harry is not quiet. All cold, big things are smart. If something is round then it is smart. If Anne is kind then Anne is smart. All furry, big things are quiet. If Harry is not cold then Harry is big. All kind things are furry. Furry things are round. If Harry is quiet then Harry is furry.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
All cold, big things are smart.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Anne is kind then Anne is smart.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "smart" "+"))
All furry, big things are quiet.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Harry is not cold then Harry is big.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "big" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Harry is quiet then Harry is furry.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple4)]
("Anne" "is" "quiet" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple11)]
("Harry" "is" "kind" "-")
triple11
Gary is smart.
True
2
proof
[(((triple9) -> rule2) OR ((((triple7) -> rule7)) -> rule2) OR ((((((triple8) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not smart.
False
2
inv-proof
[(((triple9) -> rule2) OR ((((triple7) -> rule7)) -> rule2) OR ((((((triple8) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "smart" "-")
((triple9) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Harry is round.
True
3
proof
[(((((triple11) -> rule6)) -> rule7))]
("Harry" "is" "round" "+")
((((triple11) -> (rule6 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule7))]
("Harry" "is" "round" "-")
((((triple11) -> (rule6 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple11) -> rule6)) -> rule7)) -> rule2))]
("Harry" "is" "smart" "+")
((((((triple11) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple11) -> rule6)) -> rule7)) -> rule2))]
("Harry" "is" "smart" "-")
((((((triple11) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is not kind.[(triple3)] Anne is quiet.[(triple4)] Anne is round.[(triple5 OR ((triple2) -> rule7))] Anne is smart.[(triple6 OR ((triple5) -> rule2) OR ((((triple2) -> rule7)) -> rule2))] Gary is furry.[(triple7 OR ((triple8) -> rule6))] Gary is kind.[(triple8)] Gary is round.[(triple9 OR ((triple7) -> rule7) OR ((((triple8) -> rule6)) -> rule7))] Harry is kind.[(triple11)] Harry is not big.[(triple10)] Harry is not quiet.[(triple12)] @1: Gary is smart.[(((triple9) -> rule2) OR ((((triple7) -> rule7)) -> rule2) OR ((((((triple8) -> rule6)) -> rule7)) -> rule2))] Harry is furry.[(((triple11) -> rule6))] @2: Harry is round.[(((((triple11) -> rule6)) -> rule7))] @3: Harry is smart.[(((((((triple11) -> rule6)) -> rule7)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is not kind.
("Anne" "is" "kind" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple2) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple5) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((triple8) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
((triple7) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is not big.
("Harry" "is" "big" "-")
triple10
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((triple11) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple11) -> (rule6 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple11) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3