Erin is white. Fiona is rough. Gary is furry. Harry is blue. If something is white and furry then it is cold. White things are cold. If something is white then it is smart. All blue, furry things are nice. White, rough things are cold. If something is nice then it is smart. Nice, blue things are furry. If something is furry then it is blue.
Erin is white.
("Erin" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is white and furry then it is cold.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All blue, furry things are nice.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
White, rough things are cold.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Nice, blue things are furry.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Fiona is rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "rough" "-")
triple2
Erin is cold.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is nice.
True
4
proof
[(((((triple3) -> rule8) triple3) -> rule4))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((((triple3) -> rule8) triple3) -> rule4))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
True
5
proof
[(((((((triple3) -> rule8) triple3) -> rule4)) -> rule6))]
("Gary" "is" "smart" "+")
((((((triple3) -> (rule8 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not smart.
False
5
inv-proof
[(((((((triple3) -> rule8) triple3) -> rule4)) -> rule6))]
("Gary" "is" "smart" "-")
((((((triple3) -> (rule8 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule7 <- FAIL)]]
("Fiona" "is" "smart" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Harry" "is" "nice" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Erin is white.[(triple1)] Fiona is rough.[(triple2)] Gary is furry.[(triple3)] Harry is blue.[(triple4)] @1: Erin is cold.[(((triple1) -> rule2))] Erin is smart.[(((triple1) -> rule3))] Gary is blue.[(((triple3) -> rule8))] @2: Gary is nice.[(((((triple3) -> rule8) triple3) -> rule4))] @3: Gary is smart.[(((((((triple3) -> rule8) triple3) -> rule4)) -> rule6))]
Erin is white.
("Erin" "is" "white" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule8 % int2)) triple3) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple3) -> (rule8 % int3)) triple3) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3