Bob is white. Charlie is kind. Dave is big. Gary is rough. If someone is white then they are rough. All round people are big. If someone is smart and not round then they are big.
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is smart and not round then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Bob is white.[(triple1)] Charlie is kind.[(triple2)] Dave is big.[(triple3)] Gary is rough.[(triple4)] @1: Bob is rough.[(((triple1) -> rule1))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1