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