The cow chases the tiger. The cow is blue. The cow is not nice. The cow is young. The cow does not need the rabbit. The cow needs the tiger. The rabbit is green. The tiger chases the cow. The tiger is big. The tiger is not nice. The tiger is not young. The tiger does not need the rabbit. If someone needs the cow and the cow is nice then the cow chases the tiger. If the cow needs the rabbit and the cow is not young then the rabbit is not green. If someone likes the tiger and the tiger is not blue then the tiger chases the cow. If someone is young then they chase the cow. If someone needs the tiger then they need the cow. If someone needs the rabbit then the rabbit chases the cow. If the rabbit is young and the rabbit likes the tiger then the tiger is young. If someone chases the cow then they chase the rabbit.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow is young.
("cow" "is" "young" "+")
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If someone needs the cow and the cow is nice then the cow chases the tiger.
((("someone" "needs" "cow" "+") ("cow" "is" "nice" "+")) -> ("cow" "chases" "tiger" "+"))
If the cow needs the rabbit and the cow is not young then the rabbit is not green.
((("cow" "needs" "rabbit" "+") ("cow" "is" "young" "~")) -> ("rabbit" "is" "green" "-"))
If someone likes the tiger and the tiger is not blue then the tiger chases the cow.
((("someone" "likes" "tiger" "+") ("tiger" "is" "blue" "~")) -> ("tiger" "chases" "cow" "+"))
If someone is young then they chase the cow.
((("someone" "is" "young" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the tiger then they need the cow.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the rabbit then the rabbit chases the cow.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If the rabbit is young and the rabbit likes the tiger then the tiger is young.
((("rabbit" "is" "young" "+") ("rabbit" "likes" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone chases the cow then they chase the rabbit.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "rabbit" "+"))
The tiger does not need the rabbit.
True
1
proof
[(triple12)]
("tiger" "needs" "rabbit" "-")
triple12
The tiger is not big.
False
1
inv-proof
[(triple9)]
("tiger" "is" "big" "-")
triple9
The cow needs the cow.
True
2
proof
[(((triple6) -> rule5))]
("cow" "needs" "cow" "+")
((triple6) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple8) -> rule8))]
("tiger" "chases" "rabbit" "-")
((triple8) -> (rule8 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cow chases the rabbit.
True
3
proof
[(((((triple4) -> rule4)) -> rule8))]
("cow" "chases" "rabbit" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow does not chase the rabbit.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule8))]
("cow" "chases" "rabbit" "-")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@2: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The tiger does not need the cow.
Unknown
inv-rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "cow" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow chases the tiger.[(triple1)] The cow does not need the rabbit.[(triple5)] The cow is blue.[(triple2)] The cow is not nice.[(triple3)] The cow is young.[(triple4)] The cow needs the tiger.[(triple6)] The rabbit is green.[(triple7)] The tiger chases the cow.[(triple8)] The tiger does not need the rabbit.[(triple12)] The tiger is big.[(triple9)] The tiger is not nice.[(triple10)] The tiger is not young.[(triple11)] @1: The cow chases the cow.[(((triple4) -> rule4))] The cow needs the cow.[(((triple6) -> rule5))] The tiger chases the rabbit.[(((triple8) -> rule8))] @2: The cow chases the rabbit.[(((((triple4) -> rule4)) -> rule8))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is not nice.
("cow" "is" "nice" "-")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple8
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is not nice.
("tiger" "is" "nice" "-")
triple10
The tiger is not young.
("tiger" "is" "young" "-")
triple11
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple4) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple6) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple8) -> (rule8 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((((triple4) -> (rule4 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2