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