The cat visits the cow. The cow chases the rabbit. The cow chases the tiger. The cow is red. The cow sees the cat. The cow sees the rabbit. The cow sees the tiger. The cow visits the tiger. The rabbit is big. The tiger chases the cat. If something sees the cat then the cat visits the tiger. If the cow is rough then the cow is young. If something is red then it is rough. If something is young then it visits the cat. If something chases the rabbit then the rabbit visits the tiger. If something visits the cow and it sees the rabbit then the rabbit sees the tiger.
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
If something sees the cat then the cat visits the tiger.
((("something" "sees" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If the cow is rough then the cow is young.
((("cow" "is" "rough" "+")) -> ("cow" "is" "young" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is young then it visits the cat.
((("something" "is" "young" "+")) -> ("something" "visits" "cat" "+"))
If something chases the rabbit then the rabbit visits the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something visits the cow and it sees the rabbit then the rabbit sees the tiger.
((("something" "visits" "cow" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
The rabbit is big.
True
1
proof
[(triple9)]
("rabbit" "is" "big" "+")
triple9
The cow is not red.
False
1
inv-proof
[(triple4)]
("cow" "is" "red" "-")
triple4
The cat visits the tiger.
True
2
proof
[(((triple5) -> rule1))]
("cat" "visits" "tiger" "+")
((triple5) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The rabbit does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule5))]
("rabbit" "visits" "tiger" "-")
((triple2) -> (rule5 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The cow is young.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("cow" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is not young.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("cow" "is" "young" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow visits the cat.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule4))]
("cow" "visits" "cat" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow does not visit the cat.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule4))]
("cow" "visits" "cat" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger visits the cat.
Unknown
rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "cat" "+")
The rabbit does not visit the cat.
Unknown
inv-rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The rabbit sees the tiger.
Unknown
rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "tiger" "+")
The tiger does not see the rabbit.
Unknown
inv-random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The tiger sees the cat.
Unknown
random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "+")
@0: The cat visits the cow.[(triple1)] The cow chases the rabbit.[(triple2)] The cow chases the tiger.[(triple3)] The cow is red.[(triple4)] The cow sees the cat.[(triple5)] The cow sees the rabbit.[(triple6)] The cow sees the tiger.[(triple7)] The cow visits the tiger.[(triple8)] The rabbit is big.[(triple9)] The tiger chases the cat.[(triple10)] @1: The cat visits the tiger.[(((triple5) -> rule1))] The cow is rough.[(((triple4) -> rule3))] The rabbit visits the tiger.[(((triple2) -> rule5))] @2: The cow is young.[(((((triple4) -> rule3)) -> rule2))] @3: The cow visits the cat.[(((((((triple4) -> rule3)) -> rule2)) -> rule4))]
The cat visits the cow.
("cat" "visits" "cow" "+")
triple1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow sees the cat.
("cow" "sees" "cat" "+")
triple5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple6
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple8
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple5) -> (rule1 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple4) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple2) -> (rule5 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3