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