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