The cow is green. The cow is not nice. The cow is rough. The cow is round. The cow is young. The cow needs the tiger. The cow sees the tiger. The cow does not visit the tiger. The tiger is green. The tiger is nice. The tiger is rough. The tiger is round. The tiger is young. The tiger needs the cow. The tiger sees the cow. The tiger does not visit the cow. If someone needs the cow and they are not young then they are rough. If someone is nice and round then they do not visit the tiger. If someone is round and they do not see the cow then they are green. If someone needs the cow and the cow visits the tiger then they need the tiger. If the cow is nice and the cow is not rough then the cow needs the tiger. If someone sees the cow and they do not need the tiger then they see the tiger.
The cow is green.
("cow" "is" "green" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
If someone needs the cow and they are not young then they are rough.
((("someone" "needs" "cow" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
If someone is nice and round then they do not visit the tiger.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "tiger" "-"))
If someone is round and they do not see the cow then they are green.
((("someone" "is" "round" "+") ("someone" "sees" "cow" "~")) -> ("someone" "is" "green" "+"))
If someone needs the cow and the cow visits the tiger then they need the tiger.
((("someone" "needs" "cow" "+") ("cow" "visits" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If the cow is nice and the cow is not rough then the cow needs the tiger.
((("cow" "is" "nice" "+") ("cow" "is" "rough" "~")) -> ("cow" "needs" "tiger" "+"))
If someone sees the cow and they do not need the tiger then they see the tiger.
((("someone" "sees" "cow" "+") ("someone" "needs" "tiger" "~")) -> ("someone" "sees" "tiger" "+"))
The cow is not nice.
True
1
proof
[(triple2)]
("cow" "is" "nice" "-")
triple2
The tiger does not see the cow.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "cow" "-")
triple15
The tiger does not visit the tiger.
True
3
proof
[(((triple10 triple12) -> rule2))]
("tiger" "visits" "tiger" "-")
((triple10 triple12) -> (rule2 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The tiger visits the tiger.
False
3
inv-proof
[(((triple10 triple12) -> rule2))]
("tiger" "visits" "tiger" "+")
((triple10 triple12) -> (rule2 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow does not visit the tiger.[(triple8)] The cow is green.[(triple1)] The cow is not nice.[(triple2)] The cow is rough.[(triple3)] The cow is round.[(triple4)] The cow is young.[(triple5)] The cow needs the tiger.[(triple6)] The cow sees the tiger.[(triple7)] The tiger does not visit the cow.[(triple16)] The tiger is green.[(triple9)] The tiger is nice.[(triple10)] The tiger is rough.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger needs the cow.[(triple14)] The tiger sees the cow.[(triple15)] @1: The tiger does not visit the tiger.[(((triple10 triple12) -> rule2))]
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
triple8
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is not nice.
("cow" "is" "nice" "-")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
triple16
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
((triple10 triple12) -> (rule2 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1