The dog is big. The dog likes the tiger. The lion chases the squirrel. The lion eats the tiger. The squirrel eats the tiger. The squirrel likes the dog. The tiger chases the dog. The tiger chases the squirrel. The tiger eats the dog. The tiger likes the lion. If something is big then it chases the dog. If something is green and nice then it is kind.
The dog is big.
("dog" "is" "big" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something is big then it chases the dog.
((("something" "is" "big" "+")) -> ("something" "chases" "dog" "+"))
If something is green and nice then it is kind.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
The lion eats the tiger.
True
1
proof
[(triple4)]
("lion" "eats" "tiger" "+")
triple4
The lion does not eat the tiger.
False
1
inv-proof
[(triple4)]
("lion" "eats" "tiger" "-")
triple4
The dog chases the dog.
True
2
proof
[(((triple1) -> rule1))]
("dog" "chases" "dog" "+")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "chases" "dog" "-")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
The squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The dog likes the squirrel.
Unknown
random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "+")
@0: The dog is big.[(triple1)] The dog likes the tiger.[(triple2)] The lion chases the squirrel.[(triple3)] The lion eats the tiger.[(triple4)] The squirrel eats the tiger.[(triple5)] The squirrel likes the dog.[(triple6)] The tiger chases the dog.[(triple7)] The tiger chases the squirrel.[(triple8)] The tiger eats the dog.[(triple9)] The tiger likes the lion.[(triple10)] @1: The dog chases the dog.[(((triple1) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple6
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1