Anne is cold. Erin is red. Fiona is furry. Gary is cold. If something is green and kind then it is furry. Kind, furry things are big. If something is kind and big then it is furry. All cold things are kind. If something is red then it is cold. If Fiona is red then Fiona is rough. All kind, rough things are furry. Cold things are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is green and kind then it is furry.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Kind, furry things are big.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is kind and big then it is furry.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Fiona is red then Fiona is rough.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "rough" "+"))
All kind, rough things are furry.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Gary is cold.
True
1
proof
[(triple4)]
("Gary" "is" "cold" "+")
triple4
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Anne is kind.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("Erin" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Anne is not furry.
False
5
inv-proof
[(((((triple1) -> rule4) ((triple1) -> rule8)) -> rule7))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Erin is furry.
True
7
proof
[(((((((triple2) -> rule5)) -> rule4) ((((triple2) -> rule5)) -> rule8)) -> rule7))]
("Erin" "is" "furry" "+")
((((((triple2) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Anne is not big.
False
8
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule8)) -> rule7)) -> rule2))]
("Anne" "is" "big" "-")
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is rough.
Unknown
rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is big.
Unknown
rconc
[@3: Fiona is big.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule5 <- FAIL)]]
("Fiona" "is" "big" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is cold.[(triple1)] Erin is red.[(triple2)] Fiona is furry.[(triple3)] Gary is cold.[(triple4)] @1: Anne is kind.[(((triple1) -> rule4))] Anne is rough.[(((triple1) -> rule8))] Erin is cold.[(((triple2) -> rule5))] Gary is kind.[(((triple4) -> rule4))] Gary is rough.[(((triple4) -> rule8))] @2: Anne is furry.[(((((triple1) -> rule4) ((triple1) -> rule8)) -> rule7))] Erin is kind.[(((((triple2) -> rule5)) -> rule4))] Erin is rough.[(((((triple2) -> rule5)) -> rule8))] Gary is furry.[(((((triple4) -> rule4) ((triple4) -> rule8)) -> rule7))] @3: Anne is big.[(((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule8)) -> rule7)) -> rule2))] Erin is furry.[(((((((triple2) -> rule5)) -> rule4) ((((triple2) -> rule5)) -> rule8)) -> rule7))] Gary is big.[(((((triple4) -> rule4) ((((triple4) -> rule4) ((triple4) -> rule8)) -> rule7)) -> rule2))] @4: Erin is big.[(((((((triple2) -> rule5)) -> rule4) ((((((triple2) -> rule5)) -> rule4) ((((triple2) -> rule5)) -> rule8)) -> rule7)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple4) -> (rule4 % int3)) ((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple2) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule4 % int4)) ((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((triple2) -> (rule5 % int5))) -> (rule4 % int4)) ((((((triple2) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple2) -> (rule5 % int5))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5