Anne is nice. Bob is red. Charlie is furry. Erin is nice. All nice things are furry. If something is green then it is big. All green things are red. If something is red and furry then it is young. Big things are young. Red, young things are nice. All green, nice things are young. If Erin is green and Erin is nice then Erin is big.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is red and furry then it is young.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Red, young things are nice.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All green, nice things are young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Erin is green and Erin is nice then Erin is big.
((("Erin" "is" "green" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "big" "+"))
Erin is nice.
True
1
proof
[(triple4)]
("Erin" "is" "nice" "+")
triple4
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Erin is furry.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is nice.[(triple1)] Bob is red.[(triple2)] Charlie is furry.[(triple3)] Erin is nice.[(triple4)] @1: Anne is furry.[(((triple1) -> rule1))] Erin is furry.[(((triple4) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1