Bob is blue. If Bob is blue and Bob is not green then Bob is not quiet. If Bob is quiet and Bob is blue then Bob is white. All smart things are quiet. All blue things are smart. If something is smart and not green then it is not blue. If something is quiet and not blue then it is nice. If Bob is not quiet then Bob is young. If something is green and not smart then it is white.
Bob is blue.
("Bob" "is" "blue" "+")
If Bob is blue and Bob is not green then Bob is not quiet.
((("Bob" "is" "blue" "+") ("Bob" "is" "green" "~")) -> ("Bob" "is" "quiet" "-"))
If Bob is quiet and Bob is blue then Bob is white.
((("Bob" "is" "quiet" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "white" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not green then it is not blue.
((("something" "is" "smart" "+") ("something" "is" "green" "~")) -> ("something" "is" "blue" "-"))
If something is quiet and not blue then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
If Bob is not quiet then Bob is young.
((("Bob" "is" "quiet" "~")) -> ("Bob" "is" "young" "+"))
If something is green and not smart then it is white.
((("something" "is" "green" "+") ("something" "is" "smart" "~")) -> ("something" "is" "white" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is smart.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
True
5
proof
[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule2))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not white.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule2))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] @1: Bob is smart.[(((triple1) -> rule4))] @2: Bob is quiet.[(((((triple1) -> rule4)) -> rule3))] @3: Bob is white.[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3