The cow sees the dog. The dog likes the tiger. The lion sees the cow. The tiger eats the dog. If something is red then it sees the tiger. If something sees the dog then it sees the tiger. If something sees the dog then the dog is not nice. If something sees the dog then the dog sees the lion. If something is big then it does not eat the cow. If something sees the cow and the cow does not see the tiger then the tiger is big.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
If something is red then it sees the tiger.
((("something" "is" "red" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the dog then it sees the tiger.
((("something" "sees" "dog" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the dog then the dog is not nice.
((("something" "sees" "dog" "+")) -> ("dog" "is" "nice" "-"))
If something sees the dog then the dog sees the lion.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If something is big then it does not eat the cow.
((("something" "is" "big" "+")) -> ("something" "eats" "cow" "-"))
If something sees the cow and the cow does not see the tiger then the tiger is big.
((("something" "sees" "cow" "+") ("cow" "sees" "tiger" "~")) -> ("tiger" "is" "big" "+"))
The tiger eats the dog.
True
1
proof
[(triple4)]
("tiger" "eats" "dog" "+")
triple4
The lion does not see the cow.
False
1
inv-proof
[(triple3)]
("lion" "sees" "cow" "-")
triple3
The dog sees the lion.
True
2
proof
[(((triple1) -> rule4))]
("dog" "sees" "lion" "+")
((triple1) -> (rule4 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog does not see the lion.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "sees" "lion" "-")
((triple1) -> (rule4 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "big" "-")
The lion sees the tiger.
Unknown
rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "tiger" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cow sees the dog.[(triple1)] The dog likes the tiger.[(triple2)] The lion sees the cow.[(triple3)] The tiger eats the dog.[(triple4)] @1: The cow sees the tiger.[(((triple1) -> rule2))] The dog is not nice.[(((triple1) -> rule3))] The dog sees the lion.[(((triple1) -> rule4))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The lion sees the cow.
("lion" "sees" "cow" "+")
triple3
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple4
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple1) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The dog is not nice.
("dog" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple1) -> (rule4 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1