Bob is green. Bob is kind. Bob is white. Erin is cold. Erin is furry. Erin is green. Erin is kind. Erin is quiet. Erin is rough. Erin is not white. Fiona is green. Fiona is not kind. If Bob is furry then Bob is white. If someone is furry then they are kind. If Erin is furry then Erin is cold. Kind people are green. Green, furry people are quiet. If someone is rough and green then they are quiet. If someone is kind and not cold then they are rough. If someone is green then they are rough.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
If Bob is furry then Bob is white.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "white" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Erin is furry then Erin is cold.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "cold" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Green, furry people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and green then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not cold then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Erin is quiet.
True
1
proof
[(triple8 OR ((triple6 triple5) -> rule5) OR ((triple9 triple6) -> rule6) OR ((triple9 ((triple7) -> rule4)) -> rule6) OR ((((triple6) -> rule8) triple6) -> rule6) OR ((((triple7) -> rule4) triple5) -> rule5) OR ((((triple6) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((triple9 ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((triple5) -> rule2)) -> rule4) triple5) -> rule5) OR ((((((triple7) -> rule4)) -> rule8) triple6) -> rule6) OR ((((triple6) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((triple7) -> rule4)) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((((((triple7) -> rule4)) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) triple6) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "+")
triple8
((triple6 triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple7) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple9 ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple7) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((triple6) -> (rule8 % int4)) ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple7) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple5) -> (rule2 % int2))) -> (rule4 % int4))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is not green.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "green" "-")
triple11
Fiona is rough.
True
2
proof
[(((triple11) -> rule8))]
("Fiona" "is" "rough" "+")
((triple11) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule8) OR ((((triple2) -> rule4)) -> rule8))]
("Bob" "is" "rough" "-")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule6) OR ((((triple1) -> rule8) ((triple2) -> rule4)) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) ((triple2) -> rule4)) -> rule6))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule8 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not quiet.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule6) OR ((((triple1) -> rule8) ((triple2) -> rule4)) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) ((triple2) -> rule4)) -> rule6))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule8 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1 OR ((triple2) -> rule4))] Bob is kind.[(triple2)] Bob is white.[(triple3)] Erin is cold.[(triple4 OR ((triple5) -> rule3))] Erin is furry.[(triple5)] Erin is green.[(triple6 OR ((triple7) -> rule4) OR ((((triple5) -> rule2)) -> rule4))] Erin is kind.[(triple7 OR ((triple5) -> rule2))] Erin is not white.[(triple10)] Erin is quiet.[(triple8 OR ((triple6 triple5) -> rule5) OR ((triple9 triple6) -> rule6) OR ((triple9 ((triple7) -> rule4)) -> rule6) OR ((((triple6) -> rule8) triple6) -> rule6) OR ((((triple7) -> rule4) triple5) -> rule5) OR ((((triple6) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((triple9 ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((triple5) -> rule2)) -> rule4) triple5) -> rule5) OR ((((((triple7) -> rule4)) -> rule8) triple6) -> rule6) OR ((((triple6) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((triple7) -> rule4)) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((((((triple7) -> rule4)) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) triple6) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) ((triple7) -> rule4)) -> rule6) OR ((((((((triple5) -> rule2)) -> rule4)) -> rule8) ((((triple5) -> rule2)) -> rule4)) -> rule6))] Erin is rough.[(triple9 OR ((triple6) -> rule8) OR ((((triple7) -> rule4)) -> rule8) OR ((((((triple5) -> rule2)) -> rule4)) -> rule8))] Fiona is green.[(triple11)] Fiona is not kind.[(triple12)] @1: Bob is rough.[(((triple1) -> rule8) OR ((((triple2) -> rule4)) -> rule8))] Fiona is rough.[(((triple11) -> rule8))] @2: Bob is quiet.[(((((triple1) -> rule8) triple1) -> rule6) OR ((((triple1) -> rule8) ((triple2) -> rule4)) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule4)) -> rule8) ((triple2) -> rule4)) -> rule6))] Fiona is quiet.[(((((triple11) -> rule8) triple11) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
((triple7) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple7
((triple5) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not white.
("Erin" "is" "white" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
((triple6 triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple9 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple7) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple9 ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple7) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((triple6) -> (rule8 % int4)) ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple7) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple7) -> (rule4 % int4))) -> (rule8 % int3)) ((((triple5) -> (rule2 % int2))) -> (rule4 % int4))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((triple7) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple6) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple11) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1) -> (rule8 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple11) -> (rule8 % int2)) triple11) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2