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