Bob is kind. Bob is nice. Dave is cold. Dave is furry. Dave is green. Dave is nice. Gary is not cold. Gary is nice. Gary is round. Harry is kind. Harry is rough. Harry is round. If someone is round and not nice then they are kind. If someone is furry then they are kind. If someone is furry and not round then they are cold. If Bob is cold and Bob is not green then Bob is not rough. Kind people are rough. If Dave is furry and Dave is not cold then Dave is not green.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is round and not nice then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry and not round then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "+"))
If Bob is cold and Bob is not green then Bob is not rough.
((("Bob" "is" "cold" "+") ("Bob" "is" "green" "~")) -> ("Bob" "is" "rough" "-"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If Dave is furry and Dave is not cold then Dave is not green.
((("Dave" "is" "furry" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "green" "-"))
Dave is nice.
True
1
proof
[(triple6)]
("Dave" "is" "nice" "+")
triple6
Harry is not kind.
False
1
inv-proof
[(triple10)]
("Harry" "is" "kind" "-")
triple10
Bob is rough.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "rough" "-")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is rough.
True
3
proof
[(((((triple4) -> rule2)) -> rule5))]
("Dave" "is" "rough" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule5))]
("Dave" "is" "rough" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4)] Dave is green.[(triple5)] Dave is nice.[(triple6)] Gary is nice.[(triple8)] Gary is not cold.[(triple7)] Gary is round.[(triple9)] Harry is kind.[(triple10)] Harry is rough.[(triple11 OR ((triple10) -> rule5))] Harry is round.[(triple12)] @1: Bob is rough.[(((triple1) -> rule5))] Dave is kind.[(((triple4) -> rule2))] @2: Dave is rough.[(((((triple4) -> rule2)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is not cold.
("Gary" "is" "cold" "-")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple10) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2