The dog is nice. The dog likes the squirrel. The dog does not need the tiger. The squirrel likes the dog. The squirrel visits the dog. The tiger likes the dog. The tiger needs the dog. The tiger needs the squirrel. The tiger does not visit the dog. The tiger visits the squirrel. If something is nice then it needs the dog. If something is rough and big then it likes the squirrel. If something needs the dog then it likes the tiger. If something is big then it visits the dog. If something visits the dog and it needs the tiger then the tiger likes the squirrel. All big things are not red. If the tiger needs the dog then the dog visits the tiger. If something is nice and it does not like the squirrel then it needs the squirrel.
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something is nice then it needs the dog.
((("something" "is" "nice" "+")) -> ("something" "needs" "dog" "+"))
If something is rough and big then it likes the squirrel.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "likes" "squirrel" "+"))
If something needs the dog then it likes the tiger.
((("something" "needs" "dog" "+")) -> ("something" "likes" "tiger" "+"))
If something is big then it visits the dog.
((("something" "is" "big" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog and it needs the tiger then the tiger likes the squirrel.
((("something" "visits" "dog" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "likes" "squirrel" "+"))
All big things are not red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
If the tiger needs the dog then the dog visits the tiger.
((("tiger" "needs" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If something is nice and it does not like the squirrel then it needs the squirrel.
((("something" "is" "nice" "+") ("something" "likes" "squirrel" "~")) -> ("something" "needs" "squirrel" "+"))
The squirrel visits the dog.
True
1
proof
[(triple5)]
("squirrel" "visits" "dog" "+")
triple5
The dog does not like the squirrel.
False
1
inv-proof
[(triple2)]
("dog" "likes" "squirrel" "-")
triple2
The dog visits the tiger.
True
2
proof
[(((triple7) -> rule7))]
("dog" "visits" "tiger" "+")
((triple7) -> (rule7 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "needs" "dog" "-")
((triple1) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog likes the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("dog" "likes" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog does not like the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("dog" "likes" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The tiger does not like the squirrel.
Unknown
inv-rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "squirrel" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "dog" "+")
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "needs" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The dog does not need the tiger.[(triple3)] The dog is nice.[(triple1)] The dog likes the squirrel.[(triple2)] The squirrel likes the dog.[(triple4)] The squirrel visits the dog.[(triple5)] The tiger does not visit the dog.[(triple9)] The tiger likes the dog.[(triple6)] The tiger needs the dog.[(triple7)] The tiger needs the squirrel.[(triple8)] The tiger visits the squirrel.[(triple10)] @1: The dog needs the dog.[(((triple1) -> rule1))] The dog visits the tiger.[(((triple7) -> rule7))] The tiger likes the tiger.[(((triple7) -> rule3))] @2: The dog likes the tiger.[(((((triple1) -> rule1)) -> rule3))]
The dog does not need the tiger.
("dog" "needs" "tiger" "-")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple4
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple5
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
triple9
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple8
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple1) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
((triple7) -> (rule7 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple7) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2