Anne is cold. Anne is furry. Anne is quiet. Anne is round. Erin is cold. Erin is quiet. Erin is red. Erin is round. Harry is cold. Harry is kind. Harry is quiet. Harry is red. If someone is quiet then they are round. All cold people are round. All kind, red people are quiet. Big, quiet people are round. If someone is red then they are big. If Harry is round then Harry is furry. All kind people are big. If Erin is furry then Erin is quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All kind, red people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Big, quiet people are round.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Harry is round then Harry is furry.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "furry" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Erin is furry then Erin is quiet.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "quiet" "+"))
Erin is round.
True
1
proof
[(triple8 OR ((triple5) -> rule2) OR ((triple6) -> rule1) OR ((((triple7) -> rule5) triple6) -> rule4))]
("Erin" "is" "round" "+")
triple8
((triple5) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Harry is big.
True
2
proof
[(((triple10) -> rule7) OR ((triple12) -> rule5))]
("Harry" "is" "big" "+")
((triple10) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple12) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple10) -> rule7) OR ((triple12) -> rule5))]
("Harry" "is" "big" "-")
((triple10) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple12) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (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 red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is quiet.[(triple3)] Anne is round.[(triple4 OR ((triple1) -> rule2) OR ((triple3) -> rule1))] Erin is cold.[(triple5)] Erin is quiet.[(triple6)] Erin is red.[(triple7)] Erin is round.[(triple8 OR ((triple5) -> rule2) OR ((triple6) -> rule1) OR ((((triple7) -> rule5) triple6) -> rule4))] Harry is cold.[(triple9)] Harry is kind.[(triple10)] Harry is quiet.[(triple11 OR ((triple10 triple12) -> rule3))] Harry is red.[(triple12)] @1: Erin is big.[(((triple7) -> rule5))] Harry is big.[(((triple10) -> rule7) OR ((triple12) -> rule5))] Harry is round.[(((triple11) -> rule1) OR ((triple9) -> rule2) OR ((((triple10 triple12) -> rule3)) -> rule1) OR ((((triple10) -> rule7) triple11) -> rule4) OR ((((triple12) -> rule5) triple11) -> rule4) OR ((((triple10) -> rule7) ((triple10 triple12) -> rule3)) -> rule4) OR ((((triple12) -> rule5) ((triple10 triple12) -> rule3)) -> rule4))] @2: Harry is furry.[(((((triple11) -> rule1)) -> rule6) OR ((((triple9) -> rule2)) -> rule6) OR ((((((triple10 triple12) -> rule3)) -> rule1)) -> rule6) OR ((((((triple10) -> rule7) triple11) -> rule4)) -> rule6) OR ((((((triple12) -> rule5) triple11) -> rule4)) -> rule6) OR ((((((triple10) -> rule7) ((triple10 triple12) -> rule3)) -> rule4)) -> rule6) OR ((((((triple12) -> rule5) ((triple10 triple12) -> rule3)) -> rule4)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple5) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple10 triple12) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple12
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple12) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple9) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10 triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple10) -> (rule7 % int2)) triple11) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple12) -> (rule5 % int2)) triple11) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple10) -> (rule7 % int3)) ((triple10 triple12) -> (rule3 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple12) -> (rule5 % int3)) ((triple10 triple12) -> (rule3 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple10 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple10) -> (rule7 % int3)) triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple12) -> (rule5 % int3)) triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple10) -> (rule7 % int4)) ((triple10 triple12) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((((triple12) -> (rule5 % int4)) ((triple10 triple12) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4