Anne is quiet. Dave is white. Erin is blue. Gary is big. All furry people are white. If someone is white and furry then they are big. Quiet people are furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is white and furry then they are big.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
True
6
proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not big.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is quiet.[(triple1)] Dave is white.[(triple2)] Erin is blue.[(triple3)] Gary is big.[(triple4)] @1: Anne is furry.[(((triple1) -> rule3))] @2: Anne is white.[(((((triple1) -> rule3)) -> rule1))] @3: Anne is big.[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3