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