Anne is cold. Anne is not smart. Charlie is cold. Charlie is furry. Dave is nice. Gary is nice. Gary is round. If someone is green then they are furry. All round people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "+")
triple2
Gary is green.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "green" "+")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "green" "-")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("Gary" "is" "furry" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Anne is not smart.[(triple2)] Charlie is cold.[(triple3)] Charlie is furry.[(triple4)] Dave is nice.[(triple5)] Gary is nice.[(triple6)] Gary is round.[(triple7)] @1: Gary is green.[(((triple7) -> rule2))] @2: Gary is furry.[(((((triple7) -> rule2)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2