Bob is nice. Charlie is nice. Erin is white. Young, nice things are smart. All furry, big things are nice. If Bob is nice then Bob is white. If Charlie is quiet and Charlie is young then Charlie is nice. Quiet, white things are young. If Charlie is nice and Charlie is quiet then Charlie is young.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Young, nice things are smart.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All furry, big things are nice.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Bob is nice then Bob is white.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "white" "+"))
If Charlie is quiet and Charlie is young then Charlie is nice.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "nice" "+"))
Quiet, white things are young.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Charlie is nice and Charlie is quiet then Charlie is young.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "young" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Charlie is nice.[(triple2)] Erin is white.[(triple3)] @1: Bob is white.[(((triple1) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1