The cat visits the dog. The dog eats the tiger. The tiger visits the dog. If someone is kind and green then they are big. If someone eats the tiger then the tiger is red. If someone eats the cat then they see the dog. If someone sees the cat then they visit the cat. If the dog visits the tiger then the dog visits the cat. If someone is red then they see the cat.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is kind and green then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone eats the tiger then the tiger is red.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone eats the cat then they see the dog.
((("someone" "eats" "cat" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the cat then they visit the cat.
((("someone" "sees" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If the dog visits the tiger then the dog visits the cat.
((("dog" "visits" "tiger" "+")) -> ("dog" "visits" "cat" "+"))
If someone is red then they see the cat.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cat" "+"))
The tiger visits the dog.
True
1
proof
[(triple3)]
("tiger" "visits" "dog" "+")
triple3
The dog does not eat the tiger.
False
1
inv-proof
[(triple2)]
("dog" "eats" "tiger" "-")
triple2
The tiger is red.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "red" "+")
((triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "red" "-")
((triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("tiger" "sees" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("tiger" "sees" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger visits the cat.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("tiger" "visits" "cat" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger does not visit the cat.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("tiger" "visits" "cat" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "big" "+")
The dog does not see the cat.
Unknown
inv-rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "cat" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "big" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat visits the dog.[(triple1)] The dog eats the tiger.[(triple2)] The tiger visits the dog.[(triple3)] @1: The tiger is red.[(((triple2) -> rule2))] @2: The tiger sees the cat.[(((((triple2) -> rule2)) -> rule6))] @3: The tiger visits the cat.[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
((triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3