The cow is blue. The cow sees the rabbit. The cow visits the tiger. The rabbit is nice. The rabbit needs the cow. The rabbit sees the tiger. The rabbit visits the tiger. The tiger is big. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is nice. The tiger needs the rabbit. The tiger sees the rabbit. The tiger visits the rabbit. If someone sees the tiger then they visit the tiger. If someone visits the rabbit then the rabbit is big. If someone visits the cow and the cow visits the tiger then they are blue. If someone is big then they visit the cow. If someone is blue and they visit the rabbit then the rabbit is cold. If someone sees the cow then the cow sees the rabbit.
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone sees the tiger then they visit the tiger.
((("someone" "sees" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the rabbit then the rabbit is big.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If someone visits the cow and the cow visits the tiger then they are blue.
((("someone" "visits" "cow" "+") ("cow" "visits" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they visit the cow.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cow" "+"))
If someone is blue and they visit the rabbit then the rabbit is cold.
((("someone" "is" "blue" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone sees the cow then the cow sees the rabbit.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
The cow visits the tiger.
True
1
proof
[(triple3)]
("cow" "visits" "tiger" "+")
triple3
The tiger is not kind.
False
1
inv-proof
[(triple11)]
("tiger" "is" "kind" "-")
triple11
The tiger visits the cow.
True
2
proof
[(((triple8) -> rule4))]
("tiger" "visits" "cow" "+")
((triple8) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger does not visit the cow.
False
2
inv-proof
[(((triple8) -> rule4))]
("tiger" "visits" "cow" "-")
((triple8) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The rabbit visits the cow.
True
3
proof
[(((((triple15) -> rule2)) -> rule4))]
("rabbit" "visits" "cow" "+")
((((triple15) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not visit the cow.
False
3
inv-proof
[(((((triple15) -> rule2)) -> rule4))]
("rabbit" "visits" "cow" "-")
((((triple15) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
True
5
proof
[(((((((triple15) -> rule2)) -> rule4) triple3) -> rule3))]
("rabbit" "is" "blue" "+")
((((((triple15) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is not blue.
False
5
inv-proof
[(((((((triple15) -> rule2)) -> rule4) triple3) -> rule3))]
("rabbit" "is" "blue" "-")
((((((triple15) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cow" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The cow does not visit the rabbit.
Unknown
inv-random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "rabbit" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is blue.[(triple1)] The cow sees the rabbit.[(triple2)] The cow visits the tiger.[(triple3)] The rabbit is nice.[(triple4)] The rabbit needs the cow.[(triple5)] The rabbit sees the tiger.[(triple6)] The rabbit visits the tiger.[(triple7 OR ((triple6) -> rule1))] The tiger is big.[(triple8)] The tiger is blue.[(triple9 OR ((((triple8) -> rule4) triple3) -> rule3))] The tiger is cold.[(triple10)] The tiger is kind.[(triple11)] The tiger is nice.[(triple12)] The tiger needs the rabbit.[(triple13)] The tiger sees the rabbit.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The rabbit is big.[(((triple15) -> rule2))] The rabbit is cold.[(((triple9 triple15) -> rule5) OR ((((((triple8) -> rule4) triple3) -> rule3) triple15) -> rule5))] The tiger visits the cow.[(((triple8) -> rule4))] @2: The rabbit visits the cow.[(((((triple15) -> rule2)) -> rule4))] @3: The rabbit is blue.[(((((((triple15) -> rule2)) -> rule4) triple3) -> rule3))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple5
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
((triple6) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
((((triple8) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple13
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The rabbit is big.
("rabbit" "is" "big" "+")
((triple15) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple9 triple15) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((((((triple8) -> (rule4 % int3)) triple3) -> (rule3 % int2)) triple15) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple8) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((((triple15) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple15) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3