The cat is kind. The cat is rough. The cat likes the tiger. The cat sees the tiger. The cat visits the tiger. The tiger is blue. The tiger is rough. The tiger likes the cat. The tiger sees the cat. The tiger visits the cat. If someone likes the cat then they are rough. If the tiger sees the cat then the cat visits the tiger. If the tiger is rough then the tiger is blue. If someone is rough then they see the cat. If someone sees the cat then they like the tiger. If someone is rough and they see the tiger then they like the tiger. If someone visits the tiger and they are blue then they like the cat. If someone is nice then they visit the cat.
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone likes the cat then they are rough.
((("someone" "likes" "cat" "+")) -> ("someone" "is" "rough" "+"))
If the tiger sees the cat then the cat visits the tiger.
((("tiger" "sees" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If the tiger is rough then the tiger is blue.
((("tiger" "is" "rough" "+")) -> ("tiger" "is" "blue" "+"))
If someone is rough then they see the cat.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat then they like the tiger.
((("someone" "sees" "cat" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is rough and they see the tiger then they like the tiger.
((("someone" "is" "rough" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "likes" "tiger" "+"))
If someone visits the tiger and they are blue then they like the cat.
((("someone" "visits" "tiger" "+") ("someone" "is" "blue" "+")) -> ("someone" "likes" "cat" "+"))
If someone is nice then they visit the cat.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "cat" "+"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The cat is not kind.
False
1
inv-proof
[(triple1)]
("cat" "is" "kind" "-")
triple1
The tiger likes the tiger.
True
2
proof
[(((triple9) -> rule5) OR ((((triple7) -> rule4)) -> rule5) OR ((((((triple8) -> rule1)) -> rule4)) -> rule5))]
("tiger" "likes" "tiger" "+")
((triple9) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The tiger does not like the tiger.
False
2
inv-proof
[(((triple9) -> rule5) OR ((((triple7) -> rule4)) -> rule5) OR ((((((triple8) -> rule1)) -> rule4)) -> rule5))]
("tiger" "likes" "tiger" "-")
((triple9) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "visits" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "likes" "cat" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat is kind.[(triple1)] The cat is rough.[(triple2)] The cat likes the tiger.[(triple3 OR ((triple2 triple4) -> rule6) OR ((((triple2) -> rule4)) -> rule5))] The cat sees the tiger.[(triple4)] The cat visits the tiger.[(triple5 OR ((triple9) -> rule2) OR ((((triple7) -> rule4)) -> rule2) OR ((((((triple8) -> rule1)) -> rule4)) -> rule2))] The tiger is blue.[(triple6 OR ((triple7) -> rule3) OR ((((triple8) -> rule1)) -> rule3))] The tiger is rough.[(triple7 OR ((triple8) -> rule1))] The tiger likes the cat.[(triple8)] The tiger sees the cat.[(triple9 OR ((triple7) -> rule4) OR ((((triple8) -> rule1)) -> rule4))] The tiger visits the cat.[(triple10)] @1: The cat sees the cat.[(((triple2) -> rule4))] The tiger likes the tiger.[(((triple9) -> rule5) OR ((((triple7) -> rule4)) -> rule5) OR ((((((triple8) -> rule1)) -> rule4)) -> rule5))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
((triple2 triple4) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple5
((triple9) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
((triple7) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
((triple8) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple9
((triple7) -> (rule4 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple9) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3