The cat chases the tiger. The dog likes the cat. The tiger chases the cat. If someone likes the cat then the cat is red. If someone is red then they need the dog.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If someone likes the cat then the cat is red.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone is red then they need the dog.
((("someone" "is" "red" "+")) -> ("someone" "needs" "dog" "+"))
The dog likes the cat.
True
1
proof
[(triple2)]
("dog" "likes" "cat" "+")
triple2
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The cat is red.
True
2
proof
[(((triple2) -> rule1))]
("cat" "is" "red" "+")
((triple2) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "is" "red" "-")
((triple2) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the dog.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("cat" "needs" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not need the dog.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("cat" "needs" "dog" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "-")
The tiger needs the dog.
Unknown
rconc
[@1: The tiger needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "dog" "+")
The dog does not chase the tiger.
Unknown
inv-random
[@0: The dog chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "tiger" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cat chases the tiger.[(triple1)] The dog likes the cat.[(triple2)] The tiger chases the cat.[(triple3)] @1: The cat is red.[(((triple2) -> rule1))] @2: The cat needs the dog.[(((((triple2) -> rule1)) -> rule2))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The dog likes the cat.
("dog" "likes" "cat" "+")
triple2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
((triple2) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2