Bob is smart. Charlie is green. Erin is big. Fiona is smart. Rough, furry people are red. All red people are furry. If someone is furry and rough then they are green. If someone is big then they are white. Big, green people are furry. White people are furry. White people are big. Big people are white.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Rough, furry people are red.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and rough then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Big, green people are furry.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
White people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Erin is white.
True
2
proof
[(((triple3) -> rule4) OR ((triple3) -> rule8))]
("Erin" "is" "white" "+")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple3) -> rule8))]
("Erin" "is" "white" "-")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule7 <- rule8 <- FAIL)]]
("Charlie" "is" "furry" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Charlie is green.[(triple2)] Erin is big.[(triple3)] Fiona is smart.[(triple4)] @1: Erin is white.[(((triple3) -> rule4) OR ((triple3) -> rule8))] @2: Erin is furry.[(((((triple3) -> rule4)) -> rule6) OR ((((triple3) -> rule8)) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple3) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2