Anne is red. Erin is kind. Fiona is furry. Nice things are green. Kind things are red. If Erin is red then Erin is quiet. If something is nice and quiet then it is kind. If something is red then it is furry. If Erin is red and Erin is furry then Erin is nice.
Anne is red.
("Anne" "is" "red" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Erin is red then Erin is quiet.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "quiet" "+"))
If something is nice and quiet then it is kind.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Erin is red and Erin is furry then Erin is nice.
((("Erin" "is" "red" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "nice" "+"))
Fiona is furry.
True
1
proof
[(triple3)]
("Fiona" "is" "furry" "+")
triple3
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Erin is red.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "red" "+")
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "red" "-")
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Erin" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Erin" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "green" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is red.[(triple1)] Erin is kind.[(triple2)] Fiona is furry.[(triple3)] @1: Anne is furry.[(((triple1) -> rule5))] Erin is red.[(((triple2) -> rule2))] @2: Erin is furry.[(((((triple2) -> rule2)) -> rule5))] Erin is quiet.[(((((triple2) -> rule2)) -> rule3))] @3: Erin is nice.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule5)) -> rule6))] @4: Erin is green.[(((((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule5)) -> rule6)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple2) -> (rule2 % int4)) ((((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4