Erin is big. Erin is red. Erin is rough. Erin is smart. Erin is white. Gary is green. Gary is smart. If someone is furry and smart then they are green. If someone is rough and white then they are green. If Gary is furry and Gary is big then Gary is smart. Furry people are green. All big, white people are smart. If someone is furry then they are big. All rough, furry people are green. If someone is red and rough then they are furry.
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is furry and smart then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and white then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Gary is furry and Gary is big then Gary is smart.
((("Gary" "is" "furry" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "smart" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All big, white people are smart.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All rough, furry people are green.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is red and rough then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Gary is green.
True
1
proof
[(triple6)]
("Gary" "is" "green" "+")
triple6
Erin is not smart.
False
1
inv-proof
[(triple4 OR ((triple1 triple5) -> rule5) OR ((((((triple2 triple3) -> rule8)) -> rule6) triple5) -> rule5))]
("Erin" "is" "smart" "-")
triple4
((triple1 triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple2 triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Erin is big.[(triple1 OR ((((triple2 triple3) -> rule8)) -> rule6))] Erin is red.[(triple2)] Erin is rough.[(triple3)] Erin is smart.[(triple4 OR ((triple1 triple5) -> rule5) OR ((((((triple2 triple3) -> rule8)) -> rule6) triple5) -> rule5))] Erin is white.[(triple5)] Gary is green.[(triple6)] Gary is smart.[(triple7)] @1: Erin is furry.[(((triple2 triple3) -> rule8))] Erin is green.[(((triple3 triple5) -> rule2) OR ((((triple2 triple3) -> rule8)) -> rule4) OR ((triple3 ((triple2 triple3) -> rule8)) -> rule7) OR ((((triple2 triple3) -> rule8) triple4) -> rule1) OR ((((triple2 triple3) -> rule8) ((triple1 triple5) -> rule5)) -> rule1) OR ((((triple2 triple3) -> rule8) ((((((triple2 triple3) -> rule8)) -> rule6) triple5) -> rule5)) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((((triple2 triple3) -> (rule8 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
((triple1 triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple2 triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
((triple2 triple3) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3 triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple2 triple3) -> (rule8 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple3 ((triple2 triple3) -> (rule8 % int2))) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule8 % int3)) ((triple1 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple2 triple3) -> (rule8 % int4)) ((((((triple2 triple3) -> (rule8 % int4))) -> (rule6 % int3)) triple5) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4