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