Anne is nice. Bob is cold. Charlie is furry. If Anne is young and Anne is furry then Anne is smart. Nice people are furry. Furry people are cold.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
If Anne is young and Anne is furry then Anne is smart.
((("Anne" "is" "young" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "smart" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Charlie is cold.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
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 furry.
("Anne" "is" "furry" "+")
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 furry.
("Anne" "is" "furry" "+")
int2
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Bob is cold.[(triple2)] Charlie is furry.[(triple3)] @1: Anne is furry.[(((triple1) -> rule2))] Charlie is cold.[(((triple3) -> rule3))] @2: Anne is cold.[(((((triple1) -> rule2)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2