Erin is nice. All big, red things are blue. Nice things are quiet. If something is blue and nice then it is cold. If Erin is quiet then Erin is blue. All red things are big. If something is big and quiet then it is smart. If something is red then it is quiet. If Erin is red and Erin is blue then Erin is nice.
Erin is nice.
("Erin" "is" "nice" "+")
All big, red things are blue.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is blue and nice then it is cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Erin is quiet then Erin is blue.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "blue" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is big and quiet then it is smart.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Erin is red and Erin is blue then Erin is nice.
((("Erin" "is" "red" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple1)]
("Erin" "is" "nice" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple1)]
("Erin" "is" "nice" "-")
triple1
Erin is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Erin" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Erin" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
True
5
proof
[(((((((triple1) -> rule2)) -> rule4) triple1) -> rule3))]
("Erin" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((((((triple1) -> rule2)) -> rule4) triple1) -> rule3))]
("Erin" "is" "cold" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "big" "+")
@0: Erin is nice.[(triple1)] @1: Erin is quiet.[(((triple1) -> rule2))] @2: Erin is blue.[(((((triple1) -> rule2)) -> rule4))] @3: Erin is cold.[(((((((triple1) -> rule2)) -> rule4) triple1) -> rule3))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3