The bear is nice. The rabbit visits the bear. The tiger is not red. If someone likes the rabbit then they like the tiger. If someone chases the tiger then the tiger likes the rabbit. If someone is nice then they chase the tiger.
The bear is nice.
("bear" "is" "nice" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger is not red.
("tiger" "is" "red" "-")
If someone likes the rabbit then they like the tiger.
((("someone" "likes" "rabbit" "+")) -> ("someone" "likes" "tiger" "+"))
If someone chases the tiger then the tiger likes the rabbit.
((("someone" "chases" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If someone is nice then they chase the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "tiger" "+"))
The bear is nice.
True
1
proof
[(triple1)]
("bear" "is" "nice" "+")
triple1
The rabbit does not visit the bear.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "bear" "-")
triple2
The bear chases the tiger.
True
2
proof
[(((triple1) -> rule3))]
("bear" "chases" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "chases" "tiger" "-")
((triple1) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger likes the rabbit.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger does not like the rabbit.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("tiger" "likes" "rabbit" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit does not chase the tiger.
Unknown
inv-rconc
[@1: The rabbit chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "tiger" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not chase the rabbit.
Unknown
inv-random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "-")
The bear chases the rabbit.
Unknown
random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "+")
@0: The bear is nice.[(triple1)] The rabbit visits the bear.[(triple2)] The tiger is not red.[(triple3)] @1: The bear chases the tiger.[(((triple1) -> rule3))] @2: The tiger likes the rabbit.[(((((triple1) -> rule3)) -> rule2))] @3: The tiger likes the tiger.[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple2
The tiger is not red.
("tiger" "is" "red" "-")
triple3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3