Anne is furry. Erin is not round. Harry is green. If someone is kind and cold then they are big. Furry, quiet people are big. All green people are big. If someone is big and quiet then they are not furry. Round people are kind. If someone is cold then they are kind. If someone is big and not round then they are cold. Big, green people are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Erin is not round.
("Erin" "is" "round" "-")
Harry is green.
("Harry" "is" "green" "+")
If someone is kind and cold then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Furry, quiet people are big.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is big and quiet then they are not furry.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "-"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and not round then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "+"))
Big, green people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Erin is not round.
True
1
proof
[(triple2)]
("Erin" "is" "round" "-")
triple2
Erin is round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Harry is big.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "big" "+")
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "big" "-")
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule8))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule8))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not furry.
True
7
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3) triple3) -> rule8)) -> rule4))]
("Harry" "is" "furry" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is furry.
False
7
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3) triple3) -> rule8)) -> rule4))]
("Harry" "is" "furry" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Harry" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Anne" "is" "kind" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is furry.[(triple1)] Erin is not round.[(triple2)] Harry is green.[(triple3)] @1: Harry is big.[(((triple3) -> rule3))] @2: Harry is quiet.[(((((triple3) -> rule3) triple3) -> rule8))] @3: Harry is not furry.[(((((triple3) -> rule3) ((((triple3) -> rule3) triple3) -> rule8)) -> rule4))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Erin is not round.
("Erin" "is" "round" "-")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3