Bob is smart. Dave is rough. Gary is smart. If someone is furry and kind then they are smart. All kind, green people are white. If Gary is kind then Gary is furry. All big, smart people are green. White, smart people are rough. All smart people are big.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is furry and kind then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All kind, green people are white.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Gary is kind then Gary is furry.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "furry" "+"))
All big, smart people are green.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
White, smart people are rough.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Gary is smart.
True
1
proof
[(triple3)]
("Gary" "is" "smart" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is smart.[(triple1)] Dave is rough.[(triple2)] Gary is smart.[(triple3)] @1: Bob is big.[(((triple1) -> rule6))] Gary is big.[(((triple3) -> rule6))] @2: Bob is green.[(((((triple1) -> rule6) triple1) -> rule4))] Gary is green.[(((((triple3) -> rule6) triple3) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2