Bob is rough. Charlie is green. If Bob is rough then Bob is round. All white people are rough. If Charlie is nice then Charlie is round.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
If Bob is rough then Bob is round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "+"))
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is nice then Charlie is round.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "round" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Bob is round.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "round" "-")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is rough.[(triple1)] Charlie is green.[(triple2)] @1: Bob is round.[(((triple1) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1