Anne is furry. Anne is quiet. Anne is white. Dave is big. Dave is round. Dave is white. Gary is cold. All white, big things are cold. If something is quiet then it is green. If something is green and furry then it is big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All white, big things are cold.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is green and furry then it is big.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Gary is cold.
True
1
proof
[(triple7)]
("Gary" "is" "cold" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple4)]
("Dave" "is" "big" "-")
triple4
Anne is green.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "green" "+")
((triple2) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is not cold.
False
3
inv-proof
[(((triple6 triple4) -> rule1))]
("Dave" "is" "cold" "-")
((triple6 triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is big.
True
4
proof
[(((((triple2) -> rule2) triple1) -> rule3))]
("Anne" "is" "big" "+")
((((triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not big.
False
4
inv-proof
[(((((triple2) -> rule2) triple1) -> rule3))]
("Anne" "is" "big" "-")
((((triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
True
6
proof
[(((triple3 ((((triple2) -> rule2) triple1) -> rule3)) -> rule1))]
("Anne" "is" "cold" "+")
((triple3 ((((triple2) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not cold.
False
6
inv-proof
[(((triple3 ((((triple2) -> rule2) triple1) -> rule3)) -> rule1))]
("Anne" "is" "cold" "-")
((triple3 ((((triple2) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3)] Dave is big.[(triple4)] Dave is round.[(triple5)] Dave is white.[(triple6)] Gary is cold.[(triple7)] @1: Anne is green.[(((triple2) -> rule2))] Dave is cold.[(((triple6 triple4) -> rule1))] @2: Anne is big.[(((((triple2) -> rule2) triple1) -> rule3))] @3: Anne is cold.[(((triple3 ((((triple2) -> rule2) triple1) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple6 triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple3 ((((triple2) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3