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