Erin is quiet. Fiona is red. If Erin is white and Erin is kind then Erin is red. Red things are nice. If something is kind and green then it is quiet. Green, kind things are nice. All nice things are cold. If Erin is kind and Erin is nice then Erin is white. If something is nice and red then it is cold. All nice, cold things are white.
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Erin is white and Erin is kind then Erin is red.
((("Erin" "is" "white" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "red" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is kind and green then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Green, kind things are nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Erin is kind and Erin is nice then Erin is white.
((("Erin" "is" "kind" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "white" "+"))
If something is nice and red then it is cold.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All nice, cold things are white.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Fiona is red.
True
1
proof
[(triple2)]
("Fiona" "is" "red" "+")
triple2
Erin is not quiet.
False
1
inv-proof
[(triple1)]
("Erin" "is" "quiet" "-")
triple1
Fiona is nice.
True
2
proof
[(((triple2) -> rule2))]
("Fiona" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "nice" "-")
((triple2) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule1 <- FAIL)]]
("Erin" "is" "white" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is quiet.[(triple1)] Fiona is red.[(triple2)] @1: Fiona is nice.[(((triple2) -> rule2))] @2: Fiona is cold.[(((((triple2) -> rule2)) -> rule5) OR ((((triple2) -> rule2) triple2) -> rule7))] @3: Fiona is white.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule5)) -> rule8) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule7)) -> rule8))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3