Charlie is big. Erin is furry. Fiona is smart. Harry is nice. If something is big and nice then it is blue. All furry things are kind.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is big and nice then it is blue.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is big.[(triple1)] Erin is furry.[(triple2)] Fiona is smart.[(triple3)] Harry is nice.[(triple4)] @1: Erin is kind.[(((triple2) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1