Bob is cold. Bob is red. Bob is young. Charlie is furry. Charlie is not red. Charlie is not young. Gary is cold. Gary is furry. Gary is nice. Gary is rough. Harry is furry. Harry is rough. If Gary is not young then Gary is round. If something is rough and young then it is nice. If something is young and not furry then it is nice. Rough, nice things are red. All rough, furry things are red. If something is furry and not cold then it is not rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is not young then Gary is round.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "round" "+"))
If something is rough and young then it is nice.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is young and not furry then it is nice.
((("something" "is" "young" "+") ("something" "is" "furry" "~")) -> ("something" "is" "nice" "+"))
Rough, nice things are red.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All rough, furry things are red.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is furry and not cold then it is not rough.
((("something" "is" "furry" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "-"))
Charlie is not young.
True
1
proof
[(triple6)]
("Charlie" "is" "young" "-")
triple6
Charlie is young.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "young" "+")
triple6
Harry is red.
True
3
proof
[(((triple12 triple11) -> rule5))]
("Harry" "is" "red" "+")
((triple12 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple12 triple11) -> rule5))]
("Harry" "is" "red" "-")
((triple12 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Bob is young.[(triple3)] Charlie is furry.[(triple4)] Charlie is not red.[(triple5)] Charlie is not young.[(triple6)] Gary is cold.[(triple7)] Gary is furry.[(triple8)] Gary is nice.[(triple9)] Gary is rough.[(triple10)] Harry is furry.[(triple11)] Harry is rough.[(triple12)] @1: Gary is red.[(((triple10 triple8) -> rule5) OR ((triple10 triple9) -> rule4))] Harry is red.[(((triple12 triple11) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Charlie is not young.
("Charlie" "is" "young" "-")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
((triple10 triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10 triple9) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12 triple11) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1