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