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