Anne is smart. Bob is furry. Dave is furry. Fiona is furry. All red things are nice. Smart, nice things are furry. All smart things are red.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Smart, nice things are furry.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
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
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is smart.[(triple1)] Bob is furry.[(triple2)] Dave is furry.[(triple3)] Fiona is furry.[(triple4)] @1: Anne is red.[(((triple1) -> rule3))] @2: Anne is nice.[(((((triple1) -> rule3)) -> rule1))] @3: Anne is furry.[(((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3