Bob is big. Bob is green. Bob is kind. Bob is rough. Charlie is not rough. Charlie is round. Gary is big. Gary is green. Gary is rough. Gary is young. If something is rough and kind then it is not smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is rough and kind then it is not smart.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "-"))
Gary is big.
True
1
proof
[(triple7)]
("Gary" "is" "big" "+")
triple7
Charlie is not round.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "round" "-")
triple6
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is rough.[(triple4)] Charlie is not rough.[(triple5)] Charlie is round.[(triple6)] Gary is big.[(triple7)] Gary is green.[(triple8)] Gary is rough.[(triple9)] Gary is young.[(triple10)] @1: Bob is not smart.[(((triple4 triple3) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Bob is not smart.
("Bob" "is" "smart" "-")
((triple4 triple3) -> (rule1 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1