Bob is round. Charlie is round. Dave is rough. All blue, kind people are not cold. All white, blue people are rough. Cold, white people are not rough. If someone is blue and kind then they are not rough. Blue people are white. If Bob is round then Bob is blue. If someone is cold and not blue then they are nice. If someone is rough and kind then they are nice.
Bob is round.
("Bob" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is rough.
("Dave" "is" "rough" "+")
All blue, kind people are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
All white, blue people are rough.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Cold, white people are not rough.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "-"))
If someone is blue and kind then they are not rough.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "-"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Bob is round then Bob is blue.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "blue" "+"))
If someone is cold and not blue then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "+"))
If someone is rough and kind then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Bob is blue.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "blue" "-")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("Bob" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
True
6
proof
[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not rough.
False
6
inv-proof
[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule2))]
("Bob" "is" "rough" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "nice" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is round.[(triple1)] Charlie is round.[(triple2)] Dave is rough.[(triple3)] @1: Bob is blue.[(((triple1) -> rule6))] @2: Bob is white.[(((((triple1) -> rule6)) -> rule5))] @3: Bob is rough.[(((((((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3