Anne is big. Anne is cold. Anne is furry. Anne is quiet. Anne is red. Anne is smart. Anne is white. Erin is furry. Erin is red. Erin is smart. Erin is white. Fiona is big. Fiona is cold. Fiona is furry. Fiona is red. Harry is smart. If Erin is red then Erin is cold. Red, white people are big. If someone is smart and furry then they are red. All furry people are smart. If Harry is smart then Harry is furry. If someone is red then they are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Erin is red then Erin is cold.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "cold" "+"))
Red, white people are big.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is smart and furry then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart then Harry is furry.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "furry" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Erin is smart.
True
1
proof
[(triple10 OR ((triple8) -> rule4))]
("Erin" "is" "smart" "+")
triple10
((triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule6) OR ((triple5 triple7) -> rule2) OR ((((triple6 triple3) -> rule3)) -> rule6) OR ((((triple6 triple3) -> rule3) triple7) -> rule2) OR ((((((triple3) -> rule4) triple3) -> rule3)) -> rule6) OR ((((((triple3) -> rule4) triple3) -> rule3) triple7) -> rule2))]
("Anne" "is" "big" "-")
triple1
((triple5) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple5 triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple6 triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple6 triple3) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is smart.
True
2
proof
[(((triple14) -> rule4))]
("Fiona" "is" "smart" "+")
((triple14) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple9) -> rule6) OR ((triple9 triple11) -> rule2) OR ((((triple10 triple8) -> rule3)) -> rule6) OR ((((triple10 triple8) -> rule3) triple11) -> rule2) OR ((((((triple8) -> rule4) triple8) -> rule3)) -> rule6) OR ((((((triple8) -> rule4) triple8) -> rule3) triple11) -> rule2))]
("Erin" "is" "big" "-")
((triple9) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple10 triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple10 triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple8) -> (rule4 % int3)) triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple8) -> (rule4 % int3)) triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Harry is red.
True
4
proof
[(((triple16 ((triple16) -> rule5)) -> rule3))]
("Harry" "is" "red" "+")
((triple16 ((triple16) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple16 ((triple16) -> rule5)) -> rule3))]
("Harry" "is" "red" "-")
((triple16 ((triple16) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
True
5
proof
[(((((triple16 ((triple16) -> rule5)) -> rule3)) -> rule6))]
("Harry" "is" "big" "+")
((((triple16 ((triple16) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not big.
False
5
inv-proof
[(((((triple16 ((triple16) -> rule5)) -> rule3)) -> rule6))]
("Harry" "is" "big" "-")
((((triple16 ((triple16) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is big.[(triple1 OR ((triple5) -> rule6) OR ((triple5 triple7) -> rule2) OR ((((triple6 triple3) -> rule3)) -> rule6) OR ((((triple6 triple3) -> rule3) triple7) -> rule2) OR ((((((triple3) -> rule4) triple3) -> rule3)) -> rule6) OR ((((((triple3) -> rule4) triple3) -> rule3) triple7) -> rule2))] Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is quiet.[(triple4)] Anne is red.[(triple5 OR ((triple6 triple3) -> rule3) OR ((((triple3) -> rule4) triple3) -> rule3))] Anne is smart.[(triple6 OR ((triple3) -> rule4))] Anne is white.[(triple7)] Erin is furry.[(triple8)] Erin is red.[(triple9 OR ((triple10 triple8) -> rule3) OR ((((triple8) -> rule4) triple8) -> rule3))] Erin is smart.[(triple10 OR ((triple8) -> rule4))] Erin is white.[(triple11)] Fiona is big.[(triple12 OR ((triple15) -> rule6) OR ((((((triple14) -> rule4) triple14) -> rule3)) -> rule6))] Fiona is cold.[(triple13)] Fiona is furry.[(triple14)] Fiona is red.[(triple15 OR ((((triple14) -> rule4) triple14) -> rule3))] Harry is smart.[(triple16)] @1: Erin is big.[(((triple9) -> rule6) OR ((triple9 triple11) -> rule2) OR ((((triple10 triple8) -> rule3)) -> rule6) OR ((((triple10 triple8) -> rule3) triple11) -> rule2) OR ((((((triple8) -> rule4) triple8) -> rule3)) -> rule6) OR ((((((triple8) -> rule4) triple8) -> rule3) triple11) -> rule2))] Erin is cold.[(((triple9) -> rule1) OR ((((triple10 triple8) -> rule3)) -> rule1) OR ((((((triple8) -> rule4) triple8) -> rule3)) -> rule1))] Fiona is smart.[(((triple14) -> rule4))] Harry is furry.[(((triple16) -> rule5))] @2: Harry is red.[(((triple16 ((triple16) -> rule5)) -> rule3))] @3: Harry is big.[(((((triple16 ((triple16) -> rule5)) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple5) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple5 triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple6 triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple6 triple3) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple7) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple6 triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
((triple10 triple8) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple8) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple10
((triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple11
Fiona is big.
("Fiona" "is" "big" "+")
triple12
((triple15) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((((triple14) -> (rule4 % int3)) triple14) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple13
Fiona is furry.
("Fiona" "is" "furry" "+")
triple14
Fiona is red.
("Fiona" "is" "red" "+")
triple15
((((triple14) -> (rule4 % int2)) triple14) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Erin is big.
("Erin" "is" "big" "+")
((triple9) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple10 triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple10 triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple8) -> (rule4 % int3)) triple8) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple8) -> (rule4 % int3)) triple8) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple9) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple8) -> (rule4 % int3)) triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple14) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple16) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple16 ((triple16) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple16 ((triple16) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3