Anne is cold. Dave is rough. Gary is cold. If someone is nice then they are furry. If someone is blue then they are nice. If someone is big and cold then they are kind. If Dave is nice and Dave is blue then Dave is rough. All blue, furry people are kind. Rough people are nice. Cold, furry people are blue. All cold people are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and cold then they are kind.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Dave is nice and Dave is blue then Dave is rough.
((("Dave" "is" "nice" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "rough" "+"))
All blue, furry people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Cold, furry people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is blue.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule8)) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Anne is furry.
True
4
proof
[(((((((triple1) -> rule8)) -> rule2)) -> rule1))]
("Anne" "is" "furry" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule2)) -> rule1))]
("Gary" "is" "furry" "-")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "blue" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Dave is rough.[(triple2)] Gary is cold.[(triple3)] @1: Anne is blue.[(((triple1) -> rule8))] Dave is nice.[(((triple2) -> rule6))] Gary is blue.[(((triple3) -> rule8))] @2: Anne is nice.[(((((triple1) -> rule8)) -> rule2))] Dave is furry.[(((((triple2) -> rule6)) -> rule1))] Gary is nice.[(((((triple3) -> rule8)) -> rule2))] @3: Anne is furry.[(((((((triple1) -> rule8)) -> rule2)) -> rule1))] Gary is furry.[(((((((triple3) -> rule8)) -> rule2)) -> rule1))] @4: Anne is kind.[(((((triple1) -> rule8) ((((((triple1) -> rule8)) -> rule2)) -> rule1)) -> rule5))] Gary is kind.[(((((triple3) -> rule8) ((((((triple3) -> rule8)) -> rule2)) -> rule1)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule8 % int4)) ((((((triple1) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule8 % int4)) ((((((triple3) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4