Dave is quiet. Dave is smart. Fiona is big. Fiona is rough. Gary is big. Gary is red. Gary is smart. If something is rough and big then it is quiet.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is rough and big then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Gary is red.
True
1
proof
[(triple6)]
("Gary" "is" "red" "+")
triple6
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2)] Fiona is big.[(triple3)] Fiona is rough.[(triple4)] Gary is big.[(triple5)] Gary is red.[(triple6)] Gary is smart.[(triple7)] @1: Fiona is quiet.[(((triple4 triple3) -> rule1))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4 triple3) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1