The cat needs the tiger. The cat sees the tiger. The dog is round. The dog does not see the squirrel. The dog does not visit the cat. The squirrel is not kind. The squirrel is not rough. The squirrel does not need the cat. The tiger is kind. The tiger is rough. The tiger needs the cat. The tiger does not need the squirrel. The tiger sees the dog. The tiger sees the squirrel. The tiger visits the squirrel. If someone sees the cat and they are not young then the cat is round. If someone sees the dog then the dog visits the squirrel. If someone needs the tiger then they visit the dog. If someone visits the squirrel and they do not need the dog then they visit the dog. If someone is blue then they need the tiger. If someone visits the tiger and they do not need the cat then the cat sees the squirrel. If someone is rough and they need the cat then they are blue. If someone sees the tiger and they do not need the squirrel then the tiger sees the cat.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The dog is round.
("dog" "is" "round" "+")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The dog does not visit the cat.
("dog" "visits" "cat" "-")
The squirrel is not kind.
("squirrel" "is" "kind" "-")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone sees the cat and they are not young then the cat is round.
((("someone" "sees" "cat" "+") ("someone" "is" "young" "~")) -> ("cat" "is" "round" "+"))
If someone sees the dog then the dog visits the squirrel.
((("someone" "sees" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If someone needs the tiger then they visit the dog.
((("someone" "needs" "tiger" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the squirrel and they do not need the dog then they visit the dog.
((("someone" "visits" "squirrel" "+") ("someone" "needs" "dog" "~")) -> ("someone" "visits" "dog" "+"))
If someone is blue then they need the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "tiger" "+"))
If someone visits the tiger and they do not need the cat then the cat sees the squirrel.
((("someone" "visits" "tiger" "+") ("someone" "needs" "cat" "~")) -> ("cat" "sees" "squirrel" "+"))
If someone is rough and they need the cat then they are blue.
((("someone" "is" "rough" "+") ("someone" "needs" "cat" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the tiger and they do not need the squirrel then the tiger sees the cat.
((("someone" "sees" "tiger" "+") ("someone" "needs" "squirrel" "~")) -> ("tiger" "sees" "cat" "+"))
The tiger is kind.
True
1
proof
[(triple9)]
("tiger" "is" "kind" "+")
triple9
The tiger is not rough.
False
1
inv-proof
[(triple10)]
("tiger" "is" "rough" "-")
triple10
The tiger is blue.
True
3
proof
[(((triple10 triple11) -> rule7))]
("tiger" "is" "blue" "+")
((triple10 triple11) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "visits" "dog" "-")
((triple1) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The tiger needs the tiger.
True
4
proof
[(((((triple10 triple11) -> rule7)) -> rule5))]
("tiger" "needs" "tiger" "+")
((((triple10 triple11) -> (rule7 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not need the tiger.
False
4
inv-proof
[(((((triple10 triple11) -> rule7)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((triple10 triple11) -> (rule7 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger visits the dog.
True
5
proof
[(((((((triple10 triple11) -> rule7)) -> rule5)) -> rule3))]
("tiger" "visits" "dog" "+")
((((((triple10 triple11) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger does not visit the dog.
False
5
inv-proof
[(((((((triple10 triple11) -> rule7)) -> rule5)) -> rule3))]
("tiger" "visits" "dog" "-")
((((((triple10 triple11) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The squirrel does not visit the dog.
Unknown
inv-rconc
[@3: The squirrel visits the dog.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule7 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "blue" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "blue" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "blue" "+")
The dog does not visit the tiger.
Unknown
inv-random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "-")
The cat sees the dog.
Unknown
random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The cat needs the tiger.[(triple1)] The cat sees the tiger.[(triple2)] The dog does not see the squirrel.[(triple4)] The dog does not visit the cat.[(triple5)] The dog is round.[(triple3)] The squirrel does not need the cat.[(triple8)] The squirrel is not kind.[(triple6)] The squirrel is not rough.[(triple7)] The tiger does not need the squirrel.[(triple12)] The tiger is kind.[(triple9)] The tiger is rough.[(triple10)] The tiger needs the cat.[(triple11)] The tiger sees the dog.[(triple13)] The tiger sees the squirrel.[(triple14)] The tiger visits the squirrel.[(triple15)] @1: The cat visits the dog.[(((triple1) -> rule3))] The dog visits the squirrel.[(((triple13) -> rule2))] The tiger is blue.[(((triple10 triple11) -> rule7))] @2: The tiger needs the tiger.[(((((triple10 triple11) -> rule7)) -> rule5))] @3: The tiger visits the dog.[(((((((triple10 triple11) -> rule7)) -> rule5)) -> rule3))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple4
The dog does not visit the cat.
("dog" "visits" "cat" "-")
triple5
The dog is round.
("dog" "is" "round" "+")
triple3
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
triple8
The squirrel is not kind.
("squirrel" "is" "kind" "-")
triple6
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple7
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple11
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple13
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple14
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple15
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple1) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple13) -> (rule2 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple10 triple11) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple10 triple11) -> (rule7 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((((((triple10 triple11) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3