Bob is not furry. Bob is not smart. Charlie is big. Charlie is not furry. Charlie is rough. Dave is big. Dave is kind. Dave is red. Dave is smart. Gary is rough. If something is kind and big then it is nice. Red, kind things are nice. Nice things are furry.
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If something is kind and big then it is nice.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Red, kind things are nice.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Dave is kind.
True
1
proof
[(triple7)]
("Dave" "is" "kind" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple6)]
("Dave" "is" "big" "-")
triple6
Dave is nice.
True
3
proof
[(((triple7 triple6) -> rule1) OR ((triple8 triple7) -> rule2))]
("Dave" "is" "nice" "+")
((triple7 triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple8 triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
3
inv-proof
[(((triple7 triple6) -> rule1) OR ((triple8 triple7) -> rule2))]
("Dave" "is" "nice" "-")
((triple7 triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple8 triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
True
4
proof
[(((((triple7 triple6) -> rule1)) -> rule3) OR ((((triple8 triple7) -> rule2)) -> rule3))]
("Dave" "is" "furry" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple8 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((((triple7 triple6) -> rule1)) -> rule3) OR ((((triple8 triple7) -> rule2)) -> rule3))]
("Dave" "is" "furry" "-")
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple8 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is not furry.[(triple1)] Bob is not smart.[(triple2)] Charlie is big.[(triple3)] Charlie is not furry.[(triple4)] Charlie is rough.[(triple5)] Dave is big.[(triple6)] Dave is kind.[(triple7)] Dave is red.[(triple8)] Dave is smart.[(triple9)] Gary is rough.[(triple10)] @1: Dave is nice.[(((triple7 triple6) -> rule1) OR ((triple8 triple7) -> rule2))] @2: Dave is furry.[(((((triple7 triple6) -> rule1)) -> rule3) OR ((((triple8 triple7) -> rule2)) -> rule3))]
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
((triple7 triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple8 triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple8 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2