Erin is furry. Erin is green. Erin is rough. Erin is smart. Fiona is green. Fiona is quiet. Fiona is white. Smart things are furry. Green things are furry. All smart things are green. All green, furry things are smart. If Erin is furry then Erin is green. If Erin is furry then Erin is rough. If Fiona is white then Fiona is smart. If something is white and not green then it is not quiet.
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green, furry things are smart.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Erin is furry then Erin is green.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "green" "+"))
If Erin is furry then Erin is rough.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "rough" "+"))
If Fiona is white then Fiona is smart.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "smart" "+"))
If something is white and not green then it is not quiet.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "quiet" "-"))
Erin is rough.
True
1
proof
[(triple3 OR ((triple1) -> rule6) OR ((((triple2) -> rule2)) -> rule6) OR ((((triple4) -> rule1)) -> rule6) OR ((((((triple4) -> rule3)) -> rule2)) -> rule6))]
("Erin" "is" "rough" "+")
triple3
((triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not green.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule5) OR ((triple4) -> rule3) OR ((((triple4) -> rule1)) -> rule5))]
("Erin" "is" "green" "-")
triple2
((triple1) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Fiona is smart.
True
2
proof
[(((triple7) -> rule7) OR ((triple5 ((triple5) -> rule2)) -> rule4))]
("Fiona" "is" "smart" "+")
((triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not furry.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple7) -> rule7)) -> rule1) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2))]
("Fiona" "is" "furry" "-")
((triple5) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Erin is furry.[(triple1 OR ((triple2) -> rule2) OR ((triple4) -> rule1) OR ((((triple4) -> rule3)) -> rule2))] Erin is green.[(triple2 OR ((triple1) -> rule5) OR ((triple4) -> rule3) OR ((((triple4) -> rule1)) -> rule5))] Erin is rough.[(triple3 OR ((triple1) -> rule6) OR ((((triple2) -> rule2)) -> rule6) OR ((((triple4) -> rule1)) -> rule6) OR ((((((triple4) -> rule3)) -> rule2)) -> rule6))] Erin is smart.[(triple4 OR ((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule2)) -> rule4) OR ((((triple1) -> rule5) triple1) -> rule4) OR ((((triple1) -> rule5) ((triple2) -> rule2)) -> rule4))] Fiona is green.[(triple5 OR ((((triple7) -> rule7)) -> rule3))] Fiona is quiet.[(triple6)] Fiona is white.[(triple7)] @1: Fiona is furry.[(((triple5) -> rule2) OR ((((triple7) -> rule7)) -> rule1) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2))] Fiona is smart.[(((triple7) -> rule7) OR ((triple5 ((triple5) -> rule2)) -> rule4))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple4) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
((triple1) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
((triple2 triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple5
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple5) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2