Bob is not quiet. Charlie is rough. Dave is quiet. Gary is rough. If Bob is round and Bob is red then Bob is quiet. Rough things are round.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Bob is round and Bob is red then Bob is quiet.
((("Bob" "is" "round" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "quiet" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is not quiet.[(triple1)] Charlie is rough.[(triple2)] Dave is quiet.[(triple3)] Gary is rough.[(triple4)] @1: Charlie is round.[(((triple2) -> rule2))] Gary is round.[(((triple4) -> rule2))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple4) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1