Anne is big. Fiona is quiet. Gary is not round. Furry things are quiet. If something is red then it is furry. Big things are red.
Anne is big.
("Anne" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is red.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "red" "-")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Fiona is furry.
Unknown
rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "furry" "+")
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1)] Fiona is quiet.[(triple2)] Gary is not round.[(triple3)] @1: Anne is red.[(((triple1) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule3)) -> rule2))] @3: Anne is quiet.[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Gary is not round.
("Gary" "is" "round" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3