Dave is furry. Big people are red. If someone is blue and smart then they are furry. Red people are furry. All kind people are big. If Dave is smart and Dave is furry then Dave is red. If Dave is kind and Dave is smart then Dave is big. Kind people are smart. If someone is furry then they are smart.
Dave is furry.
("Dave" "is" "furry" "+")
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and smart then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Dave is smart and Dave is furry then Dave is red.
((("Dave" "is" "smart" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "red" "+"))
If Dave is kind and Dave is smart then Dave is big.
((("Dave" "is" "kind" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "big" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is furry.[(triple1)] @1: Dave is smart.[(((triple1) -> rule8))] @2: Dave is red.[(((((triple1) -> rule8) triple1) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2