The cow needs the mouse. The dog does not need the tiger. The mouse needs the tiger. The tiger sees the cow. If something is green and it visits the dog then it needs the cow. If something sees the tiger and it needs the tiger then the tiger needs the dog. If something needs the mouse then the mouse visits the dog. If the cow visits the dog then the cow visits the tiger. If the tiger is big and the tiger is not green then the tiger sees the cow. If something is cold then it needs the tiger. If the dog is young and the dog sees the cow then the cow visits the mouse. If something visits the dog then it sees the tiger.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something is green and it visits the dog then it needs the cow.
((("something" "is" "green" "+") ("something" "visits" "dog" "+")) -> ("something" "needs" "cow" "+"))
If something sees the tiger and it needs the tiger then the tiger needs the dog.
((("something" "sees" "tiger" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If something needs the mouse then the mouse visits the dog.
((("something" "needs" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If the cow visits the dog then the cow visits the tiger.
((("cow" "visits" "dog" "+")) -> ("cow" "visits" "tiger" "+"))
If the tiger is big and the tiger is not green then the tiger sees the cow.
((("tiger" "is" "big" "+") ("tiger" "is" "green" "~")) -> ("tiger" "sees" "cow" "+"))
If something is cold then it needs the tiger.
((("something" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If the dog is young and the dog sees the cow then the cow visits the mouse.
((("dog" "is" "young" "+") ("dog" "sees" "cow" "+")) -> ("cow" "visits" "mouse" "+"))
If something visits the dog then it sees the tiger.
((("something" "visits" "dog" "+")) -> ("something" "sees" "tiger" "+"))
The mouse needs the tiger.
True
1
proof
[(triple3)]
("mouse" "needs" "tiger" "+")
triple3
The mouse does not need the tiger.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "tiger" "-")
triple3
The mouse visits the dog.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "visits" "dog" "+")
((triple1) -> (rule3 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "visits" "dog" "-")
((triple1) -> (rule3 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse sees the tiger.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("mouse" "sees" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The mouse does not see the tiger.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("mouse" "sees" "tiger" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The tiger needs the dog.
True
5
proof
[(((((((triple1) -> rule3)) -> rule8) triple3) -> rule2))]
("tiger" "needs" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule2 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The tiger does not need the dog.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule8) triple3) -> rule2))]
("tiger" "needs" "dog" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule2 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The dog needs the cow.
Unknown
rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "needs" "cow" "+")
The cow does not need the tiger.
Unknown
inv-rconc
[@1: The cow needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "tiger" "-")
The cow visits the tiger.
Unknown
rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "tiger" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The cow needs the mouse.[(triple1)] The dog does not need the tiger.[(triple2)] The mouse needs the tiger.[(triple3)] The tiger sees the cow.[(triple4)] @1: The mouse visits the dog.[(((triple1) -> rule3))] @2: The mouse sees the tiger.[(((((triple1) -> rule3)) -> rule8))] @3: The tiger needs the dog.[(((((((triple1) -> rule3)) -> rule8) triple3) -> rule2))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple4
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((triple1) -> (rule3 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule2 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3