The cat likes the cow. The cat likes the tiger. The cat visits the tiger. The cow likes the tiger. The cow visits the cat. The cow visits the tiger. The tiger likes the cow. If someone likes the cow and the cow is kind then the cow eats the cat. If someone likes the cat then the cat is cold. If the tiger is rough then the tiger is red. If someone likes the tiger then they like the cow. If someone visits the cow then they like the cat. If the cow likes the tiger and the cow visits the tiger then the tiger visits the cow.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone likes the cow and the cow is kind then the cow eats the cat.
((("someone" "likes" "cow" "+") ("cow" "is" "kind" "+")) -> ("cow" "eats" "cat" "+"))
If someone likes the cat then the cat is cold.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "cold" "+"))
If the tiger is rough then the tiger is red.
((("tiger" "is" "rough" "+")) -> ("tiger" "is" "red" "+"))
If someone likes the tiger then they like the cow.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the cow then they like the cat.
((("someone" "visits" "cow" "+")) -> ("someone" "likes" "cat" "+"))
If the cow likes the tiger and the cow visits the tiger then the tiger visits the cow.
((("cow" "likes" "tiger" "+") ("cow" "visits" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The cat likes the cow.
True
1
proof
[(triple1 OR ((triple2) -> rule4))]
("cat" "likes" "cow" "+")
triple1
((triple2) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow does not visit the tiger.
False
1
inv-proof
[(triple6)]
("cow" "visits" "tiger" "-")
triple6
The tiger visits the cow.
True
3
proof
[(((triple4 triple6) -> rule6))]
("tiger" "visits" "cow" "+")
((triple4 triple6) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "likes" "cow" "-")
((triple4) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger likes the cat.
True
4
proof
[(((((triple4 triple6) -> rule6)) -> rule5))]
("tiger" "likes" "cat" "+")
((((triple4 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger does not like the cat.
False
4
inv-proof
[(((((triple4 triple6) -> rule6)) -> rule5))]
("tiger" "likes" "cat" "-")
((((triple4 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cat is cold.
True
5
proof
[(((((((triple4 triple6) -> rule6)) -> rule5)) -> rule2))]
("cat" "is" "cold" "+")
((((((triple4 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The cat is not cold.
False
5
inv-proof
[(((((((triple4 triple6) -> rule6)) -> rule5)) -> rule2))]
("cat" "is" "cold" "-")
((((((triple4 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "red" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cat" "+")
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cat" "-")
The cow likes the cat.
Unknown
rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "cat" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat likes the cow.[(triple1 OR ((triple2) -> rule4))] The cat likes the tiger.[(triple2)] The cat visits the tiger.[(triple3)] The cow likes the tiger.[(triple4)] The cow visits the cat.[(triple5)] The cow visits the tiger.[(triple6)] The tiger likes the cow.[(triple7)] @1: The cow likes the cow.[(((triple4) -> rule4))] The tiger visits the cow.[(((triple4 triple6) -> rule6))] @2: The tiger likes the cat.[(((((triple4 triple6) -> rule6)) -> rule5))] @3: The cat is cold.[(((((((triple4 triple6) -> rule6)) -> rule5)) -> rule2))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
((triple2) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple5
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple6
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple7
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple4) -> (rule4 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple4 triple6) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((((triple4 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
((((((triple4 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3