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