The lion likes the tiger. The tiger chases the lion. If someone chases the lion then they like the tiger. If someone chases the tiger and they see the tiger then the tiger is red. If someone is red then they like the tiger. If someone likes the tiger then the tiger likes the lion. If someone sees the lion and they chase the lion then the lion likes the tiger. If someone likes the tiger then they chase the tiger.
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
If someone chases the lion then they like the tiger.
((("someone" "chases" "lion" "+")) -> ("someone" "likes" "tiger" "+"))
If someone chases the tiger and they see the tiger then the tiger is red.
((("someone" "chases" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone is red then they like the tiger.
((("someone" "is" "red" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the tiger then the tiger likes the lion.
((("someone" "likes" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If someone sees the lion and they chase the lion then the lion likes the tiger.
((("someone" "sees" "lion" "+") ("someone" "chases" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If someone likes the tiger then they chase the tiger.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
The tiger chases the lion.
True
1
proof
[(triple2)]
("tiger" "chases" "lion" "+")
triple2
The tiger does not chase the lion.
False
1
inv-proof
[(triple2)]
("tiger" "chases" "lion" "-")
triple2
The tiger likes the tiger.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the lion.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple2) -> rule1)) -> rule4))]
("tiger" "likes" "lion" "-")
((triple1) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger chases the tiger.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("tiger" "chases" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not chase the tiger.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("tiger" "chases" "tiger" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "red" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion likes the tiger.[(triple1)] The tiger chases the lion.[(triple2)] @1: The lion chases the tiger.[(((triple1) -> rule6))] The tiger likes the lion.[(((triple1) -> rule4) OR ((((triple2) -> rule1)) -> rule4))] The tiger likes the tiger.[(((triple2) -> rule1))] @2: The tiger chases the tiger.[(((((triple2) -> rule1)) -> rule6))]
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple1) -> (rule6 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((triple1) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2