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