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