Anne is big. Anne is young. Erin is red. Big people are young. All big people are green. If someone is green then they are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is red.
("Erin" "is" "red" "+")
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Anne is young.
True
1
proof
[(triple2 OR ((triple1) -> rule1))]
("Anne" "is" "young" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1))]
("Anne" "is" "young" "-")
triple2
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "green" "-")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is young.[(triple2 OR ((triple1) -> rule1))] Erin is red.[(triple3)] @1: Anne is green.[(((triple1) -> rule2))] @2: Anne is cold.[(((((triple1) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2