The cow is kind. The cow needs the squirrel. The cow sees the squirrel. The cow visits the tiger. The squirrel is kind. The squirrel is young. The squirrel sees the cow. The squirrel visits the tiger. The tiger is cold. The tiger is kind. The tiger is round. The tiger needs the cow. The tiger needs the squirrel. The tiger sees the squirrel. The tiger visits the cow. If something sees the squirrel and it visits the tiger then the squirrel does not need the tiger. If the cow visits the tiger and the cow is not big then the tiger is round. If something needs the cow then it does not visit the tiger. If something visits the cow and it visits the squirrel then the cow sees the tiger. If something needs the cow and it visits the tiger then the tiger does not visit the cow. If the squirrel is not big then the squirrel sees the cow. If something is big and not kind then it does not see the squirrel. If something is young and not kind then it sees the cow.
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something sees the squirrel and it visits the tiger then the squirrel does not need the tiger.
((("something" "sees" "squirrel" "+") ("something" "visits" "tiger" "+")) -> ("squirrel" "needs" "tiger" "-"))
If the cow visits the tiger and the cow is not big then the tiger is round.
((("cow" "visits" "tiger" "+") ("cow" "is" "big" "~")) -> ("tiger" "is" "round" "+"))
If something needs the cow then it does not visit the tiger.
((("something" "needs" "cow" "+")) -> ("something" "visits" "tiger" "-"))
If something visits the cow and it visits the squirrel then the cow sees the tiger.
((("something" "visits" "cow" "+") ("something" "visits" "squirrel" "+")) -> ("cow" "sees" "tiger" "+"))
If something needs the cow and it visits the tiger then the tiger does not visit the cow.
((("something" "needs" "cow" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "visits" "cow" "-"))
If the squirrel is not big then the squirrel sees the cow.
((("squirrel" "is" "big" "~")) -> ("squirrel" "sees" "cow" "+"))
If something is big and not kind then it does not see the squirrel.
((("something" "is" "big" "+") ("something" "is" "kind" "~")) -> ("something" "sees" "squirrel" "-"))
If something is young and not kind then it sees the cow.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "sees" "cow" "+"))
The tiger sees the squirrel.
True
1
proof
[(triple14)]
("tiger" "sees" "squirrel" "+")
triple14
The cow does not see the squirrel.
False
1
inv-proof
[(triple3)]
("cow" "sees" "squirrel" "-")
triple3
The squirrel does not need the tiger.
True
3
proof
[(((triple3 triple4) -> rule1))]
("squirrel" "needs" "tiger" "-")
((triple3 triple4) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The squirrel needs the tiger.
False
3
inv-proof
[(((triple3 triple4) -> rule1))]
("squirrel" "needs" "tiger" "+")
((triple3 triple4) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "sees" "cow" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "cow" "+")
The squirrel does not visit the cow.
Unknown
inv-random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cow is kind.[(triple1)] The cow needs the squirrel.[(triple2)] The cow sees the squirrel.[(triple3)] The cow visits the tiger.[(triple4)] The squirrel is kind.[(triple5)] The squirrel is young.[(triple6)] The squirrel sees the cow.[(triple7)] The squirrel visits the tiger.[(triple8)] The tiger is cold.[(triple9)] The tiger is kind.[(triple10)] The tiger is round.[(triple11)] The tiger needs the cow.[(triple12)] The tiger needs the squirrel.[(triple13)] The tiger sees the squirrel.[(triple14)] The tiger visits the cow.[(triple15)] @1: The squirrel does not need the tiger.[(((triple3 triple4) -> rule1))] The tiger does not visit the tiger.[(((triple12) -> rule3))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple4
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple5
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple7
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple13
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
((triple3 triple4) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
((triple12) -> (rule3 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1