Charlie is cold. Erin is young. If someone is white and not nice then they are furry. Cold people are furry. If someone is red then they are cold. Red, furry people are cold. Cold, young people are white. If someone is young then they are blue. Furry people are young. If Erin is cold and Erin is not red then Erin is not furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is white and not nice then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Red, furry people are cold.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Cold, young people are white.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Erin is cold and Erin is not red then Erin is not furry.
((("Erin" "is" "cold" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "furry" "-"))
Erin is young.
True
1
proof
[(triple2)]
("Erin" "is" "young" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple2)]
("Erin" "is" "young" "-")
triple2
Erin is blue.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule7)) -> rule5))]
("Charlie" "is" "white" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not white.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule7)) -> rule5))]
("Charlie" "is" "white" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Charlie is cold.[(triple1)] Erin is young.[(triple2)] @1: Charlie is furry.[(((triple1) -> rule2))] Erin is blue.[(((triple2) -> rule6))] @2: Charlie is young.[(((((triple1) -> rule2)) -> rule7))] @3: Charlie is blue.[(((((((triple1) -> rule2)) -> rule7)) -> rule6))] Charlie is white.[(((triple1 ((((triple1) -> rule2)) -> rule7)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3