Anne is quiet. Charlie is blue. Charlie is round. Charlie is white. Dave is quiet. Gary is round. Gary is white. All quiet things are white. If Dave is blue then Dave is smart. All green, smart things are round.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If Dave is blue then Dave is smart.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "smart" "+"))
All green, smart things are round.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "round" "-")
triple3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Charlie is blue.[(triple2)] Charlie is round.[(triple3)] Charlie is white.[(triple4)] Dave is quiet.[(triple5)] Gary is round.[(triple6)] Gary is white.[(triple7)] @1: Anne is white.[(((triple1) -> rule1))] Dave is white.[(((triple5) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple5) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1