Bob is quiet. Dave is round. Dave is not white. If someone is rough then they are smart. If Bob is white and Bob is not rough then Bob is round. If someone is rough and not smart then they are not white. If Dave is quiet then Dave is not blue. Green, white people are round. All white, rough people are quiet. All blue people are quiet. All round people are quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Bob is white and Bob is not rough then Bob is round.
((("Bob" "is" "white" "+") ("Bob" "is" "rough" "~")) -> ("Bob" "is" "round" "+"))
If someone is rough and not smart then they are not white.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "-"))
If Dave is quiet then Dave is not blue.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "blue" "-"))
Green, white people are round.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All white, rough people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple2) -> rule8))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule8))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not blue.
True
3
proof
[(((((triple2) -> rule8)) -> rule4))]
("Dave" "is" "blue" "-")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule4))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is quiet.[(triple1)] Dave is not white.[(triple3)] Dave is round.[(triple2)] @1: Dave is quiet.[(((triple2) -> rule8))] @2: Dave is not blue.[(((((triple2) -> rule8)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is not white.
("Dave" "is" "white" "-")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2