The cow does not need the tiger. The rabbit chases the cow. The rabbit does not chase the tiger. The rabbit is blue. The rabbit is rough. The rabbit needs the cow. The rabbit needs the tiger. The rabbit visits the cow. The rabbit visits the tiger. The tiger chases the cow. The tiger needs the cow. The tiger visits the cow. If someone needs the rabbit then they visit the rabbit. If someone chases the tiger then the tiger visits the rabbit. If someone needs the tiger then they are round. If someone chases the rabbit and the rabbit is round then the rabbit does not need the cow. If someone visits the rabbit then they chase the tiger. If someone visits the cow then the cow chases the tiger. If the rabbit does not chase the cow then the cow chases the tiger. If the rabbit visits the tiger and the tiger needs the rabbit then the rabbit does not chase the tiger.
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone needs the rabbit then they visit the rabbit.
((("someone" "needs" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone chases the tiger then the tiger visits the rabbit.
((("someone" "chases" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone needs the tiger then they are round.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "round" "+"))
If someone chases the rabbit and the rabbit is round then the rabbit does not need the cow.
((("someone" "chases" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "needs" "cow" "-"))
If someone visits the rabbit then they chase the tiger.
((("someone" "visits" "rabbit" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the cow then the cow chases the tiger.
((("someone" "visits" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If the rabbit does not chase the cow then the cow chases the tiger.
((("rabbit" "chases" "cow" "~")) -> ("cow" "chases" "tiger" "+"))
If the rabbit visits the tiger and the tiger needs the rabbit then the rabbit does not chase the tiger.
((("rabbit" "visits" "tiger" "+") ("tiger" "needs" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "-"))
The tiger chases the cow.
True
1
proof
[(triple10)]
("tiger" "chases" "cow" "+")
triple10
The rabbit does not need the tiger.
False
1
inv-proof
[(triple7)]
("rabbit" "needs" "tiger" "-")
triple7
The rabbit is round.
True
2
proof
[(((triple7) -> rule3))]
("rabbit" "is" "round" "+")
((triple7) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cow does not chase the tiger.
False
2
inv-proof
[(((triple12) -> rule6) OR ((triple8) -> rule6))]
("cow" "chases" "tiger" "-")
((triple12) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
((triple8) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
True
3
proof
[(((((triple12) -> rule6)) -> rule2) OR ((((triple8) -> rule6)) -> rule2))]
("tiger" "visits" "rabbit" "+")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The tiger does not visit the rabbit.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule2) OR ((((triple8) -> rule6)) -> rule2))]
("tiger" "visits" "rabbit" "-")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The tiger chases the tiger.
True
4
proof
[(((((((triple12) -> rule6)) -> rule2)) -> rule5) OR ((((((triple8) -> rule6)) -> rule2)) -> rule5))]
("tiger" "chases" "tiger" "+")
((((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
The tiger does not chase the tiger.
False
4
inv-proof
[(((((((triple12) -> rule6)) -> rule2)) -> rule5) OR ((((((triple8) -> rule6)) -> rule2)) -> rule5))]
("tiger" "chases" "tiger" "-")
((((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
The cow does not visit the rabbit.
Unknown
inv-rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "rabbit" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "round" "+")
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cow chases the rabbit.
Unknown
random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "+")
The tiger does not need the rabbit.
Unknown
inv-random
[@0: The tiger needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "rabbit" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
@0: The cow does not need the tiger.[(triple1)] The rabbit chases the cow.[(triple2)] The rabbit does not chase the tiger.[(triple3)] The rabbit is blue.[(triple4)] The rabbit is rough.[(triple5)] The rabbit needs the cow.[(triple6)] The rabbit needs the tiger.[(triple7)] The rabbit visits the cow.[(triple8)] The rabbit visits the tiger.[(triple9)] The tiger chases the cow.[(triple10)] The tiger needs the cow.[(triple11)] The tiger visits the cow.[(triple12)] @1: The cow chases the tiger.[(((triple12) -> rule6) OR ((triple8) -> rule6))] The rabbit is round.[(((triple7) -> rule3))] @2: The tiger visits the rabbit.[(((((triple12) -> rule6)) -> rule2) OR ((((triple8) -> rule6)) -> rule2))] @3: The tiger chases the tiger.[(((((((triple12) -> rule6)) -> rule2)) -> rule5) OR ((((((triple8) -> rule6)) -> rule2)) -> rule5))]
The cow does not need the tiger.
("cow" "needs" "tiger" "-")
triple1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple2
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple6
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple7
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple8
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple9
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple12
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple12) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
((triple8) -> (rule6 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple7) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int3